1. The evolution of this methodological perspective to formal axiomatics is described in Appendix A.

2. The term “finit” is used without much explanation; one is led to think that it was a thoroughly familiar one. Indeed, the 1919 article by Bernstein calls “finit” all considerations that have a constructive feature, from Kronecker through Poincaré to Brouwer. It is obviously used also to emphasize the contrast with “transfinit”. The term was also prominently used by Weyl in Das Kontinuum (1918).

3. Primitive recursion is given by the equations

and

where S is the successor function and g, h are previously defined primitive recursive functions. The class of primitive recursive functions is obtained from the constant 0 function, S and the projection functions \(P^i_n(x_1,\ldots,x_n)=x_i\) by closure under composition and the above recursion schema.

The language of PRA has the equality symbol = and function symbols for all primitive recursive functions. The axioms of PRA consist of the defining equations for the primitive recursive functions and the induction scheme \[ {A(0)} \land {\forall x[A(x)\to A(Sx)]\to \forall x A(x)} \] for atomic formulas \(A(x)\). Note that atomic formulas \(A(x)\) of PRA are of the form \(t_1(x)=t_2(x)\) for terms \(t_1(x)\) and \(t_2(x)\).

4. Many contemporary writers consider Hilbert 1922 as the beginning of Hilbert’s finitist program; see, for example, Franks 2009. However, Hilbert’s paper is split into two parts, according to the editors of the third volume of Hilbert’s Gesammelte Abhandlungen in which it was republished: the first part stems from the older considerations that go back to the Heidelberg talk (Hilbert 1905); see appendix A.3. In the second part a new direction is taken that involves a significantly expanded formal theory; however, the theory is by design “constructive”, as negation is applied only to equations. A consistency proof for this expanded theory is not presented and could not be obtained by the old techniques; the result, when suitably restricted as the Editors of the volume suggest, can be obtained by the methods introduced in early 1922. It is only then that the finitist standpoint is taken.

5. There is a delicate evolution from “tau” to “epsilon” that can be followed in Ewald and Sieg 2013; here we use directly the epsilon terms.

6. The so-called \(\varepsilon\)-substitution method has been re-invigorated by work of Tait and Mints; a broad survey is given in Avigad and Zach 2007.

7. The Ackermann function was included among Herbrand’s finitist functions. At this point, the system F was not “identified” with PRA.

8. See, for detailed discussion, mathematical analysis and additional references, Tait 2002 and Feferman & Strahm 2010. A penetrating explication of the finitist standpoint taken by Hilbert and Bernays is given in Ravaglia 2003.

9. Hilbert’s considerations are analyzed in Sieg 2012 (section 5) and are also discussed in Hallett 2013.

10. For the close connections between Hilbert’s proposal and Gentzen’s attempt to mould it into a consistency proof, see section 6 of Sieg 2012. The work in Gentzen’s “Urdissertation” is described in von Plato 2008 and 2009.

11. For instance through an ordinal analysis as explained in Definition 3.4.

12. For a detailed descriptions of natural deduction calculi see Prawitz 1965 or Troelstra & Schwichtenberg 2000. To achieve a more symmetric treatment of negation one can replace in the above axiomatic formulation the principle of double negation by the axiom \((B\land\neg B)\to A\) (to obtain intuitionist logic) and by the axiom \((\neg A\to (B\land\neg B))\to A\) (to obtain classical logic).

13. The Hauptsatz states informally, according to Gentzen (1934/35: 177), that every purely logical proof can be transformed into a certain, by no means unique, normal form. One of the essential properties of such normal proofs is expressed by: “It does not make detours”.

14. Though the crucial paper was published only in 1958, the central ideas of the “Dialectica Interpreation” go back to lectures Gödel presented at Yale in April of 1941. See Gödel 1942 in volume III of his Collected Works.

15. Both Brouwer (1927) and Zermelo (1932), from dramatically different foundational perspectives, considered infinite proofs. Indeed, Brouwer asserted concerning his infinite proofs:

These mental mathematical proofs that in general contain infinitely many terms must not be confused with their linguistic accompaniments, which are finite and necessarily inadequate, hence do not belong to mathematics. (Brouwer 1927: 460, note 8).

He added that this remark contains his “main argument against the claims of Hilbert’s metamathematics”.

16. “Because of Gödel’s result consistency proofs now require a method that is finite (or constructive) but which is nevertheless very strong when formalized. People think this is impossible or at least unlikely and extremely difficult. The situation is somewhat similar to that of finding a new axiom that carries conviction and decides the continuum hypothesis”. (Takeuti 1975: 366)

17. Terms have to be of appropriate type, e.g., in (2) below, t and r have to be of type 0 while in (3) s and t have to be of type \(\sigma\) and \(\tau\), respectively. The required typing should always be clear from the context.

18. “Having proposed the fundamental conjecture, I concentrated on its proof and spent several years in an anguished struggle trying to resolve the problem day and night” (Takeuti 2003: 133).

19. Below in \((\forall_2\bL)\) and \((\exists_2\rR)\), \(A(a)\) is an arbitrary formula. The variable U in \((\forall_2\rR)\) and \((\exists_2\bL)\) is an eigenvariable of the respective inference, i.e., U is not to occur in the lower sequent.

20. Meaning that it proves the same formulae as the system with cuts.

21. In the 1970s Martin-Löf gave a normalization proof for a type theory with a universe that contained itself. The metatheory for this proof was basically a slight extension of the same type theory. Ironically, it turned out that the type theory was inconsistent.

22. Below Con(T) and Proof\(_\bT\) are arithmetized formalizations of the consistency of T and provability in T, respectively, as explained in Definition 1.3. \(\Corner{F}\) denotes the Gödel number of a formula F. For every number n, \(\bar{n}\) denotes the \(n^{th}\) numeral, i.e., the term obtained from 0 by putting n successor function symbols in front of it.

23. This is straightforward for languages allowing for quantifiers over sets of natural numbers, but for theories like PA one would have to add a new predicate symbol to the language.

24. Recall that the class of arithmetical formulae is denoted by \(\Pi^1_0\). These formulae can still contain free set variables which can be utilized to show that \((\Pi^1_0\Hy\bCA)_0=(\Pi^0_1\Hy\bCA)_0\).

25. They were re-obtained in purely proof-theoretic ways (and generalized) by Feferman & Sieg (1981b).

26. The attribute “reverse” comes from this additional objective: When a theorem is proved from the right axioms, the axioms can be proved from the theorem.

27. Ironically, the counterexamples that come to mind as soon as one begins to think about it come from one of the main inventors of reverse mathematics.

28. Using classical logic and just the connectives \(\land\),\(\lor\), \(\neg\) and quantifiers \(\forall\), \(\exists\), any formula can be re-written in such a way that the negation sign occurs only in front of atomic formulas. A formula of the latter form is P-positive if P does not appear negated in it.

29. The extension then has ordinals \(\Omega_{\alpha}\) for all \(\alpha\leq\nu\) and each ordinal of the form \(\Omega_{\beta+1}\) gets furnished with its own collapsing function \(\psi_{\!_{\Omega_{\beta+1}}}\).

30. For a detailed account of the history of the proof theory of iterated inductive definitions see Buchholz et al. 1981.

31. Upper bounds for (i) and (iii) are due to Takeuti (1967) while upper bounds for (iv) and (v) are owed to Takeuti and Yasugi (1973). The exacts bound in (iii) and (ii) are due to Pohlers (1977) and Buchholz (1977a), respectively. Other exact bounds involve the work of several people.

32. The Hilbert project has produced three volumes of unpublished lecture notes and material that is no longer easily accessible, for example the original first edition of Grundlagen der Geometrie and that of the 1928 book of Hilbert and Ackermann. Associated with the edition and study of that material is also a rich secondary literature with papers, for example, by Mancosu (1998, 1999a) and Zach (2003, 2004).

33. Proof-theoretic studies play an important role in areas such as temporal and modal logics with applications to software verification. Linear logic and the other substructural logics are being used successfully in linguistics. Here the computational aspects of the logics are important, and the development of proof systems for such logics aims to find systems that are both expressive and efficient. Our list of “Related Entries” below points the interested reader to information concerning these logics and their applications.

34. The best-known systems are Coq, Isabel, HOL, and the more recent theorem prover Lean. Sieg has developed with collaborators and students the system AProS; see www.phil.cmu.edu/projects/apros.

35. These four conditions correspond to the conditions \((\alpha)\) through \((\delta)\) of \(\#71\) in Dedekind 1888; they are easily seen to be equivalent to the so-called Peano axioms. The chain of the system \(\{1\}\) (with respect to the mapping \(\varphi\) of N) is the intersection of all systems that contain 1 as an element and are closed under \(\varphi\).

36. In Torretti 1978 [1984: 234], for example, one finds the following observation:

… the completeness axiom is what nowadays one would call a metamathematical statement, though one of a rather peculiar sort, since the theory with which it is concerned includes Axiom V2 [i.e., the completeness axiom] itself.

37. We have modified the translation one finds in the Collected Works. In particular, logical expression stands for logischer Ausdruck, satisfy for erfüllen, domain of thought for Denkbereich, statement for Aussage, and proposition for Satz.

38. In On the Infinite Hilbert writes retrospectively:

In particular, a contradiction discovered by Zermelo and Russell had, when it became known, a downright catastrophic effect in the world of mathematics. (Hilbert 1926: 375)

More can be learnt about Hilbert’s reaction at the time from various reports in 1902 and 1903 (cf. Peckhaus 1990: 57).

39. One should keep in mind that the “existence of sets” was the central issue, and it was to be guaranteed by the consistency of an appropriate axiom system, a viewpoint shared by Poincaré. The latter was, on the whole, impressed by Hilbert’s novel approach.

40. See Mancosu 1999b. Not only the details of Principia Mathematica were of significance; on the contrary, the broad logicist outlook had a real impact on Hilbert. Hilbert’s notes for a course on Set Theory (from the summer term 1917) and his talk Axiomatisches Denken reveal a logicist direction in his work. In the latter essay Hilbert writes:

The examination of consistency is an unavoidable task; thus, it seems to be necessary to axiomatize logic itself and to show that number theory as well as set theory are just parts of logic. (Hilbert 1918: 153).

If we try to achieve such a reduction to logic, Hilbert says at the very end of the set theory notes, “… we are facing one of the most difficult problems of mathematics”. (Hilbert 1917)

41. This is reported in Dawson 1997 (p. 68) based on doc 023-73-04 in the Carnap Nachlass at the University of Pittsburgh.

42. Volume III of Gödel’s Collected Works contains a paper entitled “Vortrag über Vollständigkeit des Funktionenkalkül’s” that is taken to be the manuscript for his talk in Königsberg. However, Gödel’s talk was a contributed talk of just 20 minutes; only a small part of the paper could have been delivered.

43. The historical context and relevant details are presented in Sieg 2012.

44. More precisely, we define a function CODE by recursion on formulae that associates with each formula \(\varphi\) a term in the language of \(T\), which is also denoted by \({\Corner{\varphi}}\).

45. The representability conditions for PROOF are as follows: If PROOF\((D, \varphi)\) then \(T \vdash \iproof(\Corner{D},\Corner{\varphi})\), and if NOT PROOF\((D,\varphi)\) then \(T\vdash \neg \iproof(\Corner{D},\Corner{\varphi})\).

46. Note that G is, as Dawson put it (on p. 68), “an involved combinatorial statement expressed in the richer language of the system of Principia Mathematica” (or set theory). It is only after the “arithmetization of syntax” and the representation of the syntactic notions in elementary number theory that G is turned into an arithmetical statement; section 3 of Gödel 1931a. See the remarks below from Wang 1981 concerning this development after the Königsberg conference, and the further very detailed description of how G is equivalent to a Diophantine equation in section 8 of Gödel’s 1934 Princeton lectures and in Gödel 1938/9.

47. The letter, to the best of our knowledge, has not been published. One of the authors, Sieg, had received a copy from Chevalley’s daughter quite a few years ago.

48. As to the details of their interaction, see the Introductory Notes to Gödel’s correspondence with von Neumann and Herbrand, in volume V of the Collected Works. Gödel’s contrary perspective on the formalizability of finitist proofs is expressed not only at the end of his 1931 paper, but also in his letters to von Neumann and Herbrand, as well as in his contribution to the meeting of the Schlick Circle on 15 January 1931 and in the “Nachtrag” to his Königsberg remarks. In the latter he wrote:

For a system in which all finitist (i.e., intuitionistically proper) forms of proof are formalized, a finitist consistency proof as sought by the formalists would be altogether impossible. However, it seems doubtful, whether one of the systems formulated up to now, say Principia Mathematica, is so comprehensive (or whether such a comprehensive system exists at all). (Gödel 1931b: 204).

49. The usual recursion theorem is formulated for partial recursive functions but there is a version, due to Kleene (1958), that works for primitive recursive functions.

50. Accessible accounts can be found in Torkel Franzén’s book (2004a) and his paper (2004b).

51. Brouwer did not include (Hyp 2) among the hypothesis. It expresses the “monotonicity” of the bar. Classically it’s rather superfluous but intuitionistically it is essential as Kleene observed: \(\BI_{\igen}\) formulated without (Hyp 2) yields instances of excluded middle that are incompatible with Brouwer’s continuity principles (Kleene & Vesley 1965: 7.14).

52. A bar B gives rise to a well-founded ordering \(\prec\) on \(\bbN^*\) where \(t\prec s\) means that t is a node above s and \(t\notin B\). Viewed in this way, \(\BI_{\igen}\) is a principle of transfinite induction along \(\prec\). For the implication \(\BI_{\igen}\to{\bCA}\) to hold it is important that B can be of arbitrary complexity. Thus the moral drawable from this is that impredicative comprehension can be deduced from transfinite induction on impredicatively defined orderings.

53. Girard is also very skeptical about the intuitionistic setting of Spector’s interpretation: “all these topics have nothing to do with intuitionism” (Girard 1987: 479).

54. As a matter of clarification, cut free proofs are not allowed to contain other instances of \(\tilde{\Omega}\).

55. For more background information see Takeuti 1985: 259; Feferman 1989: 362, and Pohlers 1991: 374.

56. For more details see Rathjen 1999a.

57. For more details see Rathjen 2015. As for the unprovability of \(\Con(\PA)\) in PA, Gentzen (1943) explicitly states that his proof makes no appeal to the second incompleteness theorem.

58. In Rathjen 2015 the question is pondered whether the latter result could have been proved much earlier (from a technical as well as sociological point of view).

59. For extensions and reflections see Sieg 1991.

60. Theorem F.4 can be extracted from Kreisel, Mints and Simpson (1975), Lopez-Escobar (1976) or Schwichtenberg (1977) and was certainly known to these authors.