 Further Reading. Hilbert’s and Ackermann’s early proofs are discussed in Zach 2003; 2004. Von Neumann’s proof is the topic of Bellotti 2016. Ackermann’s 1940 proof is discussed in Hilbert &amp; Bernays 1970, and Wang 1963. A modern presentation is given by Moser 2006. An early application of epsilon substitution is the no-counterexample interpretation (Kreisel 1951).