natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The flavor of (classical) modal logic called is (classical) propositional logic equipped with a single modality usually written “” subject to the rules that for all propositions we have
. (S4 modal logic)
(in addition in S5 modal logic one adds: ).
Traditionally the canonical interpretation of the Box operator is that is the statement that “ is necessarily true.” (The de Morgan dual to the necessity modality is the “possibility” modality.) Then the interpretation of is that “If is necessarily true then it is necessarily necessarily true.” S4 modal logic appears in many temporal logics.
If instead of a single Box operator one considers box operators of this form, the resulting modal logic is denoted . Here is sometimes interpreted as “the th agent knows .”
In intuitionistic (or constructive) Modal Logic, one does not expect the possibility modality to be dual to the necessity modality, necessarily. Alex Simpson has written in his thesis the most used constructive modal logic system, but other systems exist.
The models for T modal logic corresponded to Kripke frames where each relation is reflexive.
For modal logic they are furthermore transitive.
(We show this for .)
Suppose that where is a reflexive transitive relation on . We have to check that .
Suppose , then, for every with , we have . Now suppose we seek to check that so we have with and want , so we look at all with and have to see if , but as and hold then holds, since is transitive, and we then know that .
The terminology “S4” in modal logic originates with:
The “possible worlds” Kripke semantics of S4 originates with:
See also:
A natural deduction-formulation and making explicit the modal operator as a comonad:
Gavin M. Bierman, Valeria de Paiva, Intuitionistic necessity revisited, School of Computer Science research reports-University of Birmingham CSR (1996) [researchgate, pdf]
Gavin M. Bierman, Valeria de Paiva, On an Intuitionistic Modal Logic Studia Logica 65 (2000) 383–416 [doi:10.1023/A:1005291931660, pdf]
Satoshi Kobayashi, Monad as modality, Theoretical Computer Science 175 1 (1997) 29-74 [doi:10.1016/S0304-3975(96)00169-7]
Natasha Alechina, Michael Mendler, Valeria de Paiva, Eike Ritter: Categorical and Kripke Semantics for Constructive S4 Modal Logic, in Computer Science Logic. CSL 2001 Lecture Notes in Computer Science 2142, Springer (2001) 292 [doi:10.1007/3-540-44802-0_21]
See also:
More on , and their applications in Artificial Intelligence can be found in
General books on modal logics which treat these logics thoroughly in the general context include
Patrick Blackburn, M. de Rijke and Yde Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001.
Marcus Kracht, Tools and Techniques in Modal Logic, Studies in Logic and the Foundation of Mathematics, 142, Elsevier, 1999.
Last revised on March 8, 2024 at 11:33:20. See the history of this page for a list of all contributions to it.