Provability logic studies the properties of a formal provability predicate 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 , topological interpretations have been pioneered by H. Simmons and L. Esakia in the 1970s.
The language of has propositional variables and logical connectives , , and one unary modality . Besides all tautologies of classical propositional logic, GL has the following axiom schemes:
. (Löb’s axiom)
with inference rules
proves the transitivity rule but not the reflexivity rule whence it is an extension of but not of .
S. Artemov, L. Beklemishev, Provability logic , pp.229-403 in Gabbay, Guenthner (eds.), Handbook of Philosophical Logic vol. 13 , Kluwer Dordrecht 2004. (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.