Formal Proofs and Decidibility
David Booth, Renatus Ziegler · Birkhäuser Basel eBooks · 1996
In order to demonstrate the consistency of certain axiom systems, Hilbert makes use of a theory of mathematical proof in which the proof must be thought of as rigorously formalized in concrete symbols (see Hilbert [1922], [1923], [1926], Bernays [1922], Ackermann [1924]). “A proof is an array which must be graphically represented in its entirety” (Hilbert [1923, 152]). He adds: “A formula shall be said to be provable if it is either an axiom, or arises by substitution into an axiom, or is the concluding formula of a proof” (ibid., 152–153). The aim, then, is to show that, in a given axiom system, a contradictory formula (formalized in the same way) can with certainty never be proven. Axiom systems for which this can be demonstrated are said to be “consistent” (ibid., 157 and [1926, 179]). In the following where the formalization is quite general, such systems will be called formally consistent .