nLab necessity and possibility




In the context of modal logic and specifically in epistemic modal logic, two key modalities that one wants to consider are those of necessity and possibility.

The idea is to consider for any proposition pp

  • a proposition labeled p\Box p expressing the idea that “pp is necessarily true”;

  • a proposition labeled p\lozenge p expressing the idea that “pp is possibly true”.

Via S4 modal logic

A common formalization of necessity/possibility is via S4 or S5 modal logic, whose axioms are motivated as follows:

For every comonadic modality like necessity \Box, one typically demands that it preserves implication, in the sense that

(pq)(pq).\Box(p \to q) \to (\Box p \to \Box q).

This preservation of implication is called the axiom K. In traditional non-categorical modal logic this is often all that is considered (“K modal logic), because the operators are considered de Morgan dual:

(1)A=¬((¬A)). \Box A \;=\; \neg \big( \lozenge (\neg A) \big) \,.

In an intuitionistic modal logic, one would also demand that \lozenge preserves implication in a suitable sense, such as

(pq)(pq).\Box(p\to q) \to (\lozenge p \to \lozenge q).

One may also ask for a further compatibility such as (pq)(pq)(\lozenge p \to \Box q) \to \Box(p\to q), as Simpson does.

Similarly, the axiom (pq)(pq)\Box(p \to q) \to (\Box p \to \Box q) implies that \Box preserves logical conjunction, i.e. (pq)(pq)\Box(p\wedge q) \leftrightarrow (\Box p \wedge \Box q). The nullary version ()\Box(\top)\leftrightarrow \top follows from the “necessitation rule” which says that if pp is provable in the empty context, then so is p\Box p. (This is an additional rule assumed in modal logics.) From duality (1) it follows that \lozenge preserves logical disjunction (both binary and nullary), while intuitionistically one may want to ask for this separately (Simpson does, but Biermann & de Paiva 2000 don’t).

A minimum further requirement on a formalization of \Box and \lozenge to have the interpretation of “necessity” and “possibility” is arguably that there are implications

  • pp\Box p \rightarrow p;

  • ppp \rightarrow \lozenge p,

expressing that if something is necessarily true, then that should mean that it is true in all instances, and that if something is true in one instance, then it is evidently possible for it to be true. With these additions to the above K modal logic, one speaks of T modal logic.

By similar plausibility arguments one often demands that

  • pp\Box p \to \Box \Box p

  • pp\lozenge \lozenge p \to \lozenge p

which may be read as expressing that iterating the previous reasoning does not yield any new insight. This additional enhancement to T modal logic yields S4 modal logic.

In terms of categorical logic interpreting propositional logic into a Heyting algebra, the S4 axioms just say (Bierman & de Paiva 1996, 2000) that:

As usual, we can also replace the Heyting algebra by a cartesian closed category, thereby obtaining a “proof-relevant” system; in this case monoidality of \Box does not imply directly that it preserves products, although one might reasonably ask that it does (see strong monads in computer science). Note that if one moves from Heyting algebras to cartesian closed categories the (co)monads are not necessarily idempotent (and there are good proof-theoretical reasons why they should not be so).

The above reasoning makes plausible that any operators expressing “necessity” and “possibility” should at least satisfy these (co)monad axioms. However, not every (co)monad is sensibly interpreted this way.

For example, there is

  • the (idempotent) comonad \varnothing which sends every proposition to false (the non-being-modality);

  • the (idempotent) monad *\ast which sends every proposition to true (the being-modality).

These *\emptyset \dashv \ast satisfy all of the above axioms (as well as more axioms that are being considered, such as those called S5 modal logic) but they are not a very good interpretation of the informal concepts of “possibility” and “necessity”. Under this interpretation nothing is necessarily true, and everything is possibly true. While this is not nonsensical, it is not very interesting and doesn’t correspond well to our intuitive meanings of “necessary” and “possible”.

This issue becomes more pronounced as one generalizes from the small realm of propositional logic to include both or either of:

There are many modal operators in such contexts which are all modeled by (idempotent) (co)monads but which do not have the interpretation of expressing the modes of “necessity” or “possibility”. See at modal operator for some examples.

Therefore it makes sense to ask which additional axioms on a modal operator make it an accurate formalization of the informal concepts of necessity and possibility. The answer to this may depend on context and intention (after all one is trying to find a precise formulation of an a priori informal idea).

Possible worlds via dependent types

One common philosophical interpretation of “necessarily” and “possibly” is (Kripke semantics) in terms of a collection of “possible worlds” that are similar to the “real world”, but not the same. Under this interpretation, a proposition is necessarily true if it is true in all possible worlds, and possibly true if it is true in some possible world.

Now the idea of a proposition being true “necessarily in all possible cases” or “possibly at least in one case” is formally very well established in predicate logic: it is just the interpretation of the universal quantifier “for all” \forall and of the existential quantifier “there exists” \exists. In categorical logic, these quantifiers (see there for details) are part of adjoint triple whose middle piece is context extension, and as such they naturally induce a comonad and a monad. Thus, if we interpret “necessarily” and “possibly” according to S5 modal logic in terms of possible worlds, we can model them by this base change adjoint triple (cf. Awodey 2006, p. 279):


In more detail, let WW be the context type of variables/terms on which the propositions depend, i.e. the collection “of all possible worlds” (in fact a Kripke frame for S5 modal logic, see there). Any specific choice of WW may be taken as specifying what is to be understood as a “possible world”.

Writing H *\mathbf{H}_{\ast} for the category of all context-free types under consideration and writing H /W\mathbf{H}_{/W} for the category of types in contextWW”, then in categorical logic (for instance H /()\mathbf{H}_{/(-)} might be a hyperdoctrine over a category of contexts containing objects WW and *\ast) the quantifiers w:W\forall_{w\colon W} and w:W\exists_{w\colon W} participate in a base change adjoint triple

( WW * W):H /W w:WW * w:WH. (\exists_W \dashv W^\ast \dashv \forall_W) \;\colon\; \mathbf{H}_{/W} \stackrel{\stackrel{\forall_{w \colon W}}{\longrightarrow}}{\stackrel{\stackrel{W^\ast}{\longleftarrow}}{\underset{\exists_{w\colon W}}{\longrightarrow}}} \mathbf{H} \,.

In a context of pure logic this would be called

existential quantifier\dashv context extension \dashv universal quantifier

whereas in a context of dependent type theory this would be called

dependent sum\dashv context extension \dashv dependent product.

In either case, under the suitable version of propositions as types (and using bracket types etc. if desired), the operations \forall and \exists have the usual interpretation of “for all” and “there exists”.

Note, however, that these operations change the context from WW to *\ast. In other words, if a proposition PP depends on WW, so that it may be true in some worlds and false in others, then WP\exists_W P and WP\forall_W P no longer depend on WW. The idea of a necessity and a possibility modality is to send a proposition in some context to a proposition in the same context, so that we can for instance say that PP\Box P \to P and so on. Thus we need to make WP\exists_W P and WP\forall_W P into propositions that again depend on WW — even if they now depend trivially on WW, being extended back from the absolute context *\ast to WW.

This is just what is accomplished by passing from the above adjoint triple to the induced adjoint pair on H /W\mathbf{H}_{/W} by forming composites with the context extension operation W *W^\ast

(2)(WW)((W *w:W)(W *w:W)):H /WH /W. (\underset{W}{\lozenge} \dashv \underset{W}{\Box}) \coloneqq \left( \left( W^\ast \circ \underset{w\colon W}{\exists} \right) \dashv \left( W^\ast \circ \underset{w\colon W}{\forall} \right) \right) \;\colon\; \mathbf{H}_{/W} \longrightarrow \mathbf{H}_{/W} \,.

With this, if pH /Wp\in \mathbf{H}_{/W} is a proposition about terms ww of WW (a WW-dependent type) then

  • W(p)\underset{W}{\lozenge}(p) is true/inhabited precisely if w:Wp(w)\underset{w \colon W}{\exists} p(w) is true/inhabited, hence (that is the standard interpretation of the quantifier) if it is possible for p(w)p(w) to be true for some ww;

  • W(p)\underset{W}{\Box}(p) is true/inhabited precisely if w:Wp(w)\underset{w \colon W}{\forall} p(w) is true/inhabited, hence (that is again the standard interpretation of the quantifier) if p(w)p(w) necessarily holds for all ww.

Thus, this gives one syntactic formalization of the informal meaning of “necessity” and “possibility”. The natural semantics for these base change operations is a generalization of the simple traditional possible worlds semantics of propositional necessity and possibility modalities. (There are, however, more complicated possible worlds semantics.)

Moreover, with this formalization, the modal operator W\underset{W}{\lozenge} is left adjoint to W\underset{W}{\Box} and hence both form an adjoint modality. As discussed there, this is a formalization of opposite concepts, which reflects well the opposition of necessity and possibility in their informal meaning.

Observe how the corresponding unit and counit maps properly reflect the intended logic of necessity, actuality and possibility:


Some technical remarks:

  1. In general, W\underset{W}{\lozenge} and W\underset{W}{\Box} as defined above are, while being a monad and comonad, respectively, not an idempotent monad and idempotent comonad if generalized from first-order hyperdoctrines to more general dependent type theories. But this just reflects the usual issues with propositions as types, see there for more discussion.

  2. While base change-adjunctions are essentially unique and not free to choose, there is a genuine choice in the above given by the choice of context WW. This is reflected in the subscripts of W\underset{W}{\lozenge} and W\underset{W}{\Box} above. It is the choice of this WW that gives different kinds of possibility and necessity. More generally there is in fact not just a choice of a context, but of a morphism of contexts, reflecting what is often called “accessibility of possible worlds”. This we come to below.

Relation to Potentiality

There is also an adjoint pair on the other side, H /*\mathbf{H}_{/\ast}, of the base change maps, in which the left adjoint is given by context extension back to H /W\mathbf{H}_{/W} followed by W\exists_W, and dually the right adjoint is given by W *W^\ast followed by W\forall_W. The former is the coreader comonad, whereas the latter is the reader monad (aka function monad):


If we think of the types P Type BP_\bullet \,\in\, Type_B in the given context – now called “BB” – as actual types (3) then the types down in the base context PTypeP \,\in\, Type should be thought of as potential types that fail to be actual in that they are missing information about their BB-dependency (see also at nondeterministic computation, here):

The definiteness-counit PP\star P \rightarrow P witnesses their inhabitation as following from that of a definite type after forgetting which definite world b:Bb \colon B was used to inhabit it.

More in detail, since (p B) *(p_B)^\ast is a conservative functor, the monadicity theorem (see this example) says

that the types PTypeP \,\in\, Type are equivalently

  1. those actual types P P_\bullet which carry a possibility-monad action BP P \lozenge_B P_\bullet \longrightarrow P_\bullet

  2. those actual types P P_\bullet which carry a necessity-co-monad co-action P BP P_\bullet \longrightarrow \Box_B P_\bullet

(The same conclusion in known in the theory of lenses in computer science, see there.)


This formalization compares reasonably well with Aristotle‘s discussion, who wrote (in the translation from Ferroni & Gili (2016), §44) first that:

of non-existent things some exist potentially

which is our

(, W!)non-existent thing|:|is aType W Wpotential thing \underset{ \color{blue} \text{non-existent thing} }{ \big( \varnothing ,\, \lozenge_W \varnothing \xrightarrow{\exists !} \varnothing \big) } \underset{ \color{blue} \text{is a} }{ \phantom{\vert} \colon\; \phantom{\vert} } \; \underset{ \color{blue} \text{potential thing} }{ Type^{\lozenge_W}_W }

and then:

if they exist … it is not possible that it is true to say that: this is possible but will not be the case.

hence (unwinding the double negation)

if potential things exist … and are possible then they will be the case (ie: will be actual)

which is our

(D ,ρ ):Type W Wgiven a potential thing WD which is possible|ρ |thenD vert git is actual \underset{ \color{blue}\text{given a potential thing} }{ (D_\bullet, \rho_\bullet) \,\colon\, Type_W^{\lozenge_W} } \;\;\;\;\;\; \vdash \;\;\;\;\;\; \underset{ \color{blue} \text{which is possible} }{ \lozenge_W D_\bullet } \underset{ \color{blue}\text{then} }{ \phantom{\vert} \xrightarrow{\;\; \rho_\bullet \;\;} \phantom{\vert} } \underset{ \color{blue}\text{it is actual} }{ D_\bullet \mathrlap{\phantom{vert_{g}}} }

Relative version

With this axiomatization via base change, it is immediate to consider the more general relative case where instead of base change to a unit type W*W \to \ast one considers base change

( ωω * ω):H /W w:ω 1()ω * w:ω 1()H /W 0. (\exists_\omega \dashv \omega^\ast \dashv \forall_\omega) \;\colon\; \mathbf{H}_{/W} \stackrel{\stackrel{\forall_{w \colon \omega^{-1}(-)}}{\longrightarrow}}{\stackrel{\stackrel{\omega^\ast}{\longleftarrow}}{\underset{\exists_{w\colon \omega^{-1}(-)}}{\longrightarrow}}} \mathbf{H}_{/W_0} \,.

along any morphism

ω:WW 0 \omega \colon W \longrightarrow W_0

and sets

(ωω)((ω *w:ω 1())(ω *w:ω 1())):H /WH /W. (\underset{\omega}{\lozenge} \dashv \underset{\omega}{\Box}) \coloneqq \left( \left( \omega^\ast \circ \underset{w\colon \omega^{-1}(-)}{\exists} \right) \dashv \left( \omega^\ast \circ \underset{w\colon \omega^{-1}(-)}{\forall} \right) \right) \;\colon\; \mathbf{H}_{/W} \longrightarrow \mathbf{H}_{/W} \,.

If here ω\omega is an effective epimorphism (a 1-epimorphism) then it exibits an equivalence relation on WW, where w 1w 2w_1\sim w_2 is given by ω(w 1)=ω(w 2)\omega(w_1) = \omega(w_2). In traditional possible worlds semantics such equivalence relation in a Kripke frame is called an “accessibility relation between possible worlds” for the case of S5 modal logic. Now

  • ωp\underset{\omega}{\lozenge} p is true/inhabited at wWw\in W iff it is true/inhabited at at least one w˜\tilde w in the same equivalence class of ww;

  • ωp\underset{\omega}{\Box} p is true/inhabited at wWw\in W iff it is true/inhabited at all w˜\tilde w in the same equivalence classes of ww.

For more on this see at S5 modal logicvia dependent types.


Historical examples

Historically, one informal example whose formalization in modal logic has been controversially discussed (see for instance IEP “Rudolf Carnap: Modal Logic”) is the pair of informal assertions

  1. “9 is necessarily greater than 7.”

  2. “The number of planets in the solar system is 9.”

(Remark. It maybe adds to the joy of modal logic to notice that the second sentence, which was regarded as true in our world at the time the above example was brought up, actually no longer is. Of course this only highlights that indeed this statement is not to be expected to be “necessarily true” in any sense.)

The issue with this example is that if one does not fix a decent formalization of these statements, then naively they seem to imply as correct the statement “The number of planets in the solar system is necessarily greater than 7.”, which however sounds like it ought to be wrong.

We now formalize and then analyze this example with the above prescription.

So let WW be any type, to be thought of as the type of possible worlds. Write

w:W(w):Type w\colon W \vdash \mathbb{N}(w) \colon Type

for the WW-dependent type that is constant on the ordinary type of natural numbers, i.e.(w)=\mathbb{N}(w) = \mathbb{N} for all w:Ww\colon W.

The terms of \mathbb{N}, i.e. the natural numbers, canonically extend to WW-dependent terms of this dependent type

w:W9:(w) w\colon W \vdash 9 \colon \mathbb{N}(w)

namely to the constant terms, which take the same value (here: 9) for all w:Ww \colon W.

In contrast to this, assume now that WW is such there is at least one non-constant function WW \to \mathbb{N}. In fact, in the spirit of the informal problem at hand, we require a surjective function. This gives a non-constant term of the constantly WW-dependent type of natural numbers, which we may just as well call

w:WNumberOfPlanetsInSolarSystem(w):(w). w \colon W \vdash NumberOfPlanetsInSolarSystem(w) \colon \mathbb{N}(w) \,.

That is the formalization of the above example we consider, and it should be evident enough. Now we may step back and see what the above formalization produce from this.

So consider the WW-dependent identity type

w:W(9=NumberOfPlanetsInTheSolarSystem)(w):Type. w \colon W \vdash (9 = NumberOfPlanetsInTheSolarSystem)(w) \colon Type \,.

By the assumption that NumberOfPlanetsInTheSolarSystem(w)NumberOfPlanetsInTheSolarSystem(w) is not constant in WW it follows that the dependent product over WW of that dependent identity type is the empty type, and so the same is true for W\Box_W applied to it:

  • [ W(9=NumberOfPlanetsInTheSolarSystem)][\Box_W (9 = NumberOfPlanetsInTheSolarSystem)] is false.

However, if we assume that there is one ww for which indeed NumberOfPlanetsInTheSolarSystem(w)NumberOfPlanetsInTheSolarSystem(w) takes the value 9, then the dependent sum over the dependent identity type contains that coincidence as a term, and so W\lozenge_W of our dependent identity type is inhabited. Hence

  • [ W(9=NumberOfPlanetsInTheSolarSystem)][\lozenge_W (9 = NumberOfPlanetsInTheSolarSystem)] is true.

In English words, these formal consequences are to be pronounced as:

  1. “It is false that it is necessary that the number of planets in the solar system is 9.”

  2. “It is true that it is possible that the number of planets in the solar system is 9.”

Which is just as it should be.

Similarly, the WW-dependent type

w:W(NumberOfPlanetsInTheSolarSystem>7)(w):(w) w \colon W \vdash (NumberOfPlanetsInTheSolarSystem \gt 7)(w) \colon \mathbb{N}(w)

is only going to be inhabited if indeed the value NumberOfPlanetsInTheSolarSystem(w)NumberOfPlanetsInTheSolarSystem(w) is greater than 7 for all w:Ww\colon W. With our formalization assumption above this is not the case, and so one finds that

  • [ W(NumberOfPlanetsInTheSolarSystem>7)][\Box_W (NumberOfPlanetsInTheSolarSystem \gt 7)] is false.


  • “It is false that it is necessary that the number of planets in the solar system is greater than 7.”

Quantum modal logic

under construction

We discuss1 the modal logic induced from base change of dependent types, as above, now applied to dependent linear types over finite sets (family of finite types) — to find a natural modal quantum logic (and in fact a natural quantum programming language for quantum circuits, see at quantum circuits via dependent linear types for more on this).

Given a base type (which we take to be finite)

(5)BFinType, B \;\in\; FinType \,,

write LinType BLinType_B for the BB-dependent linear types

LinType Bb:B b:LinType. \mathscr{H}_\bullet \,\in\, \mathrm{LinType}_B \;\;\;\;\;\;\leftrightarrow\;\;\;\;\;\; b : B \;\;\vdash\;\; \mathscr{H}_b : \mathrm{LinType} \,.

The intended categorical semantics is obtained by interpreting \mathscr{H}_\bullet as a BB-indexed set of complex vector spaces (or rather: Hermitian inner product spaces) which the reader may want to think of as being finite dimensional (hence: as Hilbert spaces if positive definite), though this finite-dimensionality condition of b\mathscr{H}_b is not used in the following (as opposed to the finiteness condition on BB, which is used).

We assume that our dependent linear type theory realizes base change of linear types along maps of non-linear base types in the form of Wirthmüller-type yoga of six operations:

Moreover, we assume that along maps with finite-fibers, such as the terminal map B*B \to \ast, the left base change agrees with the right base change (“ambidexterity”, so that both give the dependent biproduct b:B\otimes_{b : B} over BB):

stability:(p B) ! (p B) * =:b:B b(biproducts) \mathrm{stability} \;:\; (p_B)_! \mathscr{H}_\bullet \;\;\simeq\;\; (p_B)_\ast \mathscr{H}_\bullet \;\;=:\;\; \underset{b : B}{\bigoplus} \mathscr{H}_b \;\;\; \text{(biproducts)}

Curiously, in terms of modal logic, this is the Gell-Mann principle of quantum physics, in that it means:

Thepossible is necessary and hence actualized ϵ with some probability \array{ \llap{\text{The}}\;\text{possible} & \text{is} & \text{necessary} & \text{and hence} & \text{actualized} \\ \lozenge \mathcal{H}_\bullet & \simeq & \Box \mathcal{H}_\bullet & \xrightarrow{\phantom{--} \epsilon \phantom{--}} & \mathcal{H}_{ \bullet \; \mathrlap{\text{with some probability}} } }

Both these assumptions are verified in the linear homotopy type theory of Riley (2022), §2.4, which should have categorical semantics in (a type-theoretic model category presenting) the ( , 1 ) (\infty,1) -topos of parameterized H H\mathbb{C} -module spectra, among which complex vector spaces \mathscr{H} embed as their Eilenberg-MacLane module spectra HH\mathscr{H}.

Recalling from above the quadruple of (co-)monadic modalities associated with any base change one finds that its quantum analog for dependent linear types (along finite fibers (5))


where the interpretation of the modal (co-)units is as follows:


In the context of linear types not just (p B) *(p_B)^\ast is monadic, but also (p B) !(p_B)_!/(p B) *(p_B)_\ast (for details see the quantum reader monad), so that the factorization above enhances to the following situation:


(9)It is convenient and meaningful to declare notational conventions to: \text{It is convenient and meaningful to declare notational conventions to:} \phantom{--------------------}
  1. abbreviate p ! p * \mathscr{H} \,\coloneqq\, p_! \mathscr{H}_\bullet \,\simeq\, p_\ast \mathscr{H}_\bullet

  2. notationally suppress any outer application of (p B) *:LinTypeLinType B(p_B)^\ast \colon LinType \to LinType_B;

Thereby, the definiteness/randomness modalities in relation to necessity and possibility of classical modal logic (above) may be expressed in quantum modal logic by:

Considering the basic dependent linear type

(p B) * \mathbb{C}_\bullet \;\coloneqq\; (p_B)^\ast \mathbb{C}
b:B:LinType b \colon B \;\;\;\vdash\;\;\; \mathbb{C} \;\colon\; LinType

(which is the tensor unit in LinType BLinType_B) we may understand

B \mathscr{H} \;\coloneqq\; \Box_B \mathbb{C}_\bullet

as the Hilbert space which is spanned by a measurement basis |b\vert b \rangle.

From all this we find, first of all, that

  1. the necessity-counit exhibits the collapse of quantum states under a quantum measurement in the BB-basis

  2. the possibility-unit exhibits the condition quantum state preparation in this basis:


The collapse-principle of quantum measurement accurately expressed by the above linear necessity\toactuality\topossibility map was maybe first highlighted and made explicit in von Neumann (1932), §III.3, at least for the special case that (in our notation here) =(p B) *\mathscr{H}_\bullet \,=\, (p_B)^\ast \mathbb{C} (cf. Lüders (1951)).


We see that the base type BB (5) of quantum measurement outcomes plays the role of both

  1. the possible worlds of classical modal logicians;

  2. the many worlds of quantum interpretationists.



Discussion of modal logic of necessity and possibility goes back to Aristotle, as nicely reviewed in


  • Kant, Critique of pure reason 1781

is discussion of modality as one of the categories of pure thought, with sub-categories necessity, possibility and actuality (Wirklichkeit).


this is picked up and claimed to be refined to a dialectic system of unities of opposites.

Early discussion in the context of alethic modal logic:

See also:

Making explicit the necessity modal operator as a comonad:

The understanding of Kripke semantics for S5 modal logic as base change is indicated in:

See also:

Last revised on May 22, 2024 at 12:06:20. See the history of this page for a list of all contributions to it.