Abstract
We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to the appropriate categorical models for these logics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
N. Benton, G. Bierman, and V. dePaiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2), 1998.
G. M. Bierman and V. de Paiva. Intuitionistic necessity revisited. Technical Report CSR-96-10, University of Birmingham, School of Computer Science, June 1996.
J. Benthem, van. Modal logic and classical logic. Bibliopolis, Naples, 1983.
Z. Benaissa, E. Moggi, W. Taha, and T. Sheard. Logical modalities and multi-stage programming. In Workshop on Intuitionistic Modal Logics and Application (IMLA’99), Satellite to FLoC’99, Trento, Italy, 6th July 1999. Proceedings available from http://www.dcs.shef.ac.uk/~floc99im .
H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures Notre Dame, Indiana, second edition, 1957.
R. Davies and F. Pfenning. A modal analysis of staged computation. In Guy Steele, Jr., editor, Proc. of 23rd POPL, pages 258–270. ACM Press, 1996.
J. Despeyroux, F. Pfenning, and C. Schürmann. Primitive recursion for higher-order abstract syntax. In P. de Groote and J. Roger Hindley, editors, Proc. of TLCA’97, pages 147–163. LNCS 242, Springer Verlag, 1997.
M. Dummett. Elements of Intuitionism Clarendon Press, Oxford, 1977.
W. B. Ewald. Intuitionistic tense and modal logic. Journal of Symbolic Logic, 51, 1986.
K. Fine. An incomplete logic containing S4. Theoria, 39:31–42, 1974.
M. Fairtlough and M. Mendler. Propositional lax logic. Information and Computation, 137, 1997.
M. Fairtlough, M. Mendler, and M. Walton. First-order lax logic as a framework for constraint logic programming. Technical Report MIP-9714, University of Passau, July 1997. Postscript available through http://www.dcs.shef.ac.uk/~michael .
G. Fischer-Servi. Semantics for a class of intuitionistic modal calculi. In M. L. Dalla Chiara, editor, Italian Studies in the Philosophy of Science, pages 59–72. Reidel, 1980.
Neil Ghani, Valeria de Paiva, and Eike Ritter. Explicit Substitutions for Constructive Necessity. In Proceedings ICALP’98, 1998.
J. Goubault-Larrecq. Logical foundations of eval/quote mechanisms, and the modal logic S4. Manuscript, 1996.
R. Goldblatt. Metamathematics of modal logic. Reports on Mathematical Logic, 6,7:31–42, 21–52, 1976.
R. Goldblatt. Grothendieck Topology as Geometric Modality. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 27:495–529, 1981.
R. Goldblatt. Mathematics of Modality. CSLI Lecture Notes No. 43. Center for the Study of Language and Information, Stanford University, 1993.
B. P. Hilken. Duality for intuitionistic modal algebras. Journal of Pure and Applied Algebra, 148:171–189, 2000.
P. T. Johnstone. Stone Spaces. Cambridge University Press, 1982.
S. Kobayashi. Monad as modality. Theoretical Computer Science, 175:29–74, 1997.
J. Lambek and Ph. J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1985.
D. S. Macnab. Modal operators on Heyting algebras. Algebra Universalis, 12:5–29, 1981.
M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Department of Computer Science, University of Edinburgh, ECS-LFCS-93-255, March 1993.
M. Mendler. Characterising combinational timing analyses in intuitionistic modal logic. The Logic Journal of the IGPL, 8(6):821–852, November 2000.
E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.
F. Pfenning and R. Davies. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 2001.
D. Prawitz. Natural Deduction: A Proof-Theoretic Study. Almqvist and Wiksell, 1965.
G. Plotkin and C. Stirling. A framework for intuitionistic modal logics. In Theoretical aspects of reasoning about knowledge, Monterey, 1986.
A.K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994.
S.K. Thomason. An incompleteness theorem in modal logic. Theoria, 40:30–34, 1974.
A. S. Troelstra and D. vanDalen. Constructivism in Mathematics, volume II. North-Holland, 1988.
D. Wijesekera. Constructive modal logic I. Annals of Pure and Applied Logic, 50:271–301, 1990.
F. Wolter and M. Zakharyaschev. Intuitionistic Modal Logics. In Logic in Florence, 1995.
F. Wolter and M. Zakharyaschev. Intuitionistic modal logics as fragments of classical bimodal logics. In E. Orlowska, editor, Logic at Work. Kluwer, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alechina, N., Mendler, M., de Paiva, V., Ritter, E. (2001). Categorical and Kripke Semantics for Constructive S4 Modal Logic. In: Fribourg, L. (eds) Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44802-0_21
Download citation
DOI: https://doi.org/10.1007/3-540-44802-0_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42554-0
Online ISBN: 978-3-540-44802-0
eBook Packages: Springer Book Archive