Modal Logic, also known as Alethic Modal Logic is a term refering to a number of formal systems that deal with necessity and possibility. These systems usually are a Propositional logic that has two new symbols: \Box, which denotes necessity; and \Diamond, which denotes possibility.


The syntax of Modal logic is usually the syntax of propositional logic, with a new rule: If \phi is a well-formed formula, then \Box \phi and \Diamond \phi are well-formed formulas.


The semantics of Modal Logic commonly is given by kripke semantics . Let \mathcal {M}=(G,R,v) be a kripke model, where (G,R) is a kripke frame, G is a set of worlds, R is the accessibility relation, and v:G \times A \to \{t,f\} is a mapping from the Cartesian product of G and the set of propositional variables A to a set of truth values. Equivalently, v is a binary relation on G and the set of modal logic propositional variables.

Let w^* be an element of G that denotes the Actual world.

Let \mathcal{M},w\models \phi denote the truth value of \phi in the possible world w under the model \mathcal{M}.

Then, the T-schema of Modal logic could be defined recursively in the following way:

  • \mathcal{M},w\models P if and only if v(w,P)=t
  • \mathcal{M},w\models \lnot \phi if and only if it is not the case that \mathcal{M},w\models \phi.
  • \mathcal{M},w\models \phi \land \psi if and only if \mathcal{M},w\models \phi and \mathcal{M},w\models \psi.
  • \mathcal{M},w\models \Box \phi if and only if for all x \in G, if wRx then \mathcal{M},x\models \phi.
  • \mathcal{M},w\models \Diamond \phi if and only if there is a x \in G such that wRx and \mathcal{M},x\models \phi.
  • \models \phi if and only if \mathcal{M},w^*\models \phi

Necessitation RuleEdit

The necesitation rule is a rule of inference that states if a well-formed formula is a theorem under a system K, then the necessitation of the well-formed formula is also a theorem:

\vdash \phi \Rightarrow \vdash \Box \phi .

Table of axiomsEdit

Here is a list of axioms that are commonly used in Modal Logic systems. Some of these axioms are controversial, others are not.

Name: Axiom: Condition on Frames
Distribution Axiom

\Box(P \to Q) \to (\Box P \to \Box Q)

D \Box P \to \Diamond P \forall x \exists y(xRx) (Serial)
M \Box P \to P \forall x (xRx) (Reflexive)
4 \Box P \to \Box \Box P \forall x,y,z (xRy \land yRz \Rightarrow xRz) (Transitive)
B P \to \Box \Diamond P \forall x,y (xRy \Rightarrow yRx) (Symmetric)
5 \Diamond P \to \Box P \forall x,y,z (xRy \land xRz \Rightarrow yRx) (Eucledian)
CD \Diamond P \to \Box P \forall x,y,z (xRy \land xRz \Rightarrow y=z )(Functional
\Box M \Box(\Box P \to \forall x,y (xRy \Rightarrow yRy) (Shift Reflexive)
C4 \Box \Box P \to \Box P \forall x,y (xRy \Rightarrow \exists z(xRz \land zRy) (Dense)
C \Diamond \Box P \to \Box \Diamond P \forall x,y,z (xRy \land xRz \Rightarrow \exists w(yRw \land zRw)) (Convergent)

Where R is the accessiblity relation in the kripkle frame (W,R)

List of systemsEdit

  • System K: Necessitation rule and axiom N.
  • System T: System K and axiom T.
  • System S4: System T and axiom 4
  • System D?: System K and axiom D.
  • System S5: System S4 and axiom 5.


  • True propositions: Propositions true in the actual world.
  • False propositions: Propositions false in the actual world.
  • Possible propositions: Propositions that are true in at least one possible world.
  • Impossible propositions: Propositions that are true in no possible world.
  • Necessarily true propositions: Propositions that are true in all possible worlds.
  • Contingent propositions: Propositions that are true in some possible worlds and false in others.

Ad blocker interference detected!

Wikia is a free-to-use site that makes money from advertising. We have a modified experience for viewers using ad blockers

Wikia is not accessible if you’ve made further modifications. Remove the custom ad blocker rule(s) and the page will load as expected.