FOM: length of proofs

[Harvey Friedman]

Peccatte wrote 09:54 PM 9/15/98:

>>Following is a short note published in AMM by Joel Spencer:
>>Short theorems with long proofs
>>American Mathematical Monthly, 1983, vol. 90, 365-366
>>
>>--- begin of quote ---
>...........................................................
>>(a) Short interesting statements are decidable.
>>(b) Short interesting theorems have short proofs.
>
>......................................................................
>
>> The possible falsity of (b) is only seeping into our mathematical
>>counsciousness.
>>--- end of quote ---

Martin Davis 5:06PM 9/15/98 wrote:
>>
>There has been some discussion on fom of the relevance of G"odel
>incompleteness to ordinary mathematical practice. But I don't recall
>anything on the relevance of G"odel "speedup": going to stronger systems
>will not only increase the set of provable statements, but there will also
>be statements provable in both systems whose proof is shortened
>"arbitrarily" (i.e. by any given recursive function, the statement depending
>on the given function) by going to the stronger system.
>
>Maybe we can hope that large cardinals will not only yield proofs of
>previously open questions but will also help in obtaining short neat proofs
>where only clumsy unwieldy ones were previously available.

I had planned to respond to Peccatte at some length, and now that Martin
Davis has written about this, I want to write this brief note.

The general theme of "short theorems" with only "extremely long proofs" has
been a central feature of my work on the incompleteness theorem since the
early 80's or even earlier.

For example, in my pi-0-2 finite forms of Kruskal's theorem, extended
Kruskal's theorem, and the graph minor theorem, the following phenomena
appears:

Let A be the relevant theorem in pi-1-1 form (the above 3 theorems are all
in pi-1-1 form). I give a strong (e.g., impredicative) system T such that A
cannot be proved in T. Let (for all k)(there exists n)(B(k,n)) be my finite
form of A. Then I show that for a very small fixed k, the sigma-0-1
sentence

(there exists n)(B(k,n))

cannot be "practically" proved in T. E.g., I show that any proof of this
sigma-0-1 sentence in T must have more than p symbols, where p is an
exponential stack of 2's of height 1000. That is such a large lower bound
that the issue of exactly how proofs are formalized - e.g., exactly what
kinds of abbreviations are allowed - is irrelevant. That might change it
to, say, a stack of height 998 or so.

And of course note that this sigma-0-1 sentence is obviously provable in T
in virtue of its being sigma-0-1. But the size of that proof corresponds to
the size of the least possible n, which is even much much higher.

So the upshot is: this sigma-0-1 sentence has a proof in T, but only
incomprehensibly large proofs; and this sigma-0-1 sentence has a short
proof in a system like pi-1-1 comprehension, because one simply gives the
usual proof of the original pi-1-1 sentence A in pi-1-1-CA, applies weak
Konig's Lemma to prove (for all k)(there exists n)(B(k,n)), and
instantiates k.

One specific example is sketched in

R.L. Smith (on the FOM!), Consistency Strenghts of some Finite Forms of the
Higman and Kruskal Theorems, in: Harvey Friedman's Research on the
Foundations of Mathematics, North-Holland, 1984, 119-136.

which I state here. I never published a properly general and streamlined
analysis of this situation, although the Smith writeup of my results did go
pretty far towards this.

In the specific example, recall that a most basic form of Kruskal's theorem
(KT) is that in any infinite sequence of finite rooted trees, one tree is
inf preserving embeddable into a later tree. I had shown that this was
provable in pi-1-2-BI but not in pi-0-2-BI_0, which is a strong extension
of ATR_0.

Now J.B. Kruskal also proves considerably more general results, including
this one, which we write as KT(k). We consider trees where the vertices are
labeled from {1,...,k}. Then KT(k) =

*in any infinite sequence of finite rooted trees whose vertices are labeled
from {1,...,k}, one tree is inf and label preserving embeddable into a
later tree.*

One of the finite forms I gave for KT are as follows (see page 122 and 128
of the Smith article):

*For all k >= 1 there exists n >= 1 such that the following holds. Let
T_1,...,T_n be finite trees such that for all i, |T_i| <= i. Then there
exists i_1 < ... < i_k such that each T_i_j is inf preserving embeddable
into T_i_j+1.*

Here |T| is the number of vertices of T. Note that the above comes from the
stronger form of KT which asserts that "every infinite sequence of trees
has an infinite subsequence of trees in which each tree is inf preserving
embeddable into each later tree." This strengthening comes for free from
the general theory of well-quasi-orderings.

I also considered the following finite form for the KT(k), which is in some
respects simpler:

**For all k >= 1 there exists n >= 1 such that the following holds. Let
T_1,...,T_n be finite trees whose vertices are labeled from {1,...,k},
where for all i, |T_i| <= i. Then there exists i < j such that each T_i is
inf and label preserving embeddable into T_j.**

NOW SET k = 6. I.e., consider the following sigma-0-1 sentence:

P = There exists n >= 1 such that the following holds. Let T_1,...,T_n be
finite trees whose vertices are labeled from {1,...,6}, where for all i,
|T_i| <= i. Then there exists i < j such that T_i is inf and label
preserving embeddable into T_j.

This is a pretty good, clean sigma-0-1 sentence.

THEOREM. P has a short proof in ID_2 but none in ID_1 (or pi-1-1-BI_0). In
fact, any such proof must have at least 2[1000] symbols (iterated
exponentiation). More philosophically, P has a short proof using standard,
but clearly IMPREDICATIVE methods, yet none with them.

(See Smith, 134-135). I haven't been back to it to see how much smaller
than 6 is needed.

In this recent work about n(k), we also have such phenomena. (see my
posting 12:11 AM 9/15/98).

THEOREM. Any proof that n(3) exists in EFA (exponential function
arithmetic) must have at least 2[1000] symbols. Any proof that n(4) exists
in sigma-0-1 induction must have at least 2[1000] symbols. There is a short
proof that n(4) exists in sigma-0-2 induction. There is a short  proof that
(for all k)(n(k)) exists in sigma-0-3 induction, and no proof whatsoever in
sigma-0-2 induction.

When this n(k) work is factored into the stuff about P above, I will likely
be able to cut down the number 6 quite a bit.

In my work on mathematical pi-0-2 sentences whose proofs require large
cardinals, this phenomenon is always present. However, my highest priority
has always been to strengthen the connections to normal mathematical ideas,
which is a fancy way of saying: make them more natural. So I have never
actually carried out something like this, although I have full confidence
that I can and will when it fits into my priorities.

In fact, the phenomenon doesn't really even require the step to finite
forms. I am often looking at statements of the form (for all dimensions
k)(blah blah blah), where blah blah blah is some explicitly pi-1-1
statement; even sometimes pi-1-2 statement. I usually know that the
statement is in fact provably equivalent to a pi-0-2 sentence, but I don't
have to actually perform the transformation - which is normally trivial and
standard. Then what seems to occur is this: one can fix k to be quite small
and show that

blah blah blah(k) has a short proof using large cardinals, but

blah blah blah(k) has no proof in ZFC using fewer than 2[1000] symbols
(iterated exponentiation).

This is morally certain. However: greater connections with normal
mathematical ideas (i.e., naturalness) continues to be my highest priority.