## Notes to Proof Theory

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

\[f(x_1,\ldots,x_n,S(x))=h(x_1,\ldots,x_n,f(x_1,\ldots,x_n,x),x)\]
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.

### Notes to Appendix A

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).

### Notes to Appendix B

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).

### Notes to Appendix C

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}\).

### Notes to Appendix D

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

### Notes to Appendix E

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).

### Notes to Appendix F

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.