[FOM] 271:Clarification of Smith Article

[Harvey Friedman]

On 3/29/06 4:20 PM, "Andreas Weiermann" <weiermann at math.uu.nl> wrote:

>I am well aware that 2^[1000] is tiny
>when compared to the Graham number.
>I meant by my question whether the number of symbols
>needed for the proof of Theorem 1 in finite mathematics
>is larger than the Graham number.

>Anyway the answer to my question has been given
>promptly by Harvey Friedman in:
http://www.cs.nyu.edu/pipermail/fom/2006-March/010279.html

I think that a small comment is needed to derive this conclusion from the
cited posting of mine.

In fact, I will sketch a stronger conclusion from my cited posting.

THEOREM. Every proof in ATR of "TREE[3] exists" uses more than p symbols,
where p is the following number: the greatest halting time of a Turing
machine that can be proved to halt at the blank tape within ACA_0 + Pi12-BI
using at most 2^[1000] symbols.

To see this, consider the Sigma01 statement

"there exists q such that q is greater than all least witnesses of Sigma01
sentences provable in ATR with at most p symbols"

where p is the number in the above Theorem.

Note that the above statement is provable in ACA_0 + Pi12-BI with at most
2^[2000] symbols. 

Let q be the least witness for the above Sigma01 statement. I could have
stated the relevant result from my cited posting using 2^[2000] instead of
2^[1000]. 

Hence by my cited posting, q is smaller than TREE[3]. HENCE, if "TREE[3]
exists" can be proved in ATR using at most p symbols, then TREE[3] < q.
Contradiction.

I am pretty sure that we can squeeze a little bit more out of the work in my
cited posting. Namely:

THEOREM*. Every proof in ACA_0 + Pi12-BI of "TREE[3] exists" uses more than
p symbols, where p is the following number: the greatest halting time of a
Turing machine that can be proved to halt at the blank tape within ACA_0 +
Pi12-BI using at most 2^[1000] symbols.

This is all because "TREE[3] exists", "sits appropriately a bit higher than
ACA_0 + Pi12-BI."

We can define pi(T,TREE]3]) as the least number of symbols needed to prove
TREE[3] exists in the theory T.

1. pi(ACA_0 + BI,TREE[3]) is at most a perfectly normal number like a
trillion.
2. pi(ACA_0 + Pi12-BI,TREE[3]) > #(ACA_0 + Pi12-BI,2^[1000]). In fact,
greater than #(ACA_0 + Pi12-BI,#(ACA_0 + Pi12-BI,2^[1000])). The process can
be iterated a lot.
3. pi(ATR,TREE[3]) << pi(ACA_0 + Pi12-BI,TREE[3]).
4. The << in 3 can be given a good meaning in the theory.

For "various natural" T, pi(T,TREE[3]) varies wildly directly according to
the "strength" of T. THE SRONGER THE NATURAL SYSTEM T IS, THE LESS SYMBOLS
IT TAKES TO PROVE TREE[3], AT LEAST UP THROUGH ACA_0 + Pi12-BI and a bit
stronger. 

So we are at the foundations of a new kind of QUANTITATIVE PROOF THEORY. Of
course, it is quite CRUDE, in that even the smallest numbers involved are
grotesquely large. 

Here are some ingredients.

5. Any natural T, occurring in practice, has extremely small "entropy".

6. Entropy can be defined, say, by the number of symbols used in the
presentation of the axioms of T, where SCHEMES are allowed. If we are
talking about a theory NOT equipped with a presentation, then the entropy is
the smallest number of symbols needed to present some axiomatization.

7. Under 6, a list can be compiled of all of the seriously studied formal
systems coming up in f.o.m., and one can see that the entropies are very
small.

8. We can ask the question: can entropies ever be determined exactly in a
nontrivial natural case?

9. Because of these considerations, it makes good sense to define

#(T,p)

for any formal system T containing a sort for natural numbers, and the
system Q on that sort, and integer p >= 1 as follows. Look at all sentences
of the form 

(therexists x)(phi)

where x and all variables occurring in phi are of the natural number sort,
and all quantifiers in phi are bounded. For each such sentence that is
provable in T with at most p symbols, consider the least witness x, and then
take the max over all such least witnesses. This is #(T,p).

10. To cover unusual cases where T may not be 1-consistent, ignore such
sentences above that don't have any witnesses.

11. Find a reasonable p such that the various #(T,p), for natural T, are
significant, at least in the following sense. If T proves the consistency of
S then #(T,p) is considerably bigger than #(S,p). Show also that if p is
raised beyond the reasonable p, then this still holds.

12. In particular, show that one can use p = 2^[1000].

13. For particular combinatorial Sigma01 sentences, get estimates, lower,
and upper, on 

a. How many symbols are needed for a proof of the Sigma01 sentence in T?

b. The least witness of the Sigma01 sentence.

c. How the least number of symbols required to prove the Sigma01 sentence
varies according to the strength of the formal system.

14. In general, for any natural system T, one associates a natural Sigma01
combinatorial sentence phi "just a bit stronger than T" such that

a. The least witness of phi is greater than #(T,2^[1000]) symbols, and even
#(T,#(T,2^[1000])), as well as long iterates of this construction.

b. Any proof in T of phi needs more than #(T,2^[1000]) symbols, and even
#(T,#(T,2^[1000])), as well as long iterates of this construction.

c. For natural S provably consistent in T, the numbers for phi asociated
with S instead of T are "far smaller" than for T, in various strong senses.
every proof in S of phi needs more than #(T,#(S,2^[1000])) symbols.

These are some IDEAS for a good quantitative proof theory.

NOTE: Another kind of proof theory with quantities is already called "proof
mining", with a totally different aim.

Harvey Friedman