FOM: Formal Z and R/lengths of proofs

[Harvey Friedman]

Reply to Dubucs 11:57PM 10/28/99.

>Harvey Friedman wrote (28 Oct 1999 02:56:24 -0500):
>
>> For instance, I have been pushing the program of showing that all of the
>>famous number theoretic results of the 20th century (and earlier) can be
>>proved within EFA = exponential function arithmetic. I conjecture that
>>Mordell's Conjecture and Fermat's Last Theorem can be proved in EFA. Some
>>world famous number theorists are quiite interested in this conjecture. It
>>leads to a whole host of related investigations cast in "traditional
>>foundational schemes." E.g., I recently posted a sketch (#56) that EFA is
>>enough to prove the consistency of elementary algebra and geometry; and in
>>fact, a whole host of theorems about elementary algebra and geometry to the
>>effect that if you use elementary algera and geometry to prove a number
>>theoretic result, then you can eliminate the elementary algebra and
>>geometry in favor of elementary number theory.
>
>Could you give to the members of FOM some idea of the ratio between the
>length of the original (analytical) proof and the length of the elementary
>proof which replaces it ?
>
>Thanks,
>
>Jacques Dubucs

This is a very important question that I didn't delve into in my
prior postings because it deserves a more thorough and systematic treatment
than I had time to give. I still don't have the time to do this sort of
thing justice. But I intend to make at least one major numbered posting on
this topic when I get a chance.

I'll start with the perhaps even more basic matter: lengths of proofs of
sentences in the language of real closed fields.

I will be giving several different formulations of the axioms of RCF, with
and without <,  and consider the following questions:

a) Suppose we know that A is a true sentence in this language with n
symbols. What can we say about the number of symbols needed to prove it in
ZFC with abbreviation apparatus?

b) Suppose we know that A is a true sentence in this language with n
symbols. What can we say about the number of symbols needed to prove it in
the various formulations of the axioms of RCF?

c) Suppose we know that A has a proof in one of the formulations of the
axioms of RCF. What can we say about the number of symbols needed to prove
it in the other various formulations of the axioms of RCF?

d) Revisit all of these questions for purely existential sentences, again
with or without <.

e) Revisit all of these questions for purely universal sentences, again
with or without <. Here an additional axiom system comes into play: the
ordered field axioms with <, or the real field axioms without <.

Most of the lower bound results are single exponential, and most of the
upper bound results are double exponential - although one may be piled on
top of another so that some of the upper bound results come out triple
exponential. In particular, there is nothing like indefinitely iterated
exponentials going on here.

Then I'll move on to systems that incorporate both integers and reals. The
most obvious ways of combining EFA and RCF result in either

a) an extremely strong combined system which is bi-interpretable with Z_2
(or countable set theory); this happens when we use least upper bound for
all formulas in the extended language. Obviously, this is not conservative
over EFA (exponential function arithmetic).

b) a number of combined systems which are conservative over EFA.

Now the question of the blowup in b). There is no blowup. I.e., there is a
small constant c such that any proof in the combined systems with at most n
symbols of an arithmetic sentence can be converted into a proof in EFA with
at most cn symbols of that arithmetic sentence. And if we add abbreviation
apparatus, the same result applies. To go further and specify actual
constants is quite detailed work, where one has to get very specific about
the way the formal systems are set up - but definitely worth doing.

Now everything I have said addresses only the problem of what happens when
real algebraic methods are combined with arithmetic methods. It does not
address the question of what exactly happens when more analytic methods are
combined with arithmetic methods. That remains to be explored
systematically.