Modal logic is a [formal_system] in which we expand [-propositional_calculus] with two new operators meant to represent necessity ($~$\square$~$) and possibility ($~$\diamond$~$).%%note:There are more [ general modal logics] with different modal predicates out there.%%
Those two operators can be defined in terms of each other. For example, we have that something is possible iff it is not necessary that its opposite is true; ie, $~$\diamond A \iff \neg \square \neg A$~$.
Thus in modal logic, you can express sentences as $~$\square A$~$ to express that it is necessary that $~$A$~$ is true. You can also go more abstract and say $~$\neg\square \bot$~$ to express that it is not necessary that false is true. If we read the box operator as "there is no mathematical proof of" then the previous sentence becomes "there is no mathematical proof of falsehood", which encodes the [ consistency of arithmetic].
There are many systems of modal logic %note: See for example [t_modal_logic T],[b_modal_logic B],[s5_modal_logic S5],[s4_modal_logic S4],[k_modal_logic K], [gls_modal_logic GLS]%, which differ in the sentences they take as [-axioms] and which [ rules of inference] they allow.
Of particular interest are the systems called normal systems of modal logic, and especially the [5l3 $~$Gödel-Löb$~$] system (called $~$GL$~$ for short, also known as the logic of provability). The main interest of $~$GL$~$ comes from being a [ decidable] logic which allows us to reason about sentences of Peano arithmetic talking about provability via [ translations], as proved by the [ arithmetical adequacy theorems of Solomonov].
Another widely studied system of modal logic is $~$GLS$~$, for which Solomonov proved [ adequacy for truth] in the [-standard_model_of_arithmetic].
The [semantics_mathematical semantics] of the normal systems of modal logic come in the form of [Kripke_models]: digraph structures composed of worlds over which a visibility relation is defined.
Sentences
Well formed sentences of modal logic are defined as follows:
- $~$\bot$~$ is a well-formed sentence of modal logic.
- The sentence letters $~$p,q,…$~$ are well-formed sentences of modal logic.
- If $~$A$~$ is a well-formed sentence, then $~$\square A$~$ is a well-formed sentence.
- If $~$A$~$ and $~$B$~$ are well formed sentences, then $~$A\to B$~$ is a well-formed sentence.
The rest of [ logical connectors] can then be defined as abbreviations for structures made from implication and $~$\bot$~$. For example , $~$\neg A = A\to \bot$~$. The possibility operator $~$\diamond$~$ is defined as $~$\neg\square\neg$~$ as per the previous discussion.