Skip to main content
SpringerLink
Log in

Topological Interpretations of Provability Logic

  • Chapter
  • First Online:
Leo Esakia on Duality in Modal and Intuitionistic Logics

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 4))

Abstract

Provability logic concerns the study of modality \(\Box \) as provability in formal systems such as Peano Arithmetic. A natural, albeit quite surprising, topological interpretation of provability logic has been found in the 1970s by Harold Simmons and Leo Esakia. They have observed that the dual \(\Diamond \) modality, corresponding to consistency in the context of formal arithmetic, has all the basic properties of the topological derivative operator acting on a scattered space. The topic has become a long-term project for the Georgian school of logic led by Esakia, with occasional contributions from elsewhere. More recently, a new impetus came from the study of polymodal provability logic \(\mathbf {GLP}\) that was known to be Kripke incomplete and, in general, to have a more complicated behavior than its unimodal counterpart. Topological semantics provided a better alternative to Kripke models in the sense that \(\mathbf {GLP}\) was shown to be topologically complete. At the same time, new fascinating connections with set theory and large cardinals have emerged. We give a survey of the results on topological semantics of provability logic starting from first contributions by Esakia. However, a special emphasis is put on the recent work on topological models of polymodal provability logic. We also include a few results that have not been published so far, most notably the results of Sect. 10.4 (due to the second author) and Sects. 10.7, 10.8 (due to the first author).

In memory of Leo Esakia

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    For normal modal logics, going from an equational to a Hilbert-style axiomatization and back is automatic, as they are known to be strongly finitely algebraizable (see [19, 31]). We do not assume the reader’s familiarity with algebraic logic and prefer to give explicit axiomatizations for the systems at hand.

  2. 2.

    A gödelian theory \(U\) is \(\omega \)-consistent if its extension by unnested applications of the \(\omega \)-rule \(U^{\prime }:=U+\{\forall x\,\varphi (x): \forall n\, U\vdash \varphi (\underline{n})\}\) is consistent.

  3. 3.

    There is no conventional name for the dual of the derivative operator. Sometimes it is denoted by \(t\). Here we choose the notation \(\tilde{d}\) to emphasize its connection with \(d\).

  4. 4.

    Recall that a topological space is zero-dimensional if it has a base of clopen sets.

  5. 5.

    Curiously, the reader may notice that the notion of reflection principle as used in provability logic and formal arithmetic matches very nicely the notions such as stationary reflection in set theory. (As far as we know, the two terms have evolved completely independently from one another.)

  6. 6.

    Weakly compact cardinals are the same as \(\varPi _1^1\)-indescribable cardinals, see below.

  7. 7.

    The first author thanks J. Cummings for clarifying this.

  8. 8.

    Stronger results have been announced, see [50].

  9. 9.

    It seems to be interesting to study the question of topological completeness of \(\mathbf {GLP}\) in the absence of the full axiom of choice, possibly with the axiom of determinacy.

References

  1. Abashidze M (1985) Ordinal completeness of the Gödel-Löb modal system. In: Intensional logics and the logical structure of theories. Metsniereba, Tbilisi, pp 49–73 (Russian)

    Google Scholar 

  2. Artemov S, Beklemishev L (2004) Provability logic. In: Gabbay D, Guenthner F (eds) Handbook of philosophical logic, vol 13, 2nd edn. Kluwer, Dordrecht, pp 229–403

    Google Scholar 

  3. Bagaria J (2012) Topologies on ordinals and the completeness of polymodal provability logic (in preparation)

    Google Scholar 

  4. Bagaria J, Magidor M, Sakai H (2012) Reflection and indescribability in the constructible universe. Manuscript, To appear in Israel Journal of Mathematics

    Google Scholar 

  5. Beklemishev L, Gabelaia D (2013) Topological completeness of the provability logic glp. Ann Pure Appl Logic 128(12):1201–1223

    Article  Google Scholar 

  6. Beklemishev L (2004) Provability algebras and proof-theoretic ordinals, i. Ann Pure Appl Logic 128:103–123

    Google Scholar 

  7. Beklemishev L (2005) Reflection principles and provability algebras in formal arithmetic. Uspekhi Matematicheskikh Nauk 60(2):3–78 (English trans: Russ Math Surv 60(2):197–268)

    Google Scholar 

  8. Beklemishev L (2005) Veblen hierarchy in the context of provability algebras. In: Hájek P, Valdés-Villanueva L, Westerståhl D (eds) Proceedings of the 12th international congress on logic, methodology and philosophy of science. Kings College Publications, London, pp 65–78

    Google Scholar 

  9. Beklemishev L (2006) The Worm principle. In: Chatzidakis Z, Koepke P, Pohlers W (eds) Lecture notes in logic 27. Logic Colloquium ’02. AK Peters, pp 75–95

    Google Scholar 

  10. Beklemishev L (2009) On GLP-spaces. Manuscript. http://www.mi.ras.ru/~bekl/Papers/glp-sp.pdf

  11. Beklemishev L (2010) Kripke semantics for provability logic glp. Ann Pure Appl Logic 161:756–774

    Google Scholar 

  12. Beklemishev L (2011) Ordinal completeness of bimodal provability logic GLB. In: Bezhanishvili N et al (ed) Logic, language and computation, TbiLLC 2009. Lecture notes in artificial intelligence, number 6618, pp 1–15

    Google Scholar 

  13. Beklemishev L (2011) A simplified proof of the arithmetical completeness theorem for the provability logic GLP. Trudy Matematicheskogo Instituta imeni V.A.Steklova, 274(3):32–40 (English trans: Proc Steklov Inst Math 274(3):25–33)

    Google Scholar 

  14. Beklemishev L, Bezhanishvili G, Icard T (2010) On topological models of GLP. In: Schindler R (ed) Ways of proof theory. Ontos Verlag, Heusendamm bei Frankfurt, Germany, pp 133–152

    Google Scholar 

  15. Beklemishev L, Joosten J, Vervoort M (2005) A finitary treatment of the closed fragment of japaridze’s provability logic. J Logic Comput 15(4):447–463

    Google Scholar 

  16. Bezhanishvili G, Esakia L, Gabelaia D (2005) Some results on modal axiomatization and definability for topological spaces. Studia Logica 81:325–355

    Article  Google Scholar 

  17. Bezhanishvili G, Morandi P (2010) Scattered and hereditarily irresolvable spaces in modal logic. Archive for Mathematical Logic 49(3):343–365

    Google Scholar 

  18. Blass A (1990) Infinitary combinatorics and modal logic. J Symb Logic 55(2):761–778

    Article  Google Scholar 

  19. Block W, Pigozzi D (1989) Algebraizable logics. Memoirs of the AMS 77(396)

    Google Scholar 

  20. Boolos G (1979) The unprovability of consistency: an essay in modal logic. Cambridge University Press, Cambridge

    Google Scholar 

  21. Boolos G (1993) The analytical completeness of dzhaparidze’s polymodal logics. Ann Pure Appl Logic 61:95–111

    Article  Google Scholar 

  22. Boolos G (1993) The logic of provability. Cambridge University Press, Cambridge

    Google Scholar 

  23. Carlucci L (2005) Worms, gaps and hydras. Math Logic Q 51(4):342–350

    Article  Google Scholar 

  24. Chagrov A, Zakharyaschev M (1997) Modal logic. Clarendon Press, Oxford

    Google Scholar 

  25. Fernández-Duque D, Joosten J (2012) Kripke models of transfinite provability logic. Adv Modal Logic 9:185–199

    Google Scholar 

  26. Fernández-Duque D, Joosten J (2013) Models of transfinite provability logic. J Symb Logic 78(2):543–561

    Google Scholar 

  27. Fernández-Duque D, Joosten J (2012) Turing progressions and their well-orders. In: How the world computes. Lecture notes in computer science. Springer, Berlin, pp 212–221

    Google Scholar 

  28. Esakia L (1981) Diagonal constructions, löb’s formula and cantor’s scattered spaces. Studies in logic and semantics. Metsniereba, Tbilisi, pp 128–143 (Russian)

    Google Scholar 

  29. Feferman S, Dawson J, Kleene S, Moore G, Solovay R, van Heijenoort J (eds) (1996) Kurt Gödel collected works, vol 1, Publications 1929–1936. Oxford University Press, Oxford

    Google Scholar 

  30. Fernández-Duque D (2012) The polytopologies of transfinite provability logic. Preprint arXiv:1207.6595v2 [math.LO]

  31. Font J, Jansana R, Pigozzi D (2003) A survey of abstract algebraic logic. Studia Logica 74(1–2):13–97

    Google Scholar 

  32. Foreman M, Kanamori A (eds) (2010) Handbook of set theory, vol 1–3. Springer, Berlin

    Google Scholar 

  33. Gödel K (1933) Eine Interpretation des intuitionistischen Aussagenkalkuls. Ergebnisse Math. Kolloq., 4:39–40 (English trans: [29], pp 301–303)

    Google Scholar 

  34. Gurevich Y (1985) Monadic second-order theories. In Barwise J, Feferman S (eds) Model-theoretical logics. Springer, Berlin, pp 479–506

    Google Scholar 

  35. Harrington L, Shelah S (1985) Some exact equiconsistency results in set theory. Notre Dame J Formal Logic 26:178–188

    Article  Google Scholar 

  36. Hilbert D, Bernays P (1968) Grundlagen der Mathematik, vols I and II, 2d edn. Springer, Berlin

    Google Scholar 

  37. Icard T, Joosten J (2012) Provability and interpretability logics with restricted realizations. Notre Dame J Formal Logic 53(2):133–154

    Article  Google Scholar 

  38. Icard T III (2011) A topological study of the closed fragment of glp. J Logic Comput 21(4):683–696

    Google Scholar 

  39. Ignatiev K (1993) On strong provability predicates and the associated modal logics. J Symb Logic 58:249–290

    Google Scholar 

  40. Japaridze G (1987) Modal-logical means of studying provability. PhD thesis, Moscow (Russian)

    Google Scholar 

  41. Jech T (2002) Set theory: the third millenium edition. Springer, Berlin

    Google Scholar 

  42. Kanamori A (2009) The higher infinite, 2nd edn. Springer, Berlin

    Google Scholar 

  43. Kudinov A, Shehtman V (2014) Derivational modal logics with the difference modality (this volume)

    Google Scholar 

  44. Löb M (1955) Solution of a problem of leon henkin. J Symb Logic 20:115–118

    Google Scholar 

  45. Macintyre A, Simmons H (1973) Gödel’s diagonalization technique and related properties of theories. Colloq Math 28:165–180

    Google Scholar 

  46. Magari R (1975) The diagonalizable algebras (the algebraization of the theories which express Theor.:II). Bollettino della Unione Matematica Italiana, Serie 4, 12, 1975. Suppl Fasc 3, 117–125

    Google Scholar 

  47. Magidor M (1982) Reflecting stationary sets. J Symb Logic 47:755–771

    Article  Google Scholar 

  48. McKinsey J, Tarski A (1944) The algebra of topology. Ann Math 45:141–191

    Google Scholar 

  49. Mekler A, Shehlah S (1989) The consistency strength of “every stationary set reflects”. Israel J Math 67(3):353–366

    Google Scholar 

  50. Sargsyan G (2012) On the strength of PFA, I. http://tinyurl.com/bmknyyp

  51. Segerberg K (1971) An essay in classical modal logic. Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet, Uppsala

    Google Scholar 

  52. Semadeni Z (1971) Banach spaces of continuous functions. In: Monografie matematyczne, Tom 55. PWN—Polish Scientific Publishers, Warsaw

    Google Scholar 

  53. Simmons H (1975) Topological aspects of suitable theories. Proc Edinb Math Soc 2(19):383–391

    Google Scholar 

  54. Smoryński C (1985) Self-reference and modal logic. Springer, Berlin

    Book  Google Scholar 

  55. Solovay R (1976) Provability interpretations of modal logic. Israel J Math 28:33–71

    Google Scholar 

  56. Steel J (2005) Pfa implies \(\text{ ad }^{l(\mathbb{r})}\). J Symb Logic 70(4):1255–1296

    Article  Google Scholar 

  57. Steinsvold C (2007) Topological models of belief logics. PhD thesis, New York

    Google Scholar 

  58. Visser A (1984) The provability logics of recursively enumerable theories extending Peano arithmetic at arbitrary theories extending Peano arithmetic. J Philos Logic 13:97–113

    Google Scholar 

Download references

Acknowledgments

We wish to thank the referee for many useful comments, which helped to significantly improve the readability of the paper. Thanks are also due to Guram Bezhanishvili both for his detailed comments and his patience with the slow pace this chapter was taking. The first author was supported by the Russian Foundation for Basic Research (RFBR), Russian Presidential Council for Support of Leading Scientific Schools, and the Swiss–Russian cooperation project STCP–CH–RU “Computational proof theory”. The second author was supported by the Shota Rustaveli National Science Foundation grant #FR/489/5-105/11 and the French–Georgian grant CNRS–SRNSF #4135/05-01.

Author information

Authors and Affiliations

  1. V.A. Steklov Mathematical Institute, RAS, Moscow, Russia

    Lev Beklemishev

  2. Moscow M.V. Lomonosov State University, Moscow, Russia

    Lev Beklemishev

  3. National Research University Higher School of Economics, Moscow, Russia

    Lev Beklemishev

  4. TSU Andrea Razmadze Mathematical Institute, Tbilisi, Georgia

    David Gabelaia

  5. Free University of Tbilisi, Tbilisi, Georgia

    David Gabelaia

Authors
  1. Lev Beklemishev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Gabelaia
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lev Beklemishev .

Editor information

Editors and Affiliations

  1. New Mexico State University, Las Cruces, New Mexico, USA

    Guram Bezhanishvili

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Beklemishev, L., Gabelaia, D. (2014). Topological Interpretations of Provability Logic. In: Bezhanishvili, G. (eds) Leo Esakia on Duality in Modal and Intuitionistic Logics. Outstanding Contributions to Logic, vol 4. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-8860-1_10

Download citation

Publish with us

Policies and ethics

Search

Navigation