nLab provability logic

Idea

Provability logic studies the properties of a formal provability predicate $\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 $GL$, topological interpretations have been pioneered by H. Simmons and L. Esakia in the 1970s.

GL in Hilbert-style

The language of $GL$ has propositional variables $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)

$GL$ 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 $K4$ but not of $S4$.

Links

• Stanford Encyclopedia of Philosophy entry

Related entries

• scattered topos

• Magari algebra

• epistemic logic

• Brouwer-Heyting-Kolmogorov interpretation

• Gödel's incompleteness theorem

• arithmetic pretopos

References

• S. Artemov, L. Beklemishev, Provability logic , pp.229-403 in Gabbay, Guenthner (eds.), Handbook of Philosophical Logic vol. 13 , Kluwer Dordrecht 2004$^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.