In the paper [Zur Hilbertschen Beweistheorie](http://link.springer.com/article/10.1007%2FBF01475439), John Von Neumann has proposed a consistency proof for
a fragment of first-order arithmetic (the fragment without induction and with
the successor axioms only) by a variant of Hilbert's substitution method.


The paper is in German, and I so could not read it.



> 
> **Question 1.** Can anyone explain the main ideas of Von Neumann's work in this paper?
> 
> 
> **Question 2.** Are there any references in English, explaining Von Neumann's work in details?
> 
> 
> 



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


