FOM: Hilbert's program and RCF; dead white males

[Stephen G Simpson]

This is a follow-up to:

 [1] Tue Dec 21 11:04:48 1999 - Harvey Friedman - FOM: 73:Hilbert's
     program wide open?

 [2] Tue Dec 21 16:04:21 1999 - Stephen G Simpson - FOM: Hilbert's program
     and RCF

 [3] Wed Dec 22 19:43:15 1999 - Harvey Friedman - Re: FOM: Hilbert's
     program and RCF

Harvey Friedman [3] writes:

 > I don't know exactly what you are driving at, 

OK.  Let me try again to make my main point, this time leaving out
some side points that may have previously obscured the main point.

In [1] (i.e., #73), you said that there has been considerable progress
on one aspect of Hilbert's program, viz. the aspect (A) of proving the
consistency of a lot of interesting mathematics within PRA.  Yes,
fine, I agree.  But then, as the ``perhaps most notable'' progress in
this direction (A), you cited your newly announced result that PRA
proves Con(RCF).  Now, I like this result very much, but I object to
this formulation of why it is interesting.  I object on the grounds
that this formulation neglects known results that seem much better
with respect to (A).  One of these known results is that PRA proves
Con(WKL_0^*).  Here WKL_0^* is the subsystem of 2nd order arithmetic
with exponentiation and Sigma^0_0 induction and Sigma^0_1 bounding and
Delta^0_1 comprehension and Weak K"onig's Lemma.  (See Simpson/Smith,
APAL 31, 1986, 289-306.  See also Section X.4 of my book.)  This
result seems much better with respect to (A), because WKL_0^* seems to
accommodate formalization of much more mathematics than RCF.  In
particular, WKL_0^* includes the basics of analysis, and elementary
number theory, and countable modern algebra (countable groups,
countable fields, etc), but RCF includes none of these.

There is still an issue between you and Ferreira over his claim that
WKL_0^* and perhaps much weaker systems can be shown to interpret RCF
in an obvious natural way, by formalizing real polynomial algebra.  I
can see some possible problems with Ferreira's claim, and I will be
interested to see how this turns out.  In any case, all of this stuff
is of obvious long-term f.o.m. significance.

 > partly because the point you are making has nothing to do with the
 > main thrust of my posting #73.

You are correct.  My main point above has little or nothing to do with
the main thrust of #73 (i.e., [1]).  My main point above is only a
response to one relatively minor issue that was broached in #73.

 > #construct more and more comprehensive models of mathematical
 > practice which can be shown to be conservative extensions of PRA
 > for Pi-0-1 sentences. Furthermore, strive for the proof of such
 > conservativity to be actually given in PRA, in the sense that it is
 > not merely a proof somewhere that in fact such a proof exists.#

Yes, this is a good statement of my favorite variant of Hilbert's
program, the one I pursued in my paper ``Partial realization of
Hilbert's Program''.  A very important system here is WKL_0.  A lot of
mathematics can be done in WKL_0, including some fairly sophisticated
abstract algebra, functional analysis, measure theory, etc etc.  A lot
of this is worked out in Chapters IV and X of my book.

Incidentally, I have another conservation result along those lines: We
can add not only Cohen-generic and Jockusch/Soare-generic reals, but
also Sacks-generic reals and maybe even Solovay-random reals to WKL_0,
and it all stays conservative.  But at the moment I don't know how to
use the Sacks-generic and random reals in mathematical practice.  By
Brown/Simpson, there are some apparent uses of the Cohen-generic reals
(to prove the Open Mapping Theorem, etc) but I don't know for sure
that they are essential.

 > By the way, you seem to take PRA as something special for Hilbert's
 > program.

Yes, I definitely view PRA as something special for Hilbert's Program.

 > why take PRA as a dividing line? It makes more sense to recognize
 > that there are gradations, and that the weaker the theory that is
 > doing the proving, the more "unimpeachable" it is, and hence the
 > stronger the result for Hilbert's - or somebody's - program. ##

Of course.  But PRA is still special, because it represents a certain
robust and coherent concept of function obtained by finitistic
iteration.  It is of long-range scientific importance.  Tait's paper
on finitism contains good arguments about this.

 > And if Hilbert can be seen to clearly take PRA as the dividing line, then
 > perhaps people just concentrate on this dividing simply because of its
 > historical connection with David Hilbert. 

No, it is not just the historical connection with Hilbert.  After all,
Hilbert is the proverbial dead white male, but finitism and PRA are
very much a live issue in f.o.m.

 > 1. The fundamental theorem of algebra, that a complex polynomial of degree
 > >= 1 has a root.
 > 2. The whole of Euclidean geometry as developed formally by Hilbert.
 > 3. If a multivariate complex polynomial is one-one from some C^n into C^n
 > then it is onto.
 > 4. I remember being told about RCF and a famous 1,2,4,8 dimensional theorem
 > about certain types of algebras. Perhaps somebody can refresh my memory of
 > this.

Note that items 1 and 3 above are theorem shemes in RCF, not single
theorems of RCF.

Re item 4, Bott and Milnor used homotopy theory to prove that the only
finite-dimensional nonassociative algebras over the reals are those of
dimensions 1, 2, 4, 8 (the reals, the complex numbers, the
quaternions, the octonians).  Therefore, by completeness of RCF, this
is also a theorem scheme of RCF.

 > Now there is a very interesting objection to what I am
 > saying. Namely, that in each case one can only formulate the
 > theorems in a fixed dimension since the language of RCF does not
 > have variables over natural numbers.

Right.  Here is a specific question that is apparently not covered by
your announced result.  Does PRA prove that the theorem schemes for
items 1, 3, 4 above are provable in RCF?  How about EFA?

-- Steve