[FOM] a very exciting claim 1

[Harvey Friedman]

On 3/21/06 1:05 PM, "Gabriel Stolzenberg" <gstolzen at math.bu.edu> wrote:

> 
>  Andrej Bauer (March 20) quotes Harvey Friedman (March 18)
> saying:
> 
>>> 4. Examples where the known proof is nonconstructive, and where
>>> one can give a constructive proof, but it is known that all
>>> constructive proofs are grotesque (e.g., extremely long, or
>>> extremely unpleasant, etc.).
> 
>  All???  How can one know that all constructive proofs of some
> statement are grotesque (in the sense described or any other)?
> 
>  This is one of the most exciting claims I've ever heard.
> 

EXECUTIVE SUMMARY: Go to Corollary 7.

*************

Recall the famous Kruskal Theorem:

THEOREM 1. Let T_1,T_2,... be finite trees. There exists i < j such that T_i
is topologically embedable into T_j.

Obviously, one can replace topological embeddability by Kruskal
embeddability - which is inf preserving embeddability:

THEOREM 2. Let T_1,T_2,... be finite trees. There exists i < j such that T_i
is inf preserving embeddable into T_j.

I spoke to Bishop about this theorem, and sent him the simplest known proof,
due to Nash-Williams. I think I sent it also to Stolzenberg, but I am not
sure. In any case, Bishop (and Stolzenberg) confirmed that the proof is
rather far from constructive.

Here is a semifinite form of Kruskal's theorem that I didn't emphasize in
the old days. 

THEOREM 3. Let T_1,T_2,... be finite trees whose sizes (number of vertices)
are linearly bounded. There exists i < j such that T_i is inf preserving
embeddable into T_j.

Theorem 3 can be argued to fall within the "purview of predicativity", since
the conclusion is finitary. Well known CLASSICAL manipulations show that it
is Pi02.  

We know that Theorems 1,2,3 cannot be proved in a quite strong system called
Pi12-TI_0, but can be proved in Pi12-TI. Thus under the Feferman/Schutte
analysis of predicativity, Theorem 3 is not provable predicatively.

Now here is my original finite form of Kruskal's theorem.

THEOREM 4. For all k >= 1 there exists n >= 1 such that the following holds.
Let T_1,...,T_n be finite trees, where each T_i has at most i+k vertices.
There exists 1 <= i < j <= n such that T_i is inf preserving embeddable into
T_j.

We also know that Theorem 4 cannot be proved in Pi12-TI_0, but can be proved
in Pi12-TI. 

Theorem 1 was also proved by Kruskal for finite trees with labels on the
vertices. A particular case of vertex labeling is where the labels are drawn
from a fixed finite set. The conclusion is "inf preserving and label
preserving embeddable".

So we arrive at the (a bit) stronger

THEOREM 5. Let S be a finite set of labels. For all k >= 1 there exists n >=
1 such that the following holds. Let T_1,...,T_n be finite trees with
vertices labeled from S, where each T_i has at most i+k vertices. There
exists 1 <= i < j <= n such that T_i is inf preserving and label preserving
embeddable into T_j.

Now that we have these labels, we might as well get rid of the k:

THEOREM 6. Let S be a finite set of labels. There exists n >= 1 such that
the following holds. Let T_1,...,T_n be finite trees with vertices labeled
from S, where each T_i has at most i vertices. There exists 1 <= i < j <= n
such that T_i is inf preserving and label preserving embeddable into T_j.

Theorem 6 is not provable in Pi12-TI_0.

Now for the high point of

R.L. Smith, The Consistency Strengths of Some Finite Forms of the Higman and
Kruskal Theorems, in: Harvey Friedman's Research on the Foundations of
Mathematics, Studies in Logic and the Foundations of Mathematics, volume
117, ed. Harrington, Morley, Scedorv, Simpson, pp. 119-136, 1985.

COROLLARY 7. There exists n >= 1 such that the following holds. Let
T_1,...,T_n be finite trees with vertices labeled from {1,...,6}, where each
T_i has at most i vertices. There exists 1 <= i < j <= n such that T_i is
inf preserving and label preserving embeddable into T_j.

THEOREM 8. Corollary 7 can be proved in strictly finite mathematics.
However, any such proof in Pi12-TI_0 must use at least 2^[1000] symbols.

Here 2^[1000] is an exponential stack of 2's of height 1000.

In a followup posting, I will give some more variants.

Harvey Friedman