FOM: Hilbert's program and RCF

[Harvey Friedman]

This is a response to Simpson 4:02PM 12/21/99. The response is in several
parts.

1. What does Simpson think Hilbert's program is (was)?
2. Main points of my posting #73 not addressed in Simpson's response.
3. RCF versus WKL_0. Extending and combining.

1. WHAT DOES SIMPSON THINK HILBERT'S PROGRAM IS (WAS)?

I am not an historian and like to rethink f.o.m. issues from scratch.
Nevertheless, I do acknowledge that sometimes looking at the past helps in
dealing with the present and future.

Simpson wrote

>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.

The **'s are mine. Under this interpretation of Hilbert's program for
Pi-0-2 sentences - not Pi-0-1 sentences - we already know many striking
counterexamples which simply cannot be eliminated or analyzed away. E.g.,
see posting #19 and another dozen or so. You can also go back to
Paris/Harrington.

As for Pi-0-1 sentences of a mathematical character (not consistency
statements), the only examples are the ones that have come up in my posting
#72 and related earlier postings. One thing I mean to do is to give
hopefully simpler versions of these Pi-0-1 independence results that are at
least independent of weaker systems than ZFC + large cardinals - i.e., take
advantage of the fact that I could make them independent of much weaker
systems in order to make them even simpler. This should work and be perhaps
rather elegant.

The emphasis you place on the distinction between PRA proving the
consistency of S and S being a conservative extension of PRA for Pi-0-1
sentences seems to be to be very misleading. First of all, in every case
that has naturally come up, if PRA proves the consistency of S then every
Pi-0-1 sentence provable in S is provable in PRA. And also if every Pi-0-1
sentence provable in S is provable in PRA then the consistency of S can be
proved in rather trivial extensions of PRA such as PRA + Con(PRA).

I don't know exactly what you are driving at, partly because the point you
are making has nothing to do with the main thrust of my posting #73.

Now let us take this conception of Hilbert's program literally.

**every mathematically provable Pi^0_1 sentence is provable in PRA. **

Does this mean

***every mathematically proved Pi-0-1 sentence is provable in PRA***?

Let's say we are referring to the actual published literature, rather than
"provable" or my latest incursions.

Then under this interpretation, Hilbert's program is wide open, and very
exciting to investigate. In particular, we need to answer

*Is FLT provable in PRA?*

I actually care about the distinction between EFA and PRA. Perhaps
historians will argue whether or not and to what extent or in what sense
Hilbert cared about the distinction between EFA and PRA. So I will ask

*Is FLT provable in EFA?*

I conjecture that both are true, and the latter is considerably harder to
prove than the former.

And of course FLT is no isolated case. There are more things that need to
be investigated along these lines.

Now suppose that Simpson does not mean *** but rather something more
strictly looking like **.

Then I would take the program to, in an operational sense, mean

#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.#

There is a reason for the second sentence above. See posting #61 and the
posting of Avigad Tue Nov 02 12:29:51 1999 as well as the review of
Simpson's book by Burgess which can be found at
http://www.math.psu.edu/simpson/sosoa/burgess/

I can inject here once again the spirit of my posting #73.

Perhaps we can even find a formal system, which supports mathematical
reasoning of enormous scope in an unfettered natural way, including proofs
of theorems that are known to have great logical strength in the presence
of the usual base theories we use, such as RCA_0, but where we have a
demonstrable conservative extension of PRA for Pi-0-1 sentences? Somehow we
manage to avoid incorporating the standard base theories such as RCA_0 by a
more subtle analysis of mathematical practice.

I am now actively trying to refute this possibility. Perhaps it can be
refuted to a large extent, but still carried out to a surprisingly large
extent? I just don't know how this will come out. There could be very
clever surprises on both sides of this fence.

2.  MAIN POINTS OF MY POSTING #73 NOT REFLECTED IN SIMPSON'S RESPONSE.

I wrote:

> > 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.

Simpson wrote:
>
>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.

By a proposed formalization of *extensive* mathematics, in the context of
my posting #73, I meant really extensive mathematics including the entire
graduate curriculum as normally presented. So this would include such
things as Cantor Bendixson, perfect subsets of Borel sets, various forms of
abstract measure theory, least upper bound principles, noneseparable Banach
spaces and duals, etcetera.

There are no proposed formalizations that go that far that are not
essentially set theory with many iterations of the power set operation. In
any case, no formalization of things like Cantor Bendixson or a variety of
things that in the usual setup of reverse mathematics, are at least ACA_0
and beyond, and so well beyond being conservative extensions of PRA, or
provably consistent relative to PRA.

In fact, it is common wisdom that you cannot include such kinds of abstract
mathematics in a conservative extension of PRA, and the partial evidence
normally given is that such abstract mathematics reverses to systems that
in fact prove the consistency of PRA, such as ACA_0 and higher.

The point of my posting is to question that line of reasoning since it
relies on a base theory that is subject to various kinds of attack.

Simpson wrote

>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.

The point is that I am criticizing this kind of citing of Godel's theorem.
E.g., there could be a very powerful practical set theory that covers a
vast amount of abstract mathematics in an unfettered way, and yet is
provably consistent within, say PRA!  Or maybe at least provably consistent
within something unexpectedly weak.

E.g., you don't actually use full comprehension in actual abstract
unfettered mathematics, but rather only blue comprehension, and that makes
it metamathematically much much weaker, while preserving all of the
theorems in an unfettered, natural, direct way.

I want to see how far one can go in either direction with this. I.e.,
refute that this can be done. And also maybe actually do something like
this.

Simpson wrote

>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.

Of course, reverse mathematics is filled with all kinds of examples where
this fails, because over the base theory RCA_0, things reverse into ACA_0
and higher - see Simpson's book.

I'm not going to criticize this business of WKL_0 being conservative over
PRA for Pi-0-1 and Pi-0-2. After all, the result is credited to me. But it
has nothing to do with the main points of my posting #73.

>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/>.

I was making the point that it is still possible to realize Hilbert's
program in a way that is approximately 10^100 times as powerful. Only I
suspect that it can't be done and I am trying to refute that.

By the way, you seem to take PRA as something special for Hilbert's
program. See the discussion of this in the paragraph below marked ##.

3. RCF VERSUS WKL_0. EXTENDING AND COMBINING.

>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.

Simpson wrote
>
>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.

I think that the point you are making is that WKL_0, or even RCA_0, proves
the intermediate value theorem for continuous functions, and hence for
polynomials. Hence every theorem of RCF translates into a theorem in RCA_0
via the coding of real algebra in RCA_0. Incidentally, this argument can be
used to prove the consistency of RCF relative to the consistency of RCA_0,
and hence PRA. And I think it can be nudged a bit to show the consistency
of RCF within PRA. This would be much easier than previous arguments that I
know of.  Of course, the result in posting #56 that RCF can be proved
consistent within EFA is much more complicated.

##However, what you are saying here doesn't make sense unless you have
decided that Hilbert's program is absolutely tied to PRA. If you interpret
Hilbert's program to mean that one wants to prove consistency or
conservation extension results using methods that are somehow
"unimpeachable," then 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. ##

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. In the long run, this is not an
appropriate reason to take PRA as a dividing line, whereby weaker systems
don't "contribute to Hilbert's program." In other words, PRA is not the
dividing line between relevance and non relevance just because of what
Hilbert may or may not have said.

As far as what mathematics RCF proves, take RCF as formalized by the least
upper bound axioms. All sorts of deep mathematical facts can be formalized
in RCF. E.g.,

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.

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.

So this leads to the project of giving an axiomatization of real algebra
that allows one to state and prove facts about, say, all polynomials, and
all semi-algebraic sets. One would have an induction principle on the
parameters such as the degree and the number of variables, and in the case
of a semi-algebra set, on the number of parameters. Perhaps an elegant
system like this would formalize the actual reasoning done by
semi-algebraic geometers. One would then attempt to prove the consistency
of the resulting system within a weak fragment of PRA (and conservativity
also over a weak fragment of PRA).

Along these lines, it makes sense to go for a combined system with
variables over integers and variables over real numbers. The idea here is
not to rely on coding of real numbers, but rather take them as primitive.

This kind of formalization, with its associated conservative extension
results, is precisely the kind of tool that would be useful to have -
especially for mathematicians - when analyzing a proof like FLT with an eye
towards showing that FLT is provable in PRA or even EFA. There are
continuous constructions that come in.