485 Mathematical Logic

Appendix to Hilbert’s lecture "The foundations of mathematics"

PAUL BERNAYS n/a

(1927)

1927 *Zusatz zu Hilberts Vortrag über "Die Grundlagen der Mathematik", Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität 6, 89–92 (485–489 of the present volume); reprinted in Hilbert 1928, 25–28.

1928 Die Grundlagen der Mathematik, mit Zusätzen von Hermann Weyl and Paul Bernays, Hamburger Mathematische Einzelschriften 5 (Teubner, Leipzig); contains reprints of Hilbert 1927, Weyl 1927 and Bernays 1927.

In formalizing arithmetic Hilbert (1922a, but see also 1922, p. 177) introduced a functional τ(f) whose argument is a number-theoretic function and whose value is a natural number. An interpreration of τ(f) is that, if for every a, the value of τ(f) is 0 and, otherwise, it is the least a for which Besides truth-functional and quantifier-free axioms, just one "transfinite" axiom, or rather axiom schema,

is required for the formalization. The universal and existential quantifiers used in current formulations of first-order arithmetic can be defined in terms of τ(f), and the axioms governing them can be derived from these definitions and axiom schema (1).

Hilbert then takes up the problem of consistency for a system containing just one primitive function, φ, hence just one τ-term, τ(φ); φ has been introduced by recursion equations (not containing τ). Assume that we have a proof of In that proof we replace free variables by numerals; τ(φ) is tentatively replaced by 0 everywhere. Every formula of the proof becomes a numerical formula. The formula

which is an axiom obtained from schema (1), becomes

where is the numeral obtained from the term a by the substitution of 0 for τ(φ). From the equations defining φ we can decide whether If so, formula (3) is true, and the substitution of 0 for τ(φ) is adopted. All the formulas in the proof have then become true numerical formulas, hence the end formula cannot be If we adopt the substitution of for τ(φ), and formula (2) becomes, for some

which is certainly true, and we can conclude as before.

Ackermann undertook (1924) to transform Hilbert’s brief sketch into a full-fledged consistency proof of analysis. First, a new notation, used from then on by Hilbert and his disciples, is introduced. The functional τ(f) is replaced by ε(A), or and formula (1) by

denotes a number of which the propositional function A(a) holds it it holds of any number. Although Ackermann is still able to make use of Hilbert’s argument, there are considerable differences between Hilbert’s fragmentary example and the general case now treated. In particular, we now have more than one propositional function, hence more than one ε-term; therefore, in schema (4) some may occur in A(a), and 486 whether A(a) becomes a true or a false numerical formula will depend on what is substituted for the inner ε. This complication, as well as others connected with the equations defining functions and functionals, can be overcome and, after a finite number of steps, we can obtain a definite sequence of substitutions, called a total replacement (Gesamtersetzung), that transforms the proof into a sequence of numerical formulas. Let instances of schema (4) be called critical formulas. In any total replacement all noncritical formulas are transformed into formulas that are true. If a critical formula is transformed into a false formula, new total replacements are successively generated in a definite manner, and after a finite number of steps the process leads to a total replacement by which all critical formulas are transformed into true numerical formulas.

At the time of publication Ackermann came to realize that his proof was inadequate to insure the consistency of the full system of analysis. He added a footnote (1924, p. 9) restricting his rule of substitution and thus decreased the strength of his system (see also von Neumann 1927, pp. 41–46). Ackermann communicated a new version of his proof, still for the restricted system, to Bernays by letter, and this version was presented in Hilbert and Bernays 1939, pp. 93–130.

Hilbert’s remarks above (pp. 477–479) and Bernays’s paper below refer to this second version of Ackermann’s proof. When several ε-terms occur, their composition, as Hilbert explains, can take the form of "embedding" or of "super-position". Hilbert shows that, in the case of embedding, is replaced, at the first trial, by 0; if the substitution is not successful, that is, does not yield true numerical formulas, a second trial takes place; is replaced by a numeral and this substitution is certainly successful. In the case of superposition, Bernays introduces a function that is equal to 0 for all values of the argument, and he is able to reduce, for the case of one ε-formula, superposition to embedding. Proceeding as Hilbert did in the case of embedding, he then obtains what he calls "one or two total replacements", or and that correspond, respectively, to the cases of one or of two trials. Now, either the first or the second of these replacements is certainly successful for the ε-formula considered. If it is successful for all the other ε-formulas, it becomes final. If not, a new function, which is 0 for all values of the argument but one, is tried. We thus obtain a sequence of functions, To any one of these functions, there correspond either one replacement, or two, and Bernays is able to show that the procedure terminates and to find an upper bound for the number of steps involved.

The translation is by Stefan Bauer-Mengelberg and Dagfinn Føllesdal, and it is printed here with the kind permission of Professor Bernays and Teubner Verlag.

1. To supplement the preceding paper [by Hilbert] let me add some more detailed explanations concerning the consistency proof by Ackermann that was sketched there.

First, as for an upper bound on the number of steps of replacement in the case of embedding, it is given by 2ⁿ, where n is the number of ε-functionals distinct in form. The method of proof described furnishes yet another, substantially closer bound, which, for example, for the case in which there is no embedding at all yields the upper bound ¹

487

2. Let the argument by which we recognize that the procedure is finite in the case of superposition be carried out under simple specializing assumptions.

The assumptions are the following: Let the ε-functionals occurring in the proof be

and

where may contain but no other ε-functional.

The procedure now consists in a succession of "total replacements"; each of these consists of a function replacement for by means of which goes over into and a replacement for by means of which go over into numerals and the values

are obtained for

We begin with the function which has the value 0 for all a ("zero replacement"), and accordingly also replace all the terms

by 0.

Holding this replacement fixed, we apply to

the original testing procedure, which after two steps at most leads to the goal; that is, all the critical formulas corresponding to

then become true.

Thus we obtain one or two total replacements, or and respectively. Now either (or is final or one of the critical formulas corresponding to becomes false. Assume that this formula corresponds to, say, and that a₁ goes into Then we find a value such that

is true. Now that we have this value, we take as replacement function for

not but the function defined by

At this point we repeat the above procedure with the values of the now being determined only after a value has been chosen for

and thus we obtain one or two total replacements, or and

488

Now either (or is final or for one of the ε-functionals that result from

by the previous total replacement we again find a value such that for a certain

is true, while

is false. From this it directly follows that

Now, instead of we introduce as replacement function by means of the following definition:

The replacement procedure is now repeated with this function

As we continue in this way, we obtain a sequence of replacement functions

each of which is formed from the preceding one by addition, for a new argument value, of a function value different from 0; and for every function we have one or two replacements, or and The point is to show that this sequence of replacements terminates. For this purpose we first consider the replacements

In these,

is always replaced by 0; the therefore always go over into the same ε-functionals; for each of these we put either 0 or a numeral different from 0, and this is then kept as a final replacement. Accordingly, at most of the replacements can be distinct.² If, however, is identical with then neither one has, or else each has, a successor replacement or and in these

is then in both cases replaced by the same number found as a value, so that, for both replacements, the also go over into the same ε-functionals.

Accordingly, of the replacements for which coincides with a fixed replacement again at most can be distinct. Hence there cannot be more than distinct or and altogether.

From this it follows, however, that our procedure comes to an end at the latest with the replacement function For, the replacements associated with two distinct replacement functions and cannot coincide completely, since otherwise we would by means of be led to the same value that has already been found by means of whereas this value is already used in the 489 definition of the replacement functions following hence in particular also in that of

3. Let us note, finally, that in order to take into consideration the axiom of mathematical induction, which for the purpose of the consistency proof may be given in the form

we need only, whenever we have found a value for which a proposition holds, go to the least such value by seeking out the first true proposition in the sequence

of propositions that have been reduced to numerical formulas.³

¹ [See in Hilbert and Bernays 1939, pp. 96–97, how this bound is obtained.]

² [See footnote 1.]

³ [In 1935, p. 213, end of footnote 1, Bernays writes that this last paragraph, on mathematical induction, should be deleted. In 1927 Hilbert and his collaborators had not yet gauged the difficulties facing consistency proofs of arithmetic and analysis. Ackermann had set out (in 1924) to prove the consistency of analysis; but, while correcting the printer’s proofs of his paper, he had to introduce a footnote, on page 9, 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. The proof suffered, moreover, from imprecisions in its last part. Ackermann’s paper was received for publication on 30 March 1924 and came out on 26 November 1924. In 1927, received for publication on 29 July 1925 and published on 2 January 1927, von Neumann criticized Ackermann’s proof and presented a consistency proof that followed lines somewhat different from those of Ackermann’s. The proof came to be accepted as establishing the consistency of a first-order arithmetic in which induction is applied only to quantifier-free formulas. When he was already acquainted with von Neumann’s proof, Ackermann communicated, in the form of a letter, a new consistency proof to Bernays. This proof developed and deepened the arguments used in Ackermann’s 1924 proof, and, like von Neumann’s, it applied to an arithmetic in which induction is restricted to quantifier-free formulas. It is with this proof of Ackermann’s that Hilbert’s remarks above (pp. 477–479) and Bernays’s present comments are concerned. It was felt at that point, among the members of the Hilbert school, that the consistency of full first-order arithmetic could be established by relatively straightforward extensions of the arguments used by von Neumann or by Ackermann (see Hilbert 1928a, p. 137, lines 20–21; 1930, p. 490, line 4u, to p. 491, line 2; Bernays 1935, p. 211, lines 4–7). These hopes were dashed by Gödel’s 1931. Ackermann’s unpublished proof was presented in Hilbert and Bernays 1939, pp. 93–130. In 1940 Ackermann gave a consistency proof for full first-order arithmetic, using a principle of transfinite induction (up to ε₀) that is not formalizable in this arithmetic.]