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 modal logic called is propositional logic equipped with a single modality usually written “” subject to the rules that for all propositions we have
Often one adds to this the following further axioms
. (S4 modal logic).
is the basic epistemic logic.
(Taut) All (instances of ) propositional tautologies.
For each , the axiom, ():
(i.e. modus ponens);
The second deduction rule corresponds to the idea that if a statement has been proved, then it is known to all ‘agents’.
This logic is the smallest normal modal logic.
The semantics of is just the Kripke semantics of this context, so a frame, is just a set, of possible worlds with relations . A model, , is a frame in that sense together with a valuation, , and the satisfaction relation is as described in geometric models for modal logics with just the difference implied by the fact that that page correspond to the use of whilst this uses . This means that
type of modal logic | relation in its Kripke frames |
---|---|
K modal logic | any relation |
K4 modal logic? | transitive relation |
T modal logic | reflexive relation |
B modal logic? | symmetric relation |
S4 modal logic | reflexive & transitive relation |
S5 modal logic | equivalence relation |
(following BdRV (2001) Table 4.1; cf. Fagin, Halpern, Moses & Vardi (1995) Thm. 3.1.5)
The notation “K” for a modal operator meant to express epistemic modality originates with:
Last revised on August 1, 2023 at 10:46:51. See the history of this page for a list of all contributions to it.