Von Neumann's consistency proof

I will attempt to answer your first question by describing the context of the von Neumann paper you have asked about.

As is well known, Hilbert had earlier posed the problem of establishing the consistency of first order arithmetic (with full induction), and had suggested the development of the method of "$\varepsilon$-substitutions" (also known as "$\varepsilon$-calculus") as a means of achieving this goal.

The first substantial advance in this direction was made by Ackermann in his 1925-doctoral dissertation (written under Hilbert's supervision) entitled Begründung des "tertium non datur" mittels der Hilbertschen Theorie der Widerspruchsfreiheit, which was published in the same year in the journal Mathematische Annalen. In this work, Ackermann proved the consistency of a system of arithmetic with induction only for quantifier-free formulae. Ackermann's work was later extended by von Neumann in his 1927-paper you have asked about, in which von Neumann developed further techniques that demonstrated the efficacy of $\varepsilon$-calculus. He also gave a detailed critique of Ackermann's earlier proof.

Eventually, Gentzen used another technique (cut-elimination) to give a consistency proof for first order arithmetic in 1936, which highlighted the role of the ordinal $\varepsilon_0$ in the consisteny proof of arithmetic. Gentzen's breakthrough prompted Ackermann, in his 1940 paper in Mathematische Annalen, to forumlate a proof of the consistency of arithmetic with the machinery of $\varepsilon$-calculus.

Now about your second question.

From what I can tell, techniques developed by von Neumann in his 1927 paper have now been absorbed into the folklore of the subject. The following papers provide excellent expository accounts of $\varepsilon$-calculus. They also contain pointers to the rich literature of the subject.

  1. G. Mints, A method of epsilon substitution for the predicate logic with equality, Journal of Math. Sc.i 1997

  2. G. Moser and R. Zach, The epsilon calculus and herbrand complexity, Studia Logica 2006.

PS. See also Ed Dean's nice answer.


I'm late to the party, but hope that the following might usefully complement Ali's nice answer and references, first by elaborating slightly on the historical side, and second by briefly indicating an $\varepsilon$-substitution-style consistency proof for the first-order-logic-based theory analogous to the $\varepsilon$-caculus-based system treated by von Neumann.


Ackermann's Begründung des "tertium non datur" mittels der Hilbertschen Theorie der Widerspruchsfreiheit actually set out to prove the consistency of all of analysis, and Ackermann initially believed he'd done just that. However,

... while correcting the printer's proofs of his paper, he had to introduce a footnote ... that restricts his rule of substitution. After the introduction of such a restriction it was no longer clear for which system Ackermann's proof establishes consistency. Certainly not for analysis. ... In [Zur Hilbertschen Beweistheorie] ... von Neumann criticized Ackermann's proof and presented a consistency proof that ... came to be accepted as establishing the consistency of a first-order arithmetic in which induction is applied only to quantifier-free formulas.

-- From Frege to Goedel (my emphasis)

One can rather quickly give a proof in the first-order logic setting that conveys the spirit of an $\varepsilon$-substitution approach to proving the consistency of the mentioned theory.

Let $\mathsf{T}$ be the theory which has the usual universal axioms of Peano arithmetic, but in which induction is allowed only for quantifier-free formulas. To prove $\mathsf{T}$ consistent, it suffices to show that any finite conjunction of Skolem instances of axioms of $\mathsf{T}$ is satisfiable. (Note that here we're appealing to Herbrand's theorem, which has analogues in the Hilbert-Bernays $\varepsilon$ Theorems.) We can begin to do that here by interpreting $0$, $S$, $+$, $\times$ numerically in the obvious way; all non-induction axioms of $\mathsf{T}$ are purely universal, and so will come out true under such interpretation.

All that remains is numerically interpreting the Skolem function symbols arising from induction axioms (and this is what's analogous to finding numerical interpretations of $\varepsilon$-terms in the $\varepsilon$-substitution method of Hilbert, Ackermann, von Neumann). As we only have quantifier-free induction in $\mathsf{T}$, Skolem instances of induction axioms are of the form $$ \varphi(\vec{y}, 0) \wedge [\varphi(\vec{y},f_\varphi(\vec{y},x)) \rightarrow \varphi(\vec{y},Sf_\varphi(\vec{y},x))] \rightarrow \varphi(\vec{y},x)$$ where $\vec{y}$ is, say, $y_1,\dots,y_k$. Because all $\varphi$ are quantifier-free here, there is no interaction/nesting among the $f_\varphi$ arising from induction axioms, and in fact they can all be interpreted in a uniform way: namely, each $f_\varphi$ can be interpreted by $\hat{f_\varphi} : \mathbb{N}^{k+1} \rightarrow \mathbb{N}$ given as $$ \hat{f_\varphi}(n_1,\dots,n_k,m) := \left\{\begin{array}{l} \min\{j<m : \varphi(\mathbf{n}_1,\dots,\mathbf{n}_k,\mathbf{j}) \wedge \neg\varphi(\mathbf{n}_1,\dots,\mathbf{n}_k,\mathbf{j+1})\} \\ 0 \mbox{ if no such exist} \end{array}\right.$$ One can readily check that this works to satisfy any finite conjunction of Skolem instances of $\mathsf{T}$ axioms, hence the theory is consistent.

The fact that there's no nesting of quantifiers (analogously, $\varepsilon$-terms) in the axioms of $\mathsf{T}$ is crucial to getting such a uniform interpretation. Ackermann underestimated the complexity involved in handling nested $\varepsilon$-terms; even after it became clear that Ackermann's proof fell short of its grand original intent, IIRC Hilbert et al. continued to believe they were very close to the goal, until of course Goedel's work revealed the fundamental obstacles at play.