FOM: 73:Hilbert's program wide open?

[Harvey Friedman]

This discusses a new view of Hilbert's program together with an associated
research program.

1. CONVENTIONAL APPROACHES.

It is considered conventional wisdom, basic f.o.m., that Godel's second
incompleteness theorem killed Hilbert's program.

Historically, there have been complaints about this conclusion on the
following grounds. That Hilbert may have accepted some sort of "extended"
finitist reasoning such as Gentzen's use of quantifier free epsilon_0
induction, which he used to prove the consistency of PA = Peano Arithmetic.

I was never impressed by this objection, which has largely disappeared from
modern discussion (that I see) nowadays. I never believed that there was a
sufficiently clear informal notion of "extended finitism" that would admit
a definitive analysis. So my view was that for Hilbert's program, one needs
to point to a particular formalization of a particular kind of reasoning R,
and point to a particular formalization T of a particular kind of or area
of mathematics, and then investigate whether R is sufficient to prove the
consistency of T.

The general pattern of findings along these lines are now very well known.
Godel's second incompleteness theorem is of the utmost relevance, with
devastating effects. This comes about in the following way. The general
approach to formalizations R and to formalizations T are similar, where
very frequently R is a fragment of T, or at least (usually trivially)
interpretable in T in the sense of Tarski.

GODEL (modified for this purpose). If R is interpretable in T and T is
reasonable, then R does not prove the consistency of T.

More specifically, 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.

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. The other direction is false (for interpretability and
relative consistency), so that in some sense RCF is weaker than Q! And this
despite the fact that RCF is about a continuous context, yet Q is about a
discrete context.

The interesting thing about this is the use of weak fragments of arithmetic
to prove the consistency of continuous reasoning (although it is
fundamentally algebraic reasoning). There is an expectation of continuing
this program to cover much more continuous mathematics - perhaps continuous
mathematics that is not fundamentally algebraic in nature.

But this is still a rather weak, mild, restrained resurrection of Hilbert's
program. There is no expectation that one will be able to prove consistency
of mathematical reasoning that involves, say, the kind of discrete
mathematical objects used in the consistency proofs. E.g., iterated
exponential functions on the positive integers, to say nothing about
general discrete functions, or Borel measurable sets of real numbers, or
even unrestricted sets of real numbers.

After all, there is Godel's second incompleteness theorem to contend with.

Or is there?

2. FIRST PROBLEM ABOUT PUBLISHED NUMBER THEORY.

Let us consider what happens when we formalize a kind of or area of
mathematics.

In the case of PA and arithemtic reasoning, the modern way of looking at it
is to observe that induction is used over and over again throughout
arithmetic reasoning, and also every other type of arithmetic reasoning -
e.g., pigeonhole, counting arguments, etcetera, are easily reduced to
induction.

One also remarks that if you do arithmetic reasoning, you are in the
mindset to accept induction for any arithmetic property. It is acknowledged
that maybe there is something more basic about induction with respect to
properties that don't need quantifiers, but it is natural to use
quantifiers in many contexts, and there is no reason to accept induction
with respect to some arithmetic formulas with quantifiers and not for all
arithmetic formulas with quantifiers.

So people look at all of PA. And obviously by Godel, PRA does not prove the
consistency of PA.

However:

*it is clear that mathematicians do not apply induction with respect to
arbitrary arithmetic formulas. *

In one sense, this is a complete triviality. There are only finitely many
people who have ever lived, and each one of them uses only finitely many
arithmetic formulas for induction in their lifetime of arithmetic
reasoning.

But

*maybe mathematicians only apply induction with respect to arithmetic
formulas that have some as yet undisclosed special property.*

We would know exactly what to do about this situation if we knew the as yet
undisclosed special property that the arithmeitc formulas to which
induction is actually applied to. We would then make the appopriate
formalization of the appropriate fragment of PA and then decide whether or
not the resulting system can be proved consistent within PRA, or even
within EFA.

In fact, for celebrated published number theory, such a study has already
been proposed. Namely,

QUESTION 1: Is every published theorem in number theory, conveniently
stated in the language of first order arithemtic (possibly with
conventional coding apparatus), provable in EFA (exponential function
arithemtic or ISigma0(exp))?

So in this study, the special property is that only bounded quantification
is involved, with the help of exponentiation (beyond the ring structure of
the integers).

If this is the case, then clearly published number theory is provably
consistent within PRA, or even weaker systems that prove the consistency of
EFA. E.g., EFA* = superexponential function arithmetic or
ISigma0(superexp). See Hajek/Pudlak.

3. DISCUSSION OF MODELS OF LOGICAL REASONING.

However, can published number theory be proved consistent within EFA?

The immediate answer of no, using the result of Wilkie/Paris that EFA does
not even suffice to prove the consistency of Robinson's Q, and Robinson's Q
is obviously part of published number theory.

However, we can go further, and become more critical:

*it is clear that mathematicians do not apply first order reasoning with
respect to arbitrary logical formulas.*

And once again, in sone sense, this is a complete triviality. There are
only finitely many people who have ever lived, and each one of them uses
only finitely many logical formulas in their lifetime of reasoning.

But again

*maybe mathematicians only reason with respect to logical formulas that
have some as yet undisclosed special property.*

And again: we would know exactly what to do about this situation if we knew
the as yet undisclosed special property that the logical formulas actually
used have. We would then make the appopriate formalization of the
appropriate fragment of predicate calculus and then decide whether or not
the resulting systems can be proved consistent within various systems.

We will not go further with this line of reasoning - which leads to a whole
new set of issues and programs. In particular, in this posting, we will
consider the unrestricted use of first order predicate calculus as given;
i.e., an assume part of any model of mathematical reasoning that we are
trying to prove consistent - or trying to prove cannot be proved to be
consistent.

But we leave this matter with a few remarks. It makes perfectly good sense
to restrict predicate calculus along various lines. However, when examining
the use of predicate calculus reasoning in mathematics, one needs to bear
in mind that it is, in a literal sense, both too large and too small. In
particular, it is too small in that the usual formalizations do not
accomodate abbreviations, and mathematics simply cannot be done without
abbreviations. So whereas it is true that mathematicians do not consider
very many logical formulas, they do make lots of abbreviations, which
allows them to manipulate complex formulas implicitly in terms of long
series of small formulas. This is an essential aspect of mathematics.

One can of course go even further and consider finite models of
mathematical reasoning, whereby there is a bound placed on the size of any
proof. And then consider what systems can prove consistency in this sense -
but with restricted size. This leads to the finite Godel's theorem, and my
initial work on this was extended by Pudlak and reported in the Handbook of
Proof Theory. But this whole matter leads to another set of subtle issues
that is outside the scope of this posting.

Of course, one can take this to the extreme of the extreme, and criticize
any model of mathematical reasoning whatsoever, and claim that mathematics
has no significant logical patterns - or at least none that can be
appropriately circumscribed. That the Hilbert program can only amount to
checking that there is no published proof in the literature of an
inconsistency!! Of course this is easily done, so in this sense consistency
is easily proved.

However, this is not a good model of mathematical reasoning - i.e.,
presence in the already published literature. Because the next time someone
publishes something, it will not be covered in the model.

For the rest of this posting, we will take first order predicate calculus
with equality (fopce) for granted. This can be replaced by a finite
fragment of fopce - where there are only finitely many well formed
formulas, up to change of symbols - with abbreviation power. Exactly what
finite fragment is needed, required, suitable, or convenient -  is an
interesting and important question.

4. MORE PROBLEMS ABOUT PUBLISHED NUMBER THEORY.

So what is the status of the consistency of published number theory?

PROBLEM 2. Is it provable in EFA that the consistency of published number
theory implies the consistency of EFA?

By combining problems 1 and 2, we get

PROBLEM 3. Is it provable in EFA that the consistency of published number
theory is equivalent to the consistency of EFA?

It is known that

*it is not provable in EFA that the consistency of Q implies the
consistency of EFA.*

*it is not provable in EFA that the consistency of ISigma0 (polynomially
bounded arithmetic) implies the consistency of EFA.*

We proved that

*it is not provable in EFA that the consistency of RCF (real closed fields)
implies the consistency of EFA.*

PROBLEM 4. Does published number theory imply EFA = ISigma0(exp)? Or even
just ISigma0?

PROBLEM 5. Does published number theory imply the consistency of EFA =
ISigma0(exp)?

To get the ball rolling, I am working on some "friendly" number theoretic
facts which not only imply EFA and the consistency of EFA, they are
equivalent to EFA, ISigma1, and ISIGMA2. That is - if these "friendly"
number theoretic facts are counted as published number theory. But it is
most interesting to do this under a strict interpretation of "published
number theory", and I can't say that these examples are that good yet.

5. A CONCRETE EXAMPLE.

There are zillions of them. For example, consider T = the set of all
statements in Hardy/Wright that are trivially formalizable in the language
of discrete ordered rings, and T' = the set of all statements in
Hardy/Wright that are trivially formalizable in the language of discrete
ordered rings with exponentiation on the positive integers. What is the
logical status of T and T'?

Naturally, we view the axioms of discrete ordered rings (i.e., the integers
form a discrete ordered ring) as part of T and T', and also the various
Tarski laws of exponentiation as part of T'.

Here is just one concrete example to focus attention on.

Look at the axioms: Z is a discrete ordered ring, plus the four squares
theorem (every positive integer is the sum of four squares). What is the
logical status of this system?

And consider the following system.

1. Z is a discrete ordered ring.
2. The ax + by = 1 criteria for relative primeness.
3. The four squares theorem.
4. Every 1 <= i <= n divides n!
5. There is a prime between n and 2n.
6. FLT for exponents 3 and 4.

What is the logical status of this system? Is it equivalent to
ISigma0(factorial), which would make it bi-interpretable with EFA? Does it
make any difference if we strengthen 6 to FLT, with suitable Tarski axioms
for exponentiation?

6. DISCRETE MATHEMATICS.

Discrete mathematics is "wilder" than number theory. It should be quite
easy to see that published discrete mathematics has high logical strength,
at least significantly higher than EFA. After all, there is celebrated
discrete mathematics that demonstrably involves very fast growing functions
and large integers - e.g., Ackerman. So this should be easy.

Wrong.

For example, let us take what should be an easy case. Ramsey's theorem for
n-tuples for infinite sets of natural numbers. In reverse mathematics over
the base theory RCA0, this implies ACA0 and is in fact a bit stronger
(discussed in Simpson's book).

But what about without the base theory? It is easier to talk about
formalization in the special case of n = 3 where in the reverse mathematics
setup, this is equivalent to ACA0.

What one needs is some principles of discrete mathematics to get enough
induction or induction like principles and enough power to get some
recursion theoretically serious infinite sets of natural numbers. It is not
clear how to do this appropriately, starting from scratch, and staying
within published discrete mathematics.

7. OF COURSE IT CAN BE DONE (SORT OF).

Of course one can generate consistency strength in some reasonable ways.
But every time I start to write something reasonable down, I am shocked by
how much more striking it would be to do it in some other ways that
literally quote from celebrated theorems in the literature. And there are
so many possibilities for doing this that cannot be dismissed out of hand -
that just might work. That is where the excitement is.

On the other hand, it is now clear from many examples that genuine
metamathematical phenomena studied intensively in f.o.m. has been shown to
be quite well embedded in mathematics - at least through fast growth rates
and large integers. E.g., see postings #19, #21, #22, #24, #25, #27, #34,
#36, #37, #40, #42, #43, #50, #51, #69, #71. And this is the case despite
the fact that in order to generate consistency strength in these examples,
one needs a kind of logician's base theory going well beyond what is in the
published literature.

A reasonable stab at generating consistency strength from mathematical
facts was presented in #46. And I intend to present others.

Does strict adherence to celebrated theorems in the literature lead to
substantial consistency strength or not? That is the intriguing question.

**********

This is the 73rd in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM
29:Large Cardinals/where are we? I  2/22/99  6:11AM
30:Large Cardinals/where are we? II  2/23/99  6:15AM
31:First Free Sets/Large Cardinals  2/27/99  1:43AM
32:Greedy Constructions/Large Cardinals  3/2/99  11:21PM
33:A Variant  3/4/99  1:52PM
34:Walks in N^k  3/7/99  1:43PM
35:Special AE Sentences  3/18/99  4:56AM
35':Restatement  3/21/99  2:20PM
36:Adjacent Ramsey Theory  3/23/99  1:00AM
37:Adjacent Ramsey Theory/more  5:45AM  3/25/99
38:Existential Properties of Numerical Functions  3/26/99  2:21PM
39:Large Cardinals/synthesis  4/7/99  11:43AM
40:Enormous Integers in Algebraic Geometry  5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees  5/25/99  5:11PM
43:More Enormous Integers/AlgGeom  5/25/99  6:00PM
44:Indiscernible Primes  5/27/99  12:53 PM
45:Result #1/Program A  7/14/99  11:07AM
46:Tamism  7/14/99  11:25AM
47:Subalgebras/Reverse Math  7/14/99  11:36AM
48:Continuous Embeddings/Reverse Mathematics  7/15/99  12:24PM
49:Ulm Theory/Reverse Mathematics  7/17/99  3:21PM
50:Enormous Integers/Number Theory  7/17/99  11:39PN
51:Enormous Integers/Plane Geometry  7/18/99  3:16PM
52:Cardinals and Cones  7/18/99  3:33PM
53:Free Sets/Reverse Math  7/19/99  2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry  8/27/99  3:01PM
57:Fixpoints/Summation/Large Cardinals  9/10/99  3:47AM
57':Restatement  9/11/99  7:06AM
58:Program A/Conjectures  9/12/99  1:03AM
59:Restricted summation:Pi-0-1 sentences  9/17/99  10:41AM
60:Program A/Results  9/17/99  1:32PM
61:Finitist proofs of conservation  9/29/99  11:52AM
62:Approximate fixed points revisited  10/11/99  1:35AM
63:Disjoint Covers/Large Cardinals  10/11/99  1:36AM
64:Finite Posets/Large Cardinals  10/11/99  1:37AM
65:Simplicity of Axioms/Conjectures  10/19/99  9:54AM
66:PA/an approach  10/21/99  8:02PM
67:Nested Min Recursion/Large Cardinals  10/25/99  8:00AM
68:Bad to Worse/Conjectures  10/28/99  10:00PM
69:Baby Real Analysis  11/1/99  6:59AM
70:Efficient Formulas and Schemes  11/1/99  1:46PM
71:Ackerman/Algebraic Geometry/1  12/10/99  1:52PM
72:New finite forms/large cardinals  12/12/99  6:11AM