nLab provability logic





The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



Provability logic studies the properties of a formal provability predicate F\Box F interpreted as ‘F is provable’. This gives rise to modal logics kindred to K4 and its variations.

For the best known of these systems, the Gödel-Löb logic of provability GLGL, topological interpretations have been pioneered by H. Simmons and L. Esakia in the 1970s.

GL in Hilbert-style

The language of GLGL has propositional variables p 0,p 1,p_0,p_1,\dots and logical connectives \to, \bot, \top and one unary modality \Box. Besides all tautologies of classical propositional logic, GL has the following axiom schemes:

  • (φψ)(φψ)\Box (\varphi\to\psi) \to (\Box\varphi\to\Box\psi) . (Normality)

  • (φφ)φ\Box (\Box \varphi\to \varphi)\to \Box\varphi . (Löb's axiom)

with inference rules

  • φ,φψ ψ\array{ \arrayopts{\rowlines{solid}} \varphi ,\quad\varphi\to\psi\\ \psi } (Modus ponens)

  • φ φ\array{ \arrayopts{\rowlines{solid}} \varphi\\ \Box\varphi } (Necessitation)

GLGL proves the transitivity rule φφ\Box\varphi\to\Box\Box\varphi but not the reflexivity rule φφ\Box\varphi\to\varphi whence it is an extension of K4K4 but not of S4S4.


  • S. Artemov, L. Beklemishev, Provability logic , pp.229-403 in Gabbay, Guenthner (eds.), Handbook of Philosophical Logic vol. 13 , Kluwer Dordrecht 20042^2. (draft)

  • L. Beklemishev, D. Gabelaia, Topological interpretations of provability logic , arXiv:1210.7317 (2012). (abstract)

  • R. M. Solovay, Provability interpretations of modal logic , Israel J. Math. 28 (1976) pp.33–71.

Last revised on July 8, 2017 at 13:30:15. See the history of this page for a list of all contributions to it.