**Modal logic** is a type of formal logic primarily developed in the 1960s that extends classical propositional and predicate logic to include operators expressing modality. A modal—a word that expresses a modality—qualifies a statement. For example, the statement "John is happy" might be qualified by saying that John is usually happy, in which case the term "usually" is functioning as a modal. The traditional alethic modalities, or modalities of truth, include possibility ("Possibly, *p*", "It is possible that *p*"), necessity ("Necessarily, *p*", "It is necessary that *p*"), and impossibility ("Impossibly, *p*", "It is impossible that *p*").^{[1]} Other modalities that have been formalized in modal logic include temporal modalities, or modalities of time (notably, "It was the case that *p*", "It has always been that *p*", "It will be that *p*", "It will always be that *p*"),^{[2][3]} deontic modalities (notably, "It is obligatory that *p*", and "It is permissible that *p*"), epistemic modalities, or modalities of knowledge ("It is known that *p*")^{[4]} and doxastic modalities, or modalities of belief ("It is believed that *p*").^{[5]}

A formal modal logic represents modalities using modal operators. For example, "It might rain today" and "It is possible that rain will fall today" both contain the notion of possibility. In a modal logic this is represented as an operator, "Possibly", attached to the sentence "It will rain today".

These systems usually are a Propositional logic that has two new symbols:

$ \Box $, which denotes necessity; and $ \Diamond $, which denotes possibility.

## SyntaxEdit

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.

## SemanticsEdit

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 \Diamond 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.

## TerminologyEdit

- 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.