General references on provability logic

• Artemov, S.N., 2006, “Modal Logic in Mathematics,” in P. Blackburn, et al. (eds.), Handbook of Modal Logic, Amsterdam: Elsevier, pp. 927–970. (Scholar)
• Artemov, S.N. and L.D. Beklemishev, 2004, “Provability Logic,” in Handbook of Philosophical Logic, Second Edition, D. Gabbay and F. Guenthner, eds., Volume 13, Dordrecht: Kluwer, pp. 229–403. (Scholar)
• Boolos, G., 1979, The Unprovability of Consistency: An Essay in Modal Logic, Cambridge: Cambridge University Press. (Scholar)
• –––, 1993, The Logic of Provability, New York and Cambridge: Cambridge University Press. (Scholar)
• de Jongh, D.H.J. and G. Japaridze, 1998, “The Logic of Provability,” in Handbook of Proof Theory, Buss, S.R. (ed.), Amsterdam: North-Holland, pp. 475-546. (Scholar)
• Lindström, P., 1996, “Provability Logic—A Short Introduction,” Theoria, 52(1–2): 19–61. (Scholar)
• Segerberg, K., 1971, An Essay in Classical Modal Logic, Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet. (Scholar)
• Švejdar, V., 2000, “On Provability Logic,” Nordic Journal of Philosophy, 4: 95–116. (Scholar)
• Smoryński, C., 1984, “Modal Logic and Self-Reference,” in D.M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic (Volume II: Extensions of Classical Logic), Dordrecht: Springer, pp. 441–495. (Scholar)
• Smoryński, C., 1985, Self-Reference and Modal Logic, New York: Springer-Verlag. (Scholar)
• Verbrugge, R. 1996, “Provability” in The Encyclopedia of Philosophy (Supplement), D.M. Borchert (ed.), New York: Simon and Schuster MacMillan, pp. 476–478. (Scholar)
• Visser, A., 1998, “Provability Logic,” in Routledge Encyclopedia of Philosophy, W. Craig (ed.), London: Routledge, pp. 793–797. (Scholar)

History

• van Benthem, J.F.A.K., 1978, “Four Paradoxes,” Journal of Philosophical Logic, 7(1): 49–72. (Scholar)
• Boolos, G. and G. Sambin, 1991, “Provability: The Emergence of a Mathematical Modality,” Studia Logica, 50(1): 1–23. (Scholar)
• Gödel, K., 1933, “Eine Interpretation des intuitionistischen Aussagenkalküls,” Ergebnisse eines Mathematischen Kolloquiums, 4: 39–40; translation “An Interpretation of the Intuitionistic Propositional Calculus,” in K. Gödel, Collected Works, S. Feferman et al. (eds.), Oxford and New York: Oxford University Press, Volume 1, 1986, pp. 300–302. (Scholar)
• –––, 1931, “Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme I,” Monatshefte für Mathematik und Physik, 38: 173–198. (Scholar)
• Halbach, V., and A. Visser, 2014, “The Henkin Sentence,” in M. Mazano, I. Sain, and E. Alonso (eds.), The Life and Work of Leon Henkin: Essays on His Contributions, Dordrecht: Springer International Publishing, pp. 249–263. (Scholar)
• Henkin, L., 1952, “A Problem Concerning Provability,” Journal of Symbolic Logic, 17: 160. (Scholar)
• –––, 1954, “Review of G. Kreisel: On a Problem of Leon Henkin’s,” Journal of Symbolic Logic, 19(3): 219–220. (Scholar)
• Hilbert, D. and P. Bernays, 1939, Grundlagen der Mathematik, volume 2, Berlin/Heidelberg/New York: Springer-Verlag. (Scholar)
• de Jongh, D.H.J., forthcoming, “Notes on my Scientific Life,” in N. Bezhanishvili, R. Iemhoff and F. Yang (eds.), Dick de Jongh on Intuitionistic and Provability Logic, Cham: Springer. (Scholar)
• Kreisel, G., 1953, “On a Problem of Leon Henkin’s,” Indagationes Mathematicae, 15: 405–406. (Scholar)
• Lewis, C.I., 1912, “Implication and the Algebra of Logic,” Mind, 21: 522–531. (Scholar)
• Löb, M.H., 1955, “Solution of a Problem of Leon Henkin,” Journal of Symbolic Logic, 20: 115–118. (Scholar)
• Macintyre, A.J. and H. Simmons, 1973, “Gödel’s Diagonalization Technique and Related Properties of Theories,” Colloquium Mathematicum, 28: 165–180.
• Magari, R., 1975a, “The Diagonalizable Algebras,” Bollettino della Unione Mathematica Italiana, 12: 117–125. (Scholar)
• –––, 1975b, “Representation and Duality Theory for Diagonalizable Algebras,” Studia Logica, 34(4): 305–313. (Scholar)
• Smiley, T.J., 1963, “The Logical Basis of Ethics,” Acta Philosophica Fennica, 16: 237–246. (Scholar)
• Smoryński, C., 1991, “The Development of Self-reference: Löb’s Theorem,” in T. Drucker (ed.), Perspectives on the History of Mathematical Logic, Basel: Birkhäuser, pp. 110–133. (Scholar)

Cut-elimination for provability logic

• Avron, A., 1984, “On Modal Systems Having Arithmetical Interpretations,” The Journal of Symbolic Logic, 49(3): 935–942. (Scholar)
• Bílková, M., 2016, “Uniform Interpolation in Provability Logics,” in J. van Eijck, R. Iemhoff, and J.J. Joosten (eds.), Liber Amicorum Alberti: A Tribute to Albert Visser, London: College Publications, pp. 57–90. (Scholar)
• Goré, R. and R. Ramanayake, 2008, “Valentini’s Cut-Elimination for Provability Logic Resolved,” in Advances in Modal Logic (Volume 7), C. Areces and R. Goldblatt (eds.), London: College Publications, pp. 67–86. (Scholar)
• Goré, R. and R. Ramanayake, 2012, “Valentini’s Cut-Elimination for Provability Logic Resolved,” Review of Symbolic Logic, 5(2): 212–238. (Scholar)
• Goré, R., Ramanayake, R., and Shillito, I., 2021, “Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq,” in Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Cham: Springer International Publishing, pp. 299–313. (Scholar)
• Maksimova, L.L., 1989a, “A Continuum of Normal Extensions of Modal Provability Logic with the Interpolation Property,” Sibirskii Matematicheskii Zhurnal, 30(6): 122–131. (Scholar)
• Maksimova, L.L., 1989b, “Definability Theorems in Normal Extensions of the Probability Logic,” Studia Logica, 48(4): 495–507. (Scholar)
• Negri, S., 2005, “Proof Analysis in Modal Logic,” Journal of Philosophical Logic, 50: 507–544. (Scholar)
• Negri, S., 2014, “Proofs and Countermodels in Non-classical Logics,” Logica Universalis, 8(1): 25–60. (Scholar)
• Poggiolesi, F., 2009, “A Purely Syntactic and Cut-free Sequent Calculus for the Modal Logic of Provability,” The Review of Symbolic Logic, 2(4): 593–611. (Scholar)
• Rautenberg, W., 1983, “Modal Tableau Calculi and Interpolation,” Journal of Philosophical Logic, 12(4): 403–423. (Scholar)
• Sambin, G., and S. Valentini, 1982, “The Modal Logic of Provability. The Sequential Approach,” Journal of Philosophical Logic, 11(3): 311–342. (Scholar) (Scholar)
• Shamkanov, D.S., 2011, “Interpolation Properties for Provability Logics GL and GLP,” Proceedings of the Steklov Institute of Mathematics, 274(1): 303–316. (Scholar)
• –––, 2014, “Circular Proofs for the Gödel-Löb Provability Logic,” Mathematical Notes, 96(4): 575–585. (Scholar)
• –––, 2020, “Non-well-founded Derivations in the Gödel-Löb Provability Logic,” Review of Symbolic Logic, 13(4): 776–796. (Scholar)
• Smoryński, C., 1978, “Beth’s Theorem and Self-referential Sentences,” Studies in Logic and the Foundations of Mathematics, 96: 253–261. (Scholar)
• Valentini, S., 1983, “The Modal Logic of Provability: Cut-Elimination,” Journal of Philosophical Logic, 12: 471–476. (Scholar)

The fixed point theorem

• van Benthem, J., forthcoming, “An Abstract Look at the Fixed-Point Theorem for Provability Logic,” in N. Bezhanishvili, R. Iemhoff and F. Yang (eds.), Dick de Jongh on Intuitionistic and Provability Logic, Cham: Springer. (Scholar)
• de Jongh, D.H.J., and F. Montagna, 1988, “Provable Fixed Points,” Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 34(3): 229–250. (Scholar)
• Lindström, P., 2006, “Note on Some Fixed Point Constructions in Provability Logic,” Journal of Philosophical Logic, 35(3): 225–230. (Scholar)
• Reidhaar-Olson, L., 1990, “A New Proof of the Fixed-point Theorem of Provability Logic,” Notre Dame Journal of Formal Logic, 31(1): 37–43. (Scholar)
• Sambin, G., 1976, “An Effective Fixed Point Theorem in Intuitionistic Diagonalizable Algebras (The Algebraization of the Theories Which Express Theor, IX),” Studia Logica 35: 345–361. (Scholar)
• Sambin, G., and S. Valentini, 1982, “The Modal Logic of Provability. The Sequential Approach,” Journal of Philosophical Logic, 11(3): 311–342. (Scholar)

Possible worlds semantics and topological semantics

• Abashidze, M., 1985, “Ordinal Completeness of the Gödel-Löb Modal System,” (in Russian) in Intensional Logics and the Logical Structure of Theories, Tbilisi: Metsniereba, pp. 49–73. (Scholar)
• Aiello, M., I. Pratt-Hartmann and J. van Benthem (eds.), 2007, Handbook of Spatial Logics, Berlin: Springer-Verlag. (Scholar)
• Beklemishev, L.D. 2009, “Ordinal Completeness of Bimodal Provability Logic GLB,” In International Tbilisi Symposium on Logic, Language, and Computation, Berlin: Springer-Verlag, pp. 1–15. (Scholar)
• Beklemishev, L.D., G. Bezhanishvili, and T. Icard, 2009, “On Topological Models of GLP,” in R. Schindler (ed.), Ways of Proof Theory (Ontos Mathematical Logic: Volume 2), Frankfurt: Ontos Verlag, pp. 133–153. (Scholar)
• van Benthem, J.F.A.K., 1979, “Syntactic Aspects of Modal Incompleteness Theorems,” Theoria, 45(2): 63–77. (Scholar)
• Blass, A., 1990, “Infinitary Combinatorics and Modal Logic,” Journal of Symbolic Logic, 55(2): 761–778. (Scholar)
• Esakia, L., 1981, “Diagonal Constructions, Löb’s Formula and Cantor’s Scattered Spaces,” (in Russian), in Studies in Logic and Semantics, Z. Mikeladze (ed.), Tbilisi: Metsniereba, pp. 128–143. (Scholar)
• –––, 2003, “Intuitionistic Logic and Modality via Topology,” Annals of Pure and Applied Logic, 127: 155–170. (Scholar)
• Goré, R., 2009, “Machine Checking Proof Theory: An Application of Logic to Logic,” In ICLA ’09: Proceedings of the 3rd Indian Conference on Logic and Its Applications, Berlin: Springer-Verlag, pp. 23–35. (Scholar)
• Hakli, R. and S. Negri, 2012, “Does the Deduction Theorem Fail for Modal Logic?,” Synthese 187(3): 849–867. (Scholar)
• Holliday, W.H. and Litak, T., 2019, “Complete Additivity and Modal Incompleteness,” The Review of Symbolic Logic, 12(3): 487–535. (Scholar)
• Icard, T.F. III, 2011, “A Topological Study of the Closed Fragment of GLP,” Journal of Logic and Computation, 21(4): 683–696; first published online 2009, doi:10.1093/logcom/exp043 (Scholar)
• Japaridze, G.K., 1986, The Modal Logical Means of Investigation of Provability, Thesis in Philosophy (in Russian), Moscow. (Scholar)
• McKinsey, J.C.C. and A. Tarski, 1944, “The Algebra of Topology,” Annals of Mathematics, 45: 141–191. (Scholar)
• Shillito, I., 2023, New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq, Ph.D. Thesis, Canberra: The Australian National University. (Scholar)
• Verbrugge, R., 2021, “Zero-One Laws for Provability Logic: Axiomatizing Validity in Almost All Models and Almost All Frames,” in L. Libkin (ed.), Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Rome: IEEE Press. (Scholar)

Provability and Peano Arithmetic

• Davis, M., 1958, Computability and Unsolvability, New York, McGraw-Hill; reprinted with an additional appendix, New York, Dover Publications 1983. (Scholar)
• Feferman, S., 1960, “Arithmetization of Metamathematics in a General Setting,” Fundamenta Mathematicae, 49(1): 35–92. (Scholar)
• Hájek, P. and P. Pudlák, 1993, Metamathematics of First-Order Arithmetic, Berlin: Springer-Verlag. (Scholar)
• Solovay, R.M., 1976, “Provability Interpretations of Modal Logic,” Israel Journal of Mathematics, 25: 287–304. (Scholar)

The scope of provability logic: boundaries

• Berarducci, A. and R. Verbrugge, 1993, “On the Provability Logic of Bounded Arithmetic,” Annals of Pure and Applied Logic, 61: 75–93. (Scholar)
• Buss, S.R., 1986, Bounded Arithmetic, Naples: Bibliopolis. (Scholar)
• de Jongh, D.H.J., M. Jumelet and F. Montagna, 1991, “On the Proof of Solovay’s Theorem,” Studia Logica, 50(1): 51–70. (Scholar)
• Parikh, R., 1971, “Existence and Feasibility in Arithmetic“, The Journal of Symbolic Logic, 36(3): 494–508. (Scholar)

Interpretability logic

• Areces, C., Hoogland, E. and de Jongh, D.H.J., 2001, “Interpolation, Definability and Fixed-points in Interpretability Logics“, in M. Zakharyaschev, K. Segerberg, M. de Rijke and H. Wansing (eds.), Advances in Modal Logic (Volume 2), Stanford: CSLI Publications, pp. 35–58. (Scholar)
• Berarducci, A., 1990, “The Interpretability Logic of Peano Arithmetic,” Journal of Symbolic Logic, 55: 1059–1089. (Scholar)
• Bílková, M., de Jongh, D. and Joosten, J.J., 2009, “Interpretability in PRA,” Annals of Pure and Applied Logic, 161(2): 128–138. (Scholar)
• de Jongh, D.H.J., and F. Veltman, 1990, “Provability Logics for Relative Interpretability,” in P.P. Petkov (ed.), Mathematical Logic: Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria, Boston: Plenum Press, pp. 31–42. (Scholar)
• de Jongh, D.H.J., and A. Visser, 1991, “Explicit Fixed Points in Interpretability Logic,” Studia Logica, 50(1): 39–49. (Scholar)
• Joosten, J.J., and Visser, A., 2000, “The Interpretability Logic of All Reasonable Arithmetical Theories,” Erkenntnis, 53(1-2): 3–26. (Scholar)
• Joosten, J.J., Mas Rovira, J., Mikec, L., and Vuković, M., forthcoming, “An Overview of Verbrugge Semantics, a.k.a. Generalised Veltman Semantics,” in N. Bezhanishvili, R. Iemhoff and F. Yang (eds.), Dick de Jongh on Intuitionistic and Provability Logic, Cham: Springer. (Scholar)
• Mikec, L. and Vuković, M., 2020, “Interpretability Logics and Generalised Veltman Semantics,” The Journal of Symbolic Logic, 85(2): 749–772. (Scholar)
• Montagna, F., 1987, “Provability in Finite Subtheories of PA,” Journal of Symbolic Logic, 52(2): 494–511. (Scholar)
• Shavrukov, V.Yu., 1988, “The Logic of Relative Interpretability over Peano Arithmetic,” Technical Report No. 5, Moscow: Steklov Mathematical Institute (in Russian). (Scholar)
• Švejdar, V., 1983, “Modal Analysis of Generalized Rosser Sentences,” Journal of Symbolic Logic, 48: 986–999. (Scholar)
• Visser, A., 1990, “Interpretability Logic,” in P.P. Petkov (ed.), Mathematical Logic: Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria, Boston: Plenum Press, pp. 175–209. (Scholar)
• –––, 1998, “An Overview of Interpretability Logic,” in M. Kracht et al. (eds.), Advances in Modal Logic (Volume 1), Stanford: CSLI Publications, pp. 307–359. (Scholar)

Propositional quantifiers

• Artemov, S.N. and L.D. Beklemishev, 1993, “On Propositional Quantifiers in Provability Logic,” Notre Dame Journal of Formal Logic, 34: 401–419. (Scholar)
• Shavrukov, V.Yu., 1997, “Undecidability in Diagonalizable Algebras,” Journal of Symbolic Logic, 62: 79–116. (Scholar)

Japaridze’s bimodal and polymodal provability logics

• Beklemishev, L.D., 2004, “Provability Algebras and Proof-Theoretic Ordinals, I,” Annals of Pure and Applied Logic, 128: 103–123. (Scholar)
• –––, 2010a, “Kripke Semantics for Provability Logic GLP,” Annals of Pure and Applied Logic, 161(6): 756–774. (Scholar)
• –––, 2010b, “On the Craig Interpolation and the Fixed Point Properties of GLP,” in S. Feferman et al. (eds.), Proofs, Categories and Computations (Tributes, 13), London: College Publications, pp. 49–60. (Scholar)
• –––, 2011a, “A Simplified Proof of Arithmetical Completeness Theorem for Provability Logic GLP,” Proceedings Steklov Institute of Mathematics, 274(1): 25–33. (Scholar)
• –––, 2011b, “Ordinal Completeness of Bimodal Provability Logic GLB,” in N. Bezhanishvili et al. (eds.), Logic, Language, and Computation, 8th International Tbilisi Symposium TbiLLC 2009 (Lecture Notes in Computer Science: Volume 6618), Heidelberg: Springer, pp. 1–15. (Scholar)
• Beklemishev, L.D., and D. Gabelaia, 2013, “Topological Completeness of the Provability Logic GLP,” Annals of Pure and Applied Logic, 164(12): 1201–1223. (Scholar)
• –––, 2014, “Topological Interpretations of Provability Logic,“ in G. Bezhanishvili (ed.), Leo Esakia on Duality in Modal and Intuitionistic Logics (Outstanding Contributions to Logic: Volume 4), Heidelberg: Springer, pp. 257–290. (Scholar)
• Beklemishev, L.D., J. Joosten and M. Vervoort, 2005, “A Finitary Treatment of the Closed Fragment of Japaridze’s Provability Logic,” Journal of Logic and Computation, 15(4): 447–463. (Scholar)
• Fernández-Duque, D. and J.J. Joosten, 2014, “Well-orders on the Transfinite Japaridze Algebra,” Logic Journal of the IGPL, 22 (6): 933–963. (Scholar)
• Fernández-Duque, D. and Joosten, J.J., 2018, “The Omega-Rule Interpretation of Transfinite Provability Logic,” Annals of Pure and Applied Logic, 169(4): 333–371. (Scholar)
• Ignatiev, K.N., 1993, “On Strong Provability Predicates and the Associated Modal Logics,” Journal of Symbolic Logic, 58: 249–290. (Scholar)
• Japaridze, G., 1988, “The Polymodal Provability Logic,” In Intensional Logics and the Logical Structure of Theories: Material from the Fourth Soviet-Finnish Symposium on Logic, Telavi, pp. 16–48. (Scholar)
• Pakhomov, F.N., 2014, “On the Complexity of the Closed Fragment of Japaridze’s Provability Logic,” Archive for Mathematical Logic, 53(7-8): 949–967. (Scholar)
• Shamkanov, D., 2020, “Global Neighbourhood Completeness of the Provability Logic GLP,” in N. Olivetti, R. Verbrugge, S. Negri, and G. Sandu (eds.), Proceedings Advances in Modal Logic (Volume 13), London: College Publications, pp. 581–595. (Scholar)

Predicate provability logic

• Artemov, S.N., 1985a, “Nonarithmeticity of Truth Predicate Logics of Provability,” Doklady Akademii Nauk SSSR, 284: 270–271 (in Russian); English translation in Soviet Mathematics Doklady, 32: 403–405. (Scholar)
• Borges, A.A. and Joosten, J.J., 2020, “Quantified Reflection Calculus with One Modality,” in N. Olivetti, R. Verbrugge, S. Negri, and G. Sandu (eds.), Proceedings Advances in Modal Logic (Volume 13), London: College Publications, pp. 13–32. (Scholar)
• –––, 2022, “An Escape from Vardanyan’s Theorem,” The Journal of Symbolic Logic, first online 13 May 2022. doi:10.1017/jsl.2022.38 (Scholar)
• Borges, A.A., 2022, “Towards a Coq Formalization of a Quantified Modal Logic,” in C. Benzmüller and J. Otten (eds.), Proceedings of the 4th Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022), CEUR Workshop Proceedings, pp. 13–27. (Scholar)
• McGee, V. and G. Boolos, 1987, “The Degree of the Set of Sentences of Predicate Provability Logic that are True under Every Interpretation,” Journal of Symbolic Logic, 52: 165–171. (Scholar)
• Montagna, F., 1984, “The Predicate Modal Logic of Provability,” Notre Dame Journal of Formal Logic, 25(2): 179–189. (Scholar)
• Rybakov, M., 2023, “Predicate Counterparts of Modal Logics of Provability: High Undecidability and Kripke Incompleteness,” Logic Journal of the IGPL, first online 28 February 2023. doi:10.1093/jigpal/jzad002 (Scholar)
• Vardanyan, V.A., 1986, “Arithmetic Complexiy of Predicate Logics of Provability and their Fragments,” Doklady Akademii Nauk SSSR, 288: 11–14 (in Russian); English translation in Soviet Mathematics Doklady, 33: 569–572. (Scholar)
• Visser, A. and M. de Jonge, 2006, “No Escape from Vardanyan’s Theorem,” Archive of Mathematical Logic, 45(5): 539–554. (Scholar)

Other generalizations

• Aguilera, J.P. and Fernández-Duque, D., 2017, “Strong Completeness of Provability Logic for Ordinal Spaces,” The Journal of Symbolic Logic, 82(2): 608–628. (Scholar)
• Alberucci, L., and A. Facchini, 2009, “On Modal μ-Calculus and Gödel-Löb logic,” Studia Logica, 91: 145–169. (Scholar)
• Ardeshir, M. and Mojtahedi, M., 2018, “The \(Σ_1\)-Provability Logic of HA,” Annals of Pure and Applied Logic, 169(10): 997–1043. (Scholar)
• Artemov, S.N., 1985b,“On Modal Logics Axiomatizing Provability,” Izvestiya Akadademii Nauk SSSR, Seriya Matematicheskaya, 49(6): 1123–1154 (in Russian); English translation in Mathematics of the USSR–Izvestiya, 27(3): 402–429. (Scholar)
• –––, 1994, “Logic of Proofs,” Annals of Pure and Applied Logic, 67(2): 29–59. (Scholar)
• –––, 2001, “Explicit Provability and Constructive Semantics,” Bulletin of Symbolic Logic, 7: 1–36. (Scholar)
• Artemov, S.N. and R. Iemhoff, 2007, “The Basic Intuitionistic Logic of Proofs,” Journal of Symbolic Logic, 72(2): 439–451. (Scholar)
• Artemov, S.N. and F. Montagna, 1994, “On First-order Theories with Provability Operator,” Journal of Symbolic Logic, 59(4): 1139–1153. (Scholar)
• Artemov, S.N. and Nogina, E., 2005, “Introducing Justification into Epistemic Logic,” Journal of Logic and Computation, 15(6): 1059–1073. (Scholar)
• Beklemishev, L.D., 1989, “On the Classification of Propositional Provability Logics,” Izvestiya Akademii Nauk SSSR, Seriya Matematicheskaya., 53(5): 915–943 (in Russian); English translation in Mathematics of the USSR–Izvestiya, 35 (1990) 247–275. (Scholar)
• –––, 1994, “On Bimodal Logics of Provability,” Annals of Pure and Applied Logic, 68: 115–160. (Scholar)
• –––, 1996, “Bimodal Logics for Extensions of Arithmetical Theories,” Journal of Symbolic Logic, 61: 91–124. (Scholar)
• –––, 1999, “Parameter-Free Induction and Provably Total Computable Functions,” Theoretical Computer Science, 224: 13–33. (Scholar)
• –––, 2003, “Proof-theoretic Analysis by Iterated Reflection,” Archive for Mathematical Logic, 6(42): 515–552. (Scholar)
• –––, 2005, “Reflection Principles and Provability Algebras in Formal Arithmetic,” Uspekhi Matematicheskikh Nauk, 60(2): 3–78. (in Russian); English translation in: Russian Mathematical Surveys, 60(2): 197–268. (Scholar)
• –––, 2006, “The Worm Principle,” in Lecture Notes in Logic 27. Logic Colloquium ’02, Z. Chatzidakis, P. Koepke, and W. Pohlers (eds.), Natick (MA): AK Peters, pp. 75–95. (Scholar)
• –––, 2012, “Calibrating Provability Logic: From Modal Logic to Reflection Calculus,” in T. Bolander, T. Braüner, S. Ghilardi, and L. Moss (eds.), Advances in Modal Logic (Volume 9), London: College Publications, pp. 89–94. (Scholar)
• –––, 2014, “Positive Provability Logic for Uniform Reflection Principles,” Annals of Pure and Applied Logic, 165 (1): 82–105. (Scholar)
• –––, 2018a, “A Note on Strictly Positive Logics and Word Rewriting Systems,” in S. Odintsov (ed.), Larisa Maksimova on Implication, Interpolation, and Definability (Outstanding Contributions to Logic: Volume 15), Cham: Springer, pp.61–70. (Scholar)
• –––, 2018b, “Reflection Calculus and Conservativity Spectra “, Russian Mathematical Surveys, 73(4): 569–613. (Scholar)
• Beklemishev, L.D., D. Fernández-Duque, and J.J. Joosten, 2014, “On Provability Logics with Linearly Ordered Modalities,” Studia Logica, 102(3): 541–566. (Scholar)
• Beklemishev, L. D., and Pakhomov, F. N., 2022, “Reflection Algebras and Conservation Results for Theories of Iterated Truth,” Annals of Pure and Applied Logic, 173(5): 103093. (Scholar)
• Beklemishev, L.D., M. Pentus and N. Vereshchagin, 1999, Provability, Complexity, Grammars, American Mathematical Society Translations (Series 2, Volume 192). (Scholar)
• Beklemishev, L.D. and A. Visser, 2006, “Problems in the Logic of Provability,” in D.M. Gabbay, S.S. Goncharov and M. Zakharyashev (eds.), Mathematical Problems from Applied Logic I: Logics for the XXIst Century (International Mathematical Series, Volume 4), New York: Springer, pp. 77–136. (Scholar)
• van Benthem, J., 2006, “Modal Frame Correspondences and Fixed-points,” Studia Logica, 83(1-3): 133–155. (Scholar)
• Bernardi, C. and D’Aquino, P., 1988, “Topological Duality for Diagonalizable Algebras“, Notre Dame Journal of Formal Logic, 29(3): 345–364. (Scholar)
• Carbone, A. and Montagna, F., 1990, “Much Shorter Proofs: A Bimodal Investigation,” Mathematical Logic Quarterly, 36(1): 47–66. (Scholar)
• Carlson, T., 1986, “Modal Logics with Several Operators and Provability Interpretations,” Israel Journal of Mathematics, 54(1): 14–24. (Scholar)
• Dashkov, E.V., 2012, “On the Positive Fragment of the Polymodal Provability Logic GLP,” Mathematical Notes, 91 (3): 318–333. (Scholar)
• Dyckhoff, R and Negri, S., 2016, A Cut-free Sequent System for Grzegorczyk Logic, with an Application to the Gödel–McKinsey–Tarski Embedding, Journal of Logic and Computation, 26: 169–187. (Scholar)
• Fernández-Duque, D., 2014, “The Polytopologies of Transfinite Provability Logic,“ Archive for Mathematical Logic, 53(3-4): 385–431. (Scholar)
• Fernández-Duque, D. and J.J. Joosten, 2013a, “Hyperations, Veblen Progressions, and Transfinite Iteration of Ordinal Functions,” Annals of Pure and Applied Logic 164 (7-8): 785–801, [available online]. (Scholar)
• Fernández-Duque, D. and J.J. Joosten, 2013b, “Models of Transfinite Provability Logic,” Journal of Symbolic Logic, 78(2): 543–561, [available online]. (Scholar)
• van der Giessen, I., 2023, “Admissible Rules for Six Intuitionistic Modal Logics,” Annals of Pure and Applied Logic, 174(4): 103233. (Scholar)
• van der Giessen, I. and Iemhoff, R., 2021, “Sequent Calculi for Intuitionistic Gödel–Löb Logic,” Notre Dame Journal of Formal Logic, 62(2): 221–246. (Scholar)
• Goré, R and Ramanayake, R., 2014, “Cut-elimination for Weak Grzegorczyk Logic Go,” Studia Logica, 102(1): 1–27. (Scholar)
• Guaspari, D. and R.M. Solovay, 1979, “Rosser Sentences,” Annals of Mathematical Logic, 16: 81–99. (Scholar)
• Iemhoff, R., 2000, “A Modal Analysis of some Principles of the Provability Logic of Heyting Arithmetic,” in Advances in Modal Logic (Volume 2), M. Zakharyashev et al. (eds.), Stanford: CSLI Publications, pp. 319–354. (Scholar)
• –––, 2001, “On the Admissible Rules of Intuitionistic Propositional Logic,” Journal of Symbolic Logic, 66: 281–294. (Scholar)
• –––, 2003, “Preservativity Logic: An Analogue of Interpretability Logic for Constructive Theories,” Mathematical Logic Quarterly, 49(3): 1–21. (Scholar)
• Iemhoff, R., de Jongh, D. and Zhou, C., 2005, “Properties of Intuitionistic Provability and Preservativity Logics,” Logic Journal of the IGPL, 13(6): 615–636. (Scholar)
• Joosten, J.J., 2021, “Münchhausen Provability,” The Journal of Symbolic Logic, 86(3): 1006–1034. (Scholar)
• Kuznets, R. and Studer, T., 2019, Logics of Proofs and Justifications, London: College Publications. (Scholar)
• Lindström, P., 1994, “The Modal Logic of Parikh Provability,” Filosofiska Meddelanden, Gröna Serien, Gothenburg: Göteborgs Universitetet. (Scholar)
• Lindström, P., 2006, “On Parikh Provability: An Exercise in Modal Logic,” in H. Lagerlund, S. Lindström, and R. Sliwinski (eds.), Modality Matters: Twenty-Five Essays in Honour of Krister Segerberg, Uppsala: Uppsala Philosophical Studies (Volume 53), pp. 53–287. (Scholar)
• Litak, L., 2007, “The Non-Reflexive Counterpart of Grz,” Bulletin of the Section of Logic, 36(3–4): 195–208. (Scholar)
• Litak, T. and Visser, A., 2018, “Lewis Meets Brouwer: Constructive Strict Implication,” Indagationes Mathematicae, 29(1): 36–90. (Scholar)
• –––, forthcoming, “Lewisian Fixed Points I: Two Incomparable Constructions,” in N. Bezhanishvili, R. Iemhoff and F. Yang (eds.), Dick de Jongh on Intuitionistic and Provability Logic, Cham: Springer. (Scholar)
• Maksimova, L.L., 2014, “The Lyndon Property and Uniform Interpolation over the Grzegorczyk Logic,” Siberian Mathematical Journal, 55(1): 118–124. (Scholar)
• Mares, E.D., 2000, “The Incompleteness of RGL,” Studia Logica, 65: 315–322. (Scholar)
• Mojtahedi, M., forthcoming, “The \(Σ_1\)-provability logic of HA revisited,” in N. Bezhanishvili, R. Iemhoff and F. Yang (eds.), Dick de Jongh on Intuitionistic and Provability Logic, Cham: Springer. (Scholar)
• Montagna, F.,1978, “On the algebraization of a Feferman’s predicate,” Studia Logica, 37(3): 221–236. (Scholar)
• –––, 1979, “On the Diagonalizable Algebra of Peano Arithmetic,” Bollettino della Unione Matematica Italiana, B(5), 16: 795–812. (Scholar)
• –––, 1980a, “Interpretations of the First-order Theory of Diagonalizable Algebras in Peano Arithmetic,” Studia Logica, 39: 347–354. (Scholar)
• –––, 1980b, “Undecidability of the First-order Theory of Diagonalizable Algebras, ” Studia Logica, 39: 355–359. (Scholar)
• –––, 1992, “Polynomially and Superexponentially Shorter Proofs in Fragments of Arithmetic,” Journal of Symbolic Logic, 57: 844–863. (Scholar)
• Pakhomov, F.N., 2012, “Undecidability of the Elementary Theory of the Semilattice of GLP-words,” Sbornik: Mathematics, 203(8): 1211. (Scholar)
• Pakhomov, F.N., 2015, “On Elementary Theories of Ordinal Notation Systems Based on Reflection Principles,” Proceedings of the Steklov Institute of Mathematics, 289: 194–212. (Scholar)
• Savateev, Y., and Shamkanov, D., 2019, “Cut Elimination for the Weak Modal Grzegorczyk Logic via Non-well-founded Proofs,” in R. Iemhoff, M. Moortgat, M. and R. de Queiroz (eds.), Proceedings of WoLLIC 2019, Heidelberg: Springer, pp. 569–583. (Scholar)
• –––, 2021, “Non-well-founded Proofs for the Grzegorczyk Modal Logic,” The Review of Symbolic Logic, 14(1): 22–50. (Scholar)
• Shamkanov, D.S., 2016, “A Realization Theorem for the Gödel–Löb Provability Logic,” Sbornik: Mathematics, 207(9): 1344–1360. (Scholar)
• Shapirovsky, I., 2008, “PSPACE-decidability of Japaridze’s Polymodal Logic,” Advances in Modal Logic, 7: 289–304. (Scholar)
• Shavrukov, V.Yu., 1993a, “A Note on the Diagonalizable Algebras of PA and ZF,” Annals of Pure and Applied Logic, 61: 161–173. (Scholar)
• –––, 1993b, “Subalgebras of Diagonalizable Algebras of Theories Containing Arithmetic,” Dissertationes Mathematicae, 323. (Scholar)
• –––, 1994, “A Smart Child of Peano’s,” Notre Dame Journal of Formal Logic, 35(2): 161–185. (Scholar)
• Troelstra, A.S., 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Berlin: Springer-Verlag. (Scholar)
• Visser, A., 1980, Aspects of Diagonalization and Provability, Ph.D. Thesis, Utrecht: University of Utrecht. (Scholar)
• –––, 1982, “On the Completeness Principle: A Study of Provability in Heyting’s Arithmetic and Extensions,” Annals of Mathematical Logic, 22(3): 263–295. (Scholar)
• –––, 1989, “Peano’s Smart Children: A Provability Logical Study of Systems with Built-in Consistency,” Notre Dame Journal of Formal Logic, 30(2): 161–196. (Scholar)
• –––, 1995, “A Course on Bimodal Provability Logic,” Annals of Pure and Applied Logic, 73(1): 109–142. (Scholar)
• –––, 1999, “Rules and Arithmetics,” Notre Dame Journal of Formal Logic, 40(1): 116–140. (Scholar)
• –––, 2002, “Substitutions of \(\Sigma_1\) Sentences: Explorations between Intuitionistic Propositional Logic and Intuitionistic Arithmetic,” Annals of Pure and Applied Logic, 114: 227–271. (Scholar)
• –––, 2005, “Löb’s Logic Meets the μ-Calculus,” in A. Middeldorp, V. van Oostrom, F. van Raamsdonk and R. de Vrijer (eds.), Processes, Terms and Cycles: Steps on the Road to Infinity, Berlin: Springer, pp. 14–25.
• –––, 2008, “Closed Fragments of Provability Logics of Constructive Theories,” Journal of Symbolic Logic, 73: 1081–1096. (Scholar)
• –––, 2016, “The Second Incompleteness Theorem: Reflections and Ruminations,” in L. Horsten and P. Welch (eds.), Gödel’s Disjunction: The Scope and Limits of Mathematical Knowledge, Oxford: Oxford University Press, pp. 67–91. (Scholar)
• –––, 2020, “Another Look at the Second Incompleteness Theorem,” The Review of Symbolic Logic, 13(2): 269–295. (Scholar)
• Visser, A. and Zoethout, J., 2019, “Provability Logic and the Completeness Principle,” Annals of Pure and Applied Logic, 170(6): 718–753. (Scholar)
• Yavorskaya, T., 2001, “Logic of Proofs and Provability,” Annals of Pure and Applied Logic, 113(1-3): 345–372. (Scholar)
• Zambella, D., 1994, “Shavrukov’s Theorem on the Subalgebras of Diagonalizable Algebras for Theories Containing \(I \Delta_0 + \exp\),” Notre Dame Journal of Formal Logic, 35: 147–157. (Scholar)

Philosophical significance

• Crocco, G., 2019, “Informal and Absolute Proofs: Some Remarks from a Gödelian Perspective,” Topoi, 38: 561–575. (Scholar)
• Davis, M., 1990, “Is Mathematical Insight Algorithmic?,” Commentary on Roger Penrose, The Emperor’s New Mind, Behavioral and Brain Sciences, 13: 659–660. (Scholar)
• –––, 1993, “How Subtle is Gödel’s Theorem? More on Roger Penrose” (Commentary on Roger Penrose, The Emperor’s New Mind), Behavioral and Brain Sciences, 16: 611–612. (Scholar)
• Egré, P., 2005, “The Knower Paradox in the Light of Provability Interpretations of Modal Logics,” Journal of Logic, Language, and Information, 14(1): 13–48. (Scholar)
• Franzén, T., 2005, Gödel’s Theorem: An Incomplete Guide to its Use and Abuse, Boca Raton, Florida: CRC Press.
• Gödel, K., 1946, “Remarks Before the Princeton Bicentennial Conference on Problems in Mathematics,” reprinted in S. Feferman et al. (eds.), Kurt Gödel Collected Works, Volume II: Publications 1938–1975, New York, Oxford: Oxford University Press, 1990, pp. 150–153. (Scholar)
• Kaplan, D. and R. Montague, 1960, “A Paradox Regained,” Notre Dame Journal of Formal Logic, 1(3): 79–90. (Scholar)
• Kennedy, J., 2014, “Gödel’s 1946 Princeton Bicentennial Lecture: An Appreciation,” in J. Kennedy (ed.), Interpreting Gödel: Critical Essays, Cambridge: Cambridh=ge University Press, pp.109–130.
• Koellner, P., 2016, “Gödel’s Disjunction,” in L. Horsten and P. Welch (eds.), Gödel’s Disjunction: The Scope and Limits of Mathematical Knowledge, Oxford: Oxford University Press, pp. 148–188.
• Kreisel, G., 1967, “Informal Rigour and Completeness Proofs,” in I. Lakatos (ed.), Problems in the Philosophy of Mathematics, Amsterdam: North-Holland, pp. 138–157. (Scholar)
• Leach-Krouse, G.E., 2013, “Conceptions of Absolute Provability,” Ph.D. Thesis, Note Dame: Notre Dame University. (Scholar)
• Leach-Krouse, G.E., 2016, “Provability, Mechanism, and the Diagonal Problem,” in L. Horsten and P. Welch (eds.), Gödel’s Disjunction: The Scope and Limits of Mathematical Knowledge, Oxford: Oxford University Press, pp. 211–242. (Scholar)
• Lindström, P, 2001, “Penrose’s New Argument,” Journal of Philosophical Logic, 30: 241–250. (Scholar)
• Montague, R., 1963, “Syntactical Treatments of Modality, with Corollaries on Reflection Principles and Finite Axiomatizability,” Acta Philosophica Fennica, 16: 153–67. (Scholar)
• Quine, W.V., 1966, “Necessary Truth,” in Quine, W.V., The Ways of Paradox and Other Essays, New York: Random House, pp. 48–56. (Scholar)
• –––, 1953, “Three Grades of Modal Involvement,” in Proceedings of the 11th International Congress of Philosophy, Amsterdam: North-Holland, pp. 65-81; reprinted in W.V. Quine, The Ways of Paradox and Other Essays, New York: Random House, 1966, pp. 156–174. (Scholar)
• de Vos, M., Verbrugge, R., and Kooi, B., 2023, “Solutions to the Knower Paradox in the Light of Haack’s Criteria,” Journal of Philosophical Logic, 52: 1101–1132. (Scholar)
• Williamson, T., 2016, “Absolute Provability and Safe Knowledge of Axioms,” in L. Horsten and P. Welch (eds.), Gödel’s Disjunction: The Scope and Limits of Mathematical Knowledge, pp. 243–253. (Scholar)