Event Detail

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

Recommended reading: Artemov, S. (2007). On two models of provability. In Mathematical Problems from Applied Logic II: Logics for the XXIst Century (pp. 1-52). New York, NY: Springer New York.