|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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 denote . Here is sometimes interpreted as “the th agent knows .”
(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 .
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
Marcus Kracht, Tools and Techniques in Modal Logic, Studies in Logic and the Foundation of Mathematics, 142, Elsevier, 1999.