modal logic


(0,1)(0,1)-Category theory

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Modalities, Closure and Reflection

Modal Logics


The term modal logic refers to an enrichment of standard formal logic where the standard operations (and, or, not, implication and perhaps forall, etc.) are accompanied by certain extra operations – called modal operators and often denoted by “\lozenge” and “\Box” or similar – such that for pp any proposition the expression p\Box p is a new proposition whose interpretation is roughly as “pp holds (only) in some mode” or “pp holds (only) in a certain way”, such as: “pp is possibly true”, “pp will eventually become true”, “pp is believed to be true”, etc.

There is no established axiom set that an operator on propositions has to satisfy to count as a modal operator. As a result, for instance in the preface of (Blackburn-deRijke-Venema) et al.) it says

‘Ask three modal logicians what modal logic is, and you are likely to get at least three different answers’.

Hence there is a good bit of flexibility in the notion modal logic. The archetypical example of a modal logic, often taken to be the default example, is a system, called S4 modal logic or some slight variants (S1, S2, …) of it, that aims to model the idea of propositions being “possibly true” or “necessarily true”. We list and discuss further examples of modal logic in more detail below in Examples.

One way to view the axioms of S4 modal logic is as being those of propositional logic together with a co-monad \Box on the universe of propositions. Accordingly, many other flavours of modal operators that are being considered (but not all) are also (co)monads, see below at modal type theory – Relation to monads. This has an evident generalization to modal type theory, which is concerned with type theories equipped with (co)monads on their type universe. Hence when restricted to modalities that are required to be (co)monads, then modal logic is the counterpart in computational trinitarianism to category theory making use of closure operator monads and to computer science with monads in computer science.

For a good survey of and introduction to modal logic see SEP - Modern Origins of Modal Logic for (historical) motivation and introduction and then SEP - Modal logic for more technical details.

Modal logics have semantics in terms of sets with relations, called Kripke frames in the context of modal logic. They also have algebraic semantics in terms of algebras with (co)-closure operators. For instance, temporal logics can have posets as models.


Modal Languages

Modal logics are built on modal languages, that is the usual propositional language plus those extra modalities. (Note that modalities may also be added to predicate logic, see first-order modal logic.) The way the modalities work has to be laid down in an axiom system for the logic in question, for instance, for the temporal logic we might require an axiom saying ‘If FFϕF F\phi is true, then FϕF\phi is true’, which will read a ‘if it is going be true in the future that ϕ\phi is going to be true in the future, then …’, see temporal logic. (Is this going to be something what we might want in ‘provability logic’; is it the case that we should expect that if it is provable that something is provable then that something must be itself provable. This concentrates the modelling process on exactly how we wish to have our ‘context’ to behave.) In this way the relational nature of a context that we are looking at can get encoded into the logic.

Modal languages add one or more modal operator, often denoted \square or \lozenge into the usual propositional logics. (For the moment, we will keep things fairly simple so assume these to be unary operators and we will not be considering operators that have more than one input, for the moment at least. The general case will be considered later on, but in any case is discussed in detail in some of the books on modal logic listed below.)

We will give a modal language with nn modal operators, i\lozenge_i, i=1,,ni = 1,\ldots, n, which can be applied to propositions of the language to form new propositions. If n=1n=1, we will refer to the language, defined below, as the basic modal language.


We suppose given a set of variables, the nn-operator basic modal language, ω(n)\mathcal{L}_\omega(n), given by

ϕ::=p λ¬ϕϕ 1ϕ 2 iϕ,\phi ::= p_\lambda \mid \bot \mid \neg \phi \mid \phi_1 \vee \phi_2 \mid \lozenge_i\phi,

where the p λp_\lambda are the propositional variables ordered by finite ordinals, λ\lambda, and, as usual, i\lozenge_i is a modality for each i=1,,ni=1, \ldots , n.


This form of definition needs a bit of interpreting if you have not met it before. It gives a way of deciding if a formula is ‘well-formed’. The well formed formulae of ω(n)\mathcal{L}_\omega(n) are defined as follows: A formula is either

  • a proposition variable,

  • the propositional constant \bot, that is falsum,

  • a negated formula,

  • a disjunction of two formulae, or

  • a formula prefixed by one of the diamonds / modal operators.


The basic modal language will be ω(1)\mathcal{L}_\omega(1). We will sometimes write PropProp for the set of propositional variables / atomic formulae or whatever other reasonable term is used in a context.


The interpretation of ϕ\lozenge \phi depends on the context (to some extent), but in the initial form here it is usually said to mean ‘possibly ϕ\phi’.


Some authors use an equivalent generation rule using ϕ\square \phi, which is ¬¬ϕ\neg \lozenge \neg \phi. Of course, this interprets as ‘necessarily ϕ\phi’ in this initial form. In epistemic logic the basic modal language interprets ϕ\square \phi as saying ‘the agent knows that ϕ\phi’.


Other formulations replace \vee and ¬\neg by implication ϕ 1ϕ 2\phi_1\to \phi_2, or by \wedge and ¬\neg.


A modal logic in ω(n)\mathcal{L}_\omega(n) is any set Λ\Lambda of ω(n)\mathcal{L}_\omega(n)-formulae such that

  • Λ\Lambda includes all ω(n)\mathcal{L}_\omega(n)-formulae that are instances of tautologies,


  • Λ\Lambda is closed under the inference rule if ϕ\phi, ϕψΛ\phi\to \psi \in \Lambda then ψΛ\psi \in \Lambda , i.e. detachment or modus ponens.

One of the basic axiom systems leads to normal modal logics.



Suppose given a normal modal logic, Λ\Lambda in ω(n)\mathcal{L}_\omega(n). A formula ϕ\phi is Λ\Lambda-deducible from a set, Γ\Gamma of formulae, if there are finitely many formulae ψ 0,,ψ mΓ\psi_0,\ldots,\psi_m\in \Gamma such that

Λ(ψ 0(ψ 1((ψ mϕ))\vdash_\Lambda (\psi_0\to (\psi_1\to (\ldots \to (\psi_m\to \phi)\ldots)

that is the formula (ψ 0(ψ 1((ψ mϕ))(\psi_0\to (\psi_1\to (\ldots \to (\psi_m\to \phi)\ldots) is in Λ\Lambda.


As the set of all formulae in ω(n)\mathcal{L}_\omega(n) satisfies the conditions for a logic and any intersection of logics is itself also a logic, we have that given a set of formulae decreed to be ‘axioms’ for a logic, there is a smallest modal logic containing them.

Common modal axioms


Here is a brief list of flavors of modal logic. More details are discussed below.


We discuss the semantics of modal logics, its models.

In Kripke frames / relational structures

The usual semantics of modal languages is in terms of frames, and this is where the link with relational structures comes in. (These are quite often called ‘Kripke frames’ as Kripke was one of the first to use relational semantics in this context.

A discussion of the history can be found in (BlackburnDeRijkeVenema, page 42).

(As there is another sense to frame as the dual of a locale, we need to consider the terminology here and where necessary will use frame (modal logic) as the entry name.) A more detailed discussion of frames, models and the whole question of the semantics of modal logics is to be found at that entry.

Modal logics are thus also the logics of relational structures, in fact, Blackburn et al (see references) have as their first slogan: Modal languages are simple but expressive languages for talking about relational structures. The temporal logic that satisfies the axiom (4)(4) has models that are posets, for instance, whilst many of the epistemic logics have models which are sets with equivalence relations on them. In each case, the idea is that the relational structure gives all the possible states of some system and the modal logic describes that system. This explains the great interest in computer science and artificial intelligence of applications of modal logics.

Algebraic semantics

The usual algebraic semantics of modal logic is in terms of Boolean algebras with operators and is described in the entry algebraic models for modal logic.

Coalgebraic semantics

The geometric / relational /Kripke semantics of modal logics are instances of coalgebraic semantics. This type of semantics also provides an excellent motivation and intuition for various types of modal logic that arise naturally in computer science.

Categorical semantics

Every category comes with its internal logic. Modal operators in this internal logic can at least sometimes be identified with (co)reflectors into specified (co)reflective subcategories. See at modal type theory for more on this.

Examples for this are local toposes and cohesive toposes. See there for more details.



A nice historical overview of modern modal logic that might serve as a general introduction as well can be found in

One of the earliest texts that exhibits the intuitionist context is

A standard textbook and reference is

Two standard references are

Other texts on modal logic include

A formulation of modal logic in terms of typing judgements and type formation rules is in

A discussion of coalgebraic modal logic and of general modal logic in terms of coalgebra and the terminal coalgebra of an endofunctor is in

Formalization of modalities (higher modalities) in homotopy type theory appears around definition 1.11 of

An overview of applications of modal logic in linguistics can be found in