University of Calgary
UofC Navigation

Hilbert's "Verunglückter Beweis," the first epsilon theorem, and consistency proofs


History and Philosophy of Logic 25 (2004) 79–94.


In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert’s Programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert’s epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert’s first epsilon theorem and a certain ‘general consistency result’ due to Bernays. An analysis of the form of this so-called ‘failed proof’ sheds further light on an interpretation of Hilbert’s Program as an instrumentalist enterprise with the aim of showing that whenever a ‘real’ proposition can be proved by ‘ideal’ means, it can also be proved by ‘real’, finitary means.


Dirk Schlimm (Bulletin of Symbolic Logic 11/2 (2005) 247–248)

Download from Taylor & Francis publishers


Download preprint

Download Preprint

See also: The Development of Mathematical Logic from Russell to Tarski · Completeness before Post · The practice of finitism · Hilbert's Program Then and Now · The Epsilon calculus