1. Ardeshir, Mohammad and S. Mojtaba Mojtahedi, Mojtaba S. 2014. “The Σ 01 Provability Logic of HA”. Annals of Pure and Applied Logic 169 (10): 997-1043. DOI: 10.1016/j.apal.2014.07.005
2. Artemov, Sergei and G. Japaridze Giorgie. 1990.“Finite Kripke models and predicate logics of provability”. The Journal of Symbolic Logic 55 (3): 1090-1098. DOI: 10.2307/2274475
3. Artemov, Sergei and Beklemishev, Lev D. 2005. “Provability Logic”. In Gabbay, D., Guenthner, F. (editors) Handbook of Philosophical Logic, 2nd Edition. Handbook of Philosophical Logic, vol 13. Dordrecht: Springer. DOI: 10.1007/1-4020-3521-7_3
4. Avigad, Jeremy and Feferman, Solomon. 1998. “Gödel’s Functional (“Dialectica”) Interpreta- tion”. S. R. Buss (editor) Handbook of Proof Theory 337-405. Amsterdam: Elsevier DOI: 10.2307/420972
5. Beklemishev, Lev. 1992. “Independent enumerations of theories and recursive progres- sions”. Siberian Mathematical Journal 33: 760-783
6. Beklemishev, Lev. 1995. “Iterated local reflection versus iterated consistency”. Annals of Pure and Applied Logic 75 (1-2): 25-48. DOI: 10.1016/0168-0072(95)00007-4
7. Beklemishev, Lev. 2014. “Positive provability logic for uniform reflection principles”. Annals of Pure and Applied Logic, 165 (1) : 82-105 DOI: 10.1016/j.apal.2013.07.006
8. Beklemishev, Lev and Flaminio, Tommaso. 2016. “Franco Montagna’s Work on Provability Logic and Many-valued Logic”. Studia Logica 104: 1-46. DOI: 10.1007/s11225-016-9654-3
9. Beckmann, Arnold and Pollett, Chris and Buss, Samuel R. 2003. “Ordinal notations and well- orderings in bounded arithmetic”. Annals of Pure and Applied Logic 120, (1–3): 197-223 DOI: 10.1016/s0168-0072(02)00066-0
10. Bernardi, Claudio. 1975. “The fixed-point theorem for diagonalizable algebras” . Studia Logica 34 (3): 239-251. DOI: 10.1007/BF02092015
11. Bernardi, Claudio and Sorbi, Andrea. 1983. “Classifying positive equivalence relations” . The Journal of Symbolic Logic 48 (3): 529-538. DOI: 10.2307/2273443
12. Bezboruah, Amala and Shepherdson, John C. 1976. “Gödel’s Second incompleteness theorem for Q” . The Journal of Symbolic Logic 41(2): 503-512. DOI: 10.2307/2272251
13. Boolos, George S. 2008. The Logic of Provability. Cambridge: Cambridge University Press. DOI: 10.2307/2275893
14. Boolos, George and V. McGee, Van. 1987. “The degree of the set of sentences of predicate provability logic that are true under every interpretation”. The Journal of Symbolic Logic 52: 165-171. DOI: 10.2307/2213924
15. Buss, Samuel R. 1986. Bounded Arithmetic. Napoli: Bibliopolis.
16. Crosilla, Laura. 2017. “Predicativity and Feferman” . In G. Jäger and W. Sieg (editors) Feferman on Foundations: Logic, Mathematics and Philosophy 423-447. Cham: Springer. DOI: 10.1007/978-3-319-63334-3_15
17. De Almeida Borges, Ana and Joosten, Joost. 2013. “An escape from Vardanyan’s theorem”. The Journal of Symbolic Logic 88 (4): 1613-1638. DOI: 10.1017/jsl.2022.38
18. De Jongh, Dick. 1969. “The maximality of the intuitionistic predicate calculus with respect to Heyting’s arithmetic.”(typed manuscript) Amsterdam University.
19. De Jongh, Dick, and Japaridze, Giorgi. 1998. “The Logic of Provability” . In S. R. Buss (editor) Handbook of Proof Theory 475-546. Amsterdam: Elsevier. DOI: 10.2307/420974
20. De Jongh, Dick, Marc Jumelet, and Franco Montagna. 1991. “On the Proof of Solovay’s Theorem” . Studia Logica 50 (1): 51-69. DOI: 10.1007/BF00370387
21. De Jongh, Dick, and Verbrugge, Rineke and Visser, Albert. 2011. “Intermediate logics and the de Jongh property”. Archive for Mathematical Logic 50: 197-213. DOI: 10.1007/s00153-010-0209-4
22. Detlefsen, Michael. 1979. “On interpreting Gödel Second Theorem” . Journal of Philosophical Logic 8: 297-313. DOI: 10.1007/BF00258433
23. Detlefsen, Michael. 1986. Hilbert’s Program. Dordrecht: Reidel. DOI: 10.2307/2026690
24. Detlefsen, Michael. 2001. “What does Gödel’s second theorem say?”. Philosophia Mathematica 9 (1): 37-71. DOI: 10.1093/philmat/9.1.37
25. Fitting, Melvin and Mendelsohn, Richard. 1998. First Order Modal Logic, Dordrecht: Kluwer.
26. Friedman, Harvey. 1973. “Some applications of Kleene’s methods for intuitionistic systems.”In Cambridge Summer School in Mathematical Logic, edited by A.R.D. Mathias and A.R.D. and H. Rogers: 113–170. Berlin: Springer. DOI: 10.1007/BFB0066773
27. Gentzen, Gerhard. 1938. “Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie” . Forschungen zur Logik und zur Grundlegung der exacten Wissenschaften, Neue Folge 4: 19-44 (reprinted in M. E. Szabo (editor), Collected papers of Gerhard Gentzen 1969. Amsterdam: North Holland 252–286).
28. Gentzen, Gerhard. 1943. “Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der trans- finiten Induktion in der reinen Zahlentheorie” . Mathematische Annalen, 119 (1): 140–161 (reprinted in M. E. Szabo (editor), Collected papers of Gerhard Gentzen 1969. Amsterdam: North Holland 287-308).
29. Feferman, Solomon. 1960. “Arithmetization of metamathematics in a general setting” . Fun- damenta Mathematicae 49 (1): 35-92.
30. Feferman, Solomon. 1962. “Transfinite Recursive Progressions of Axiomatic Theories”. The Journal of Symbolic Logic 27 (3): 259-316. DOI: 10.2307/2964649
31. Feferman, Solomon. 1964. “Systems of predicative analysis”. The Journal of Symbolic Logic 29: 1-30. DOI: 10.2307/2269764
32. Feferman, Solomon. 2006. “Are There Absolutely Unsolvable Problems?Gödel’s Dichotomy”. Philosophia Mathematica (III) 14: 134-152. DOI: 10.1093/philmat/nkj003
33. Franzen, Torkel. 2003. Inexhaustibility: A Non-Exhaustive Treatment. Lecture Notes in Logic 16. Cambridge: Cambridge University Press . DOI: 10.1201/9780367807078
34. Franzen, Torkel. 2004. “Transfinite progressions: a second look at completeness”. Bulletin of Symbolic Logic 10 (2004): 367-389. DOI: 10.2178/bsl/1102022662
35. Franzen, Torkel. 2005. Gödel’s theorem: an incomplete guide to its use and abuse (1st ed.). Wellesley: A. K. Peters. DOI: 10.1201/9780429295225
36. Ghilardi, Silvio. 1999.“Unification in Intuitionistic Logic” . The Journal of Symbolic Logic 64: 859-880. DOI: 10.2307/2586506
37. Girard, Jean Yves. 1987. Proof-theory and logical complexity I. Napoli: Bibliopolis. DOI: 10.1017/s0022481200041335
38. Goré, Rajeev and Ramanayake, Revantha. 2012. “Valentini’s cut-elimination for provability logic resolved” . The Review of Symbolic 5 (2): 212-238. DOI: 10.1017/S1755020311000323
39. Hájek, Peter and Pudlák, Pavel. 1993. Metamathematics of first order arithmetic. Berlin: Springer. DOI: 10.1007/978-3-662-22156-3
40. Hao, Yunge and Tourlakis, George. 2021.“An arithmetically complete pred- icate modal logic”. Bulletin of the Section of Logic. Łódź University. https://czasopisma.uni.lodz.pl/bulletin/article/view/8441 DOI: 10.18778/0138-0680.2021.18
41. Hilbert, David and Bernays, Paul. 1939. Grundlagen der Mathematik II. Berlin: Springer.
42. Kleene, Stephen C. 1952. Introduction to Metamathematics. Amsterdam: North-Holland.
43. Kreisel, Georg. 1960. “Ordinal Logics and the Characterization of Informal Concepts of Proof”. In Todd J. A. (editor), Proceedings of the International Congress of Mathematicians 289- 299. Edinburgh, Cambridge: Cambridge University Press.
44. Jech, Thomas. 1978. Set theory. Cambridge M.: Academic Press.
45. Jeroslow, Robert G. 1975. “Experimental logics and ∆ 2 theories” . Journal of Philosophical Logic 4 (3): 253-267.
46. Löb, Martin. 1955. “Solution of a Problem of Leon Henkin”. The Journal of Symbolic Logic 20 (2): 115-118. DOI: 10.2307/2266895
47. Mancosu, Paolo and Galvan, Sergio and Zach, Richard. 2021. An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs. Oxford: Oxford University Press. DOI: 10.1093/oso/9780192895936.001.0001
48. Montagna, Franco. 1978. “On the algebraization of a Feferman’s predicate” . Studia Logica 37: 221–236 DOI: 10.1007/BF00136037
49. Montagna, Franco. 1979. “On the diagonalizable algebra of Peano arithmetic.” Bollettino della Unione Matematica Italiana B (5), 16: 795-812. DOI: 10.1007/BF01205703
50. Montagna, F. 1987. “Provability in finite subtheories of PA” . The Journal of Symbolic Logic 52(2): 494–511 DOI: 10.2307/2274396
51. Poggiolesi, Francesca. 2009.“A purely syntactic and cut-free sequent calculus for the modal logic of provability”. Review of Symbolic Logic 2 (4): 593-611. DOI: 10.1017/s1755020309990244
52. Pudlák, Pavel. 1996. “On the lengths of proofs of consistency.” Collegium Logicum, annals of the Kurt Gödel Society 2 : 65-86. DOI: 10.5817/CL2014125
53. Rathjen, Michael. 2006. “The art of ordinal analysis.” In M. Sanz Solé, J. Soria de Diego, J. L. Varona Malumbres, J. Verdera (editors) Proceedings of the International Congress of Mathematicians 2 45-70. Berlin: EMS Press. DOI: 10.4171/022-2/3
54. Sambin, Giovanni. 1976. “An effective fixed-point theorem in intuitionistic diagonalizable algebras”. Studia Logica 35: 345-361. DOI: 10.1007/bf02123402
55. Sasaki, Katsumi. 2001. Löb’s axiom and cut-elimination theorem. ILLC Dissertation Series DS-2001-07, Amsterdam.
56. Schütte, Kurt. 1960. Beweistheorie, (Grundlehren der mathematischen Wissenschaften, 103), Berlin: Springer.
57. Schütte, Kurt. 1964. “Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik”. Archiv für Mathematische Logik und Grundlagenforschung 7(1–2): 45–60.
58. Schütte, Kurt. 1965. “Predicative Well-Orderings”. In J.N. Crossley and M.A.E. Dummett (editors), Formal Systems and Recursive Functions 280–303. Amsterdam: North Holland.
59. Schwichtenberg, Helmut. 1977. “Proof Theory: Some Applications of Cut-Elimination ”. In Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics 90, edited by J. Barwise 867-895. Amsterdam: Elsevier DOI: 10.1016/S0049-237X(08)71124-8
60. Smorynski, Craig. 1973. “Applications of Kripke models” . In Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, edited by A. S. Troelstra 324-391. Berlin: Springer
61. Solovay, Robert M. 1976. “Provability Interpretations of Modal Logic” . Israel Journal of Mathematics 25: 287-304. DOI: 10.1007/BF02757006
62. Sommer, Richard. 1990. Transfnite induction and hierarchies generated by transfinite recur- sion within Peano arithmetic, Ph.D. Thesis, U.C. Berkeley.
63. Takeuti, Gaisi. 1987. Proof Theory. Amsterdam: North Holland (Reprint Courier Corporation, 2013).
64. Sommer, Richard. 1995. “Transfinite induction within Peano arithmetic ” . Annals of Pure and Applied Logic 76 (3): 231-289. DOI: 10.1016/0168-0072(95)00029-G
65. Troelstra, Anne S. and Schwichtenberg, Helmut. 2000. Basic proof theory. Cambridge: Cam- bridge University Press.
66. Troelstra, Anne S. and Van Dalen, Dirk. 1988. Constructivism In Mathematics. An Introduc- tion. I and II. Amsterdam: North Holland.
67. Turing, Alan M. 1937. “Computability and lambda definability”. The Journal of Symbolic Logic 2 (4): 153-163.
68. Turing, Alan. 1939. “Systems of logic based on ordinals.”Proc. London Mathematical Society 2: 161-228.
69. Ursini, Aldo. 1979.“Intuitionistic diagonalizable algebras” . Algebra Universalis 9: 229-237. DOI: 10.1007/BF02488034
70. Verbrugge, Rineke and Berarducci, Alessandro. “On the provability logic of bounded arithmetic”. Annals of Pure and Applied Logic 61 (1-2): 75-93. DOI: 10.1016/0168-0072(93)90199-n
71. Visser, Albert. 1989. “Peano’s smart children. A provability logical study of systems with built-in consistency” . Notre Dame Journal of Formal Logic 30: 161-196. DOI: 10.1305/ndjfl/1093635077
72. Valentini, Silvio. 1983.“The modal logic of provability: Cut-elimination” . Journal of Philo- sophical Logic 12: 471-476. DOI: 10.1007/BF00249262
73. Van Dalen, Dirk. 2001. “Intuitionistic Logic”. In L. Goble (editor). The Blackwell Guide to Philosophical Logic 224–257. Malden, Mass.: Wiley-Blackwell. DOI: 10.1002/9781405164801.ch11
74. Visser, Albert and De Jonge, Maartje. 2006. “No Escape from Vardanyan’s theorem”. Archive for Mathematical Logic 45: 539–554. DOI: 10.1007/s00153-006-0328-0
75. Von Plato, Jan. 2014. “The Development of Proof Theory” . Stanford Encyclopedia of Philos- ophy https://plato.stanford.edu/entries/proof-theory-development/
76. Weaver, Nik.2005.“Predicativity beyond Γ 0 ”. arXiv:math/0509244.
77. Yavorsky, Rostislav. 2002.“On arithmetical completeness of first-order logics of provability”. In F. Wolter, H. Wansing, M. de Rijke and M. Zakharyaschev (editors) Advances in Modal Logic 3 1–16. Singapore: World Scientific Publishing, DOI: 10.1142/9789812776471_0001
78. Visser, Albert and De Jongh, Dick and Van Benthem, Johannes and Renardel de Lavalette, Jean Gerard. 1995. “NNIL, A study in intuitionistic propositional logic” In Modal Logic and Process Algebra, edited by A. Ponse M. de Rijke Y. Venema. Stanford: CSLI.
79. Zoethout, Jetze and Visser, Albert. 2019. “Provability Logic and the Completeness Principle”. Annals of Pure and Applied Logic 6: 718-753. DOI: 10.1016/j.apal.2019.02.001

Chapter Information

Bibliographic Information