FOM: Hilbert's second problem

[Matthew Frank]

Dear FOMers,

It is not often that people solve one of Hilbert's problems without
realizing it.  The problem is Hilbert's second problem (properly
interpreted); the people in question are the two founders of this list.

Hilbert's second problem asked for a proof of the consistency of the
axioms of arithmetic.  People have often assumed that he meant the
arithmetic of the integers, and that the problem was therefore answered
negatively by Godel's incompleteness theorem.  A closer look at Hilbert's
text (and his reference to replacing the axiom of continuity with
Archimedes's axiom) makes it clear that he was talking instead about the
arithmetic of the reals.  So the question might be asked more precisely
as:

Can primitive recursive arithmetic [PRA] prove the consistency of the
theory of real-closed fields [RCF]?

(Neither the idea of primitive recursive arithmetic nor the formal theory 
of real-closed field was available to Hilbert in 1900, but I think Hilbert
in the 30s would have accepted this reformulation).  If RCF is interpreted
as a second-order theory, then Godel's incompleteness theorem does apply
(via interpreting arithmetic in second-order logic), and the answer is
negative.  So, in the light of Godel's result, the question ought to be
asked about the first-order version of RCF, and it is this question which
Friedman and Simpson have answered positively.  (I should point out that
neither Friedman nor Simpson has been willing to endorse the argument for
the proper formulation of Hilbert's second problem.)   In what follows I
consider RCF as a first-order theory.

Harvey Friedman's posting 56 (Aug. 27 1999) showed that EFA proves the
consistency of RCF; since EFA is a subsystem of PRA, Hilbert's second
problem follows.  This is significantly more difficult than showing that
PRA proves the consistency of RCF.  The simpler proof (which one could
unwind to get the PRA part of Friedman's proof) uses some of Simpson's
results in his (1999) book on Subsystems of Second-Order Arithmetic.

One would like to argue as follows:  in RCA_0, we can construct the real
algebraic numbers (as in SOSOA), show that they form a model for RCF, and
use soundness to conclude the consistency of RCF.  Since the consistency
statement is a statement of PRA, and RCA_0 is conservative over PRA, PRA
can also prove the consistency of RCF.  Unfortunately (as pointed out to
me by David Marker) stating soundness, or stating that the real algebraic
form a model for RCF in the ordinary sense, requires a truth definition in
a way that goes beyond RCA_0.

Fortunately, this argument can go through by using Simpson's "strong
soundness theorem" (p. 94).  This theorem (in RCA_0) proves the soundness
of a theory with a weak model, i.e. a model together with a restricted
truth predicate.  This truth predicate only needs to work for the axioms
and substitution-instances of subformulas of those axioms, though it has
to satisfy the Tarski conditions when meaningful.

It is particularly easy to show that the real algebraics form a weak model
of RCF, since all axioms are of RCF are of the form

(for all x_1)...(for all x_n)(exists y)phi

where phi is quantifier-free.  So the substitution-instances of
subformulas of the axioms are either AE-formulas, E-formulas, or
quantifier-free formulas.  One truth predicate that works is the one 
that outputs true to all substitution instances that result in AE or E
sentences, and goes through the relevant calculations for the
quantifier-free sentences; this can be specified in RCA_0, and it is easy
to check that it satisfies the relevant Tarski conditions.  Hence it gives
the weak model, and the positive answer to Hilbert's second problem as
desired.

--Matt Frank

P.S.  My interest in this comes from a variety of sources--my own attempt
to prove the theorem in question, spurred on by conversations with Mic
Detlefsen, David Marker, and Wilfrid Sieg; some e-mail conversations with
Jeremy Gray about historical matters; and my preparations for a submission
to the Hilbert Problems symposium that Bernd Buldt advertised on FOM about
a month ago.  (Since this will be working its way into such a submission,
comments now are especially welcome.)  My submission is tentatively titled
"Two, Four, Six....: Axioms in Geometry and Physics a Century after the
Hilbert Problems" I see the second problem as a best-case scenario for
axiomatziation; the fourth and sixth problems are much more problematic,
but there are interesting results to report about them as well.