FOM: Hilbert's program and RCF

[Stephen G Simpson]

This posting is a followup to Harvey Friedman's discussion of what he
calls ``conventional approaches'' to Hilbert's program, in his posting
``FOM: 73:Hilbert's program wide open?'', Tue Dec 21 11:04:48 1999.

Friedman focuses on consistency proofs *within* PRA:

 > there is a system PRA (primitive recursive arithmetic) that some
 > authors like to identify with Hilbertian finitism. In all of the
 > proposed formalizations of extensive mathematics - including, say,
 > what goes on in such things as FLT - there is more than enough to
 > easily interpret PRA. So by Godel, Hilbert's program cannot be
 > carried out in such a setup.

However, Hilbert's program has another aspect: consistency and
conservative extension results *relative to* PRA.  There is reason to
believe that the real intention of Hilbert's program was to show that
every mathematically provable Pi^0_1 sentence is provable in PRA.  In
other words, to show that our formal system S for mathematics as a
whole is *conservative* over PRA for Pi^0_1 sentences, and provably
consistent *relative to* PRA.  This is not the same as the consistency
of S being provable *within* PRA.

See for instance W. W. Tait, Finitism, Journal of Philosophy, 1981,
pp. 524-546, and P. Kitcher, Hilbert's Epistemology, Philosophy of
Science, 43, 1976, pp. 99-115.

Of course G"odel's second incompleteness theorem shows that this more
restricted version of Hilbert's program also cannot be carried out
wholesale, e.g., for S = ZFC or, for that matter, S = PA.  However, it
*can* be carried out for, e.g., S = WKL_0, and WKL_0 suffices for a
remarkably large portion of mathematics, including many of the
best-known non-constructive theorems in analysis, algebra, and other
parts of core mathematics.  To me this looks like the most significant
progress to date in the direction of realizing Hilbert's program.
This is the point of my paper ``Partial Realizations of Hilbert's
Program'', JSL, 53, 1988, pp. 349-363, on-line at
<http://www.math.psu.edu/simpson/papers/hilbert/>.

Friedman continues:

 > There has been considerable progress on one front. Namely, to show
 > that a lot of interesting mathematics can be proved consistent
 > within PRA. Perhaps most notably, the consistency of Elementary
 > Algebra and Geometry - formalized by, say, real closed fields - is
 > proved consistent in PRA, and even in the much much weaker system
 > EFA (exponential function arithmetic, or ISigma(exp) discussed in,
 > say, Hajek/Pudlak). See posting #56.  In fact, RCF (real closed
 > fields) is interpretable in Robinson's Q (interpretable in the
 > sense of Tarski). Hence RCF is consistent relative to Q in an
 > appropriate sense.

But, how much interesting mathematics is formalizable in RCF?  Much
less than in WKL_0, for sure.  So it is not clear to me how much these
results concerning RCF contribute to Hilbert's program.

Nevertheless, I feel that these new results of Friedman on RCF (EFA
proves consistency of RCF, and Q interprets RCF) are remarkable and
have obvious foundational significance in terms of a possible future
base-theory free, coding-free incarnation of reverse mathematics,
stated in terms of interpretability.  I am looking forward to seeing
the proofs of these exciting new results.

-- Steve