Provability logic is a kind of modal logic in which we expand propositional calculus with two new operators meant to represent necessity () and possibility ().
Those two operators can be defined in terms of each other. For example, we have that something is possible iff it is not neccessary that its opposite is true; ie, .
Thus in modal logic you can express sentences as to express that it is necessary that is true. You can also go more abstract and say 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 consistence of arithmetic.
There are many systems of modal logic [1], 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 specially the system (called for short, also known as the logic of provability). The main interest of comes from being a decidable logic which allows us to reason about sentences of arithmetic via translations thanks to the arithmetical adequacy theorems of Solomonov.
Another widely studied system of modal logic is , 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.