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 $K$ is propositional logic equipped with a single modality usually written “$\Box$” subject to the rules that for all propositions $p, q \colon Prop$ we have
Often one adds to this the following further axioms
$\Box T \colon \Box p \to p$ (T modal logic)
$\Box 4 \colon \Box p \to \Box \Box p$. (S4 modal logic).
$K$ is the basic epistemic logic.
(Taut) All (instances of ) propositional tautologies.
For each $i = 1,\ldots, m$, the axiom, ($K_i$):
(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 $K_{(m)}$ is just the Kripke semantics of this context, so a frame, $\mathfrak{F}$ is just a set, $W$ of possible worlds with $m$ relations $R_i$. A model, $\mathfrak{M} = (\mathfrak{F},V)$, is a frame in that sense together with a valuation, $V \colon Prop \to \mathcal{P}(W)$, 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 $\Diamond_i = M_i$ whilst this uses $K_i$. 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.