Аннотация:Gödel’s modal logic approach to analyzing provability attracted a great deal of attention and eventually led to two distinct mathematical models. The first is the modal logic GL, also known as the Provability Logic, which was shown in 1979 by Solovay to be the logic of the formal provability predicate. The second is Gödel’s original modal logic of provability S4, together with its explicit counterpart, the Logic of Proofs LP, which was shown in 1995 by Artemov to provide an exact provability semantics for S4. These two models complement each other and cover a wide range of applications, from traditional proof theory to λ-calculi and formal epistemology.