FOM: Hilbert's program

[Joseph Shoenfield]

     I think that Hersch's posting proclaiming the failure of
logicism, formalism, and intuitionism has been more than adequately
answered, and the answers have shown that all three have retained
an importance in logic.   I would like to say a little more about
the enormous effect that the Hilbert program has had.
     The Hilbert program was to give a finitary proof of the consis-
tency of an as large as possible part of mathematics.   He and his
associates found such proofs for large parts of first order number
theory (FONT).   Then Godel showed the impossibility of proving the
consistencty of FONT in FONT.   Since it was generally agreed that
finitary proofs could be formalized in FONT, it was necessary to
extend the program to allow some non-finitistic methods.   This led
to Gentzen's proof of the consistency of FONT using induction up to
epsilon-0.   This was the beginning of proof-theory.
     Later, Godel found a new consistency proof for FONT.   He observed
that finitary proofs had two essential properties: they dealt with
concrete objects, and they used constructive methods.   By replacing
the concrete objects by certain more abstrct objects, he was able to
give a constructive consistency proof for FONT.   Later, Spector ex-
tended this to a consistency proof for SONT, using more complicated
but still constructive methods.   I highly recommend Godel's paper
to fommers; it  is a model of how to combine foundational considera-
tions with significant mathematical results.   (The English version
first appeared in vol 2 of Godel's collected works.)
     Hilbert was the first to observe an important consequence of the
work of Frege and Russell; the notion of a proof in the predicate
calculus could be described entirely in terms of the form of the
propositions involved without any reference to their meaning.   (I
feel sure Frege and Russell did not observe this.   Strange as it
may seem today, Russell never even understood the difference between
an axiom and a rule of inference.)   This meant that consistency
was a statement about concrete objects, viz, symbols and expressions;
so there was some hope of giving finitary consistency proofs.
     The name formalist has been sometimes given to those who believe
that mathematics should study only the form of its propositions without
being concerned with their meaning.   It is a gross error to think that
Hilbert was a formalist in this sense.   What he did realize was the
the form of a proposition had much more to do with the meaning than
one had any right to expect.   This important observation has had an
enormous effect in logic.   Such important and diverse topics as the
fundamentals of model theory, the theory of the Kleene hierarchies,
and the theory of constructible sets are largely concerned with rela-
tions between the form and the meaning of propositions.