Modal logic is a Formal_system in which we expand propositional_calculus with two new operators meant to represent necessity () and possibility ( $⋄$ ).^[1]

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, $⋄ A ⟺ \neg □ \neg A$ .

Thus in modal logic, you can express sentences as $□ A$ to express that it is necessary that $A$ is true. You can also go more abstract and say $\neg □ ⊥$ 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 ^[2], 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 $G ö d e l - L ö b$ system (called $G L$ for short, also known as the logic of provability). The main interest of $G L$ 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 $G L S$ , for which Solomonov proved adequacy for truth in the standard_model_of_arithmetic.

The 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:

$⊥$ 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 $□ 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 $⊥$ . For example , $\neg A = A \to ⊥$ . The possibility operator $⋄$ is defined as $\neg □ \neg$ as per the previous discussion.

^{^︎}
There are more general modal logics with different modal predicates out there.
^{^︎}
See for example T,B,S5,S4,K, GLS