[FOM] 272:Sigma01/optimal

[Harvey Friedman]

This is a continuation of
http://www.cs.nyu.edu/pipermail/fom/2006-March/010244.html

There we clarified the proof given in the cited article by Smith of my
result concerning the statement
 
PROPOSITION. (SIX labels). There exists n >= 1 such that the following
holds. Let T_1,...,T_n be 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.

The result in question is this:

THEOREM. The Proposition can be proved in strictly finite mathematics.
However, any such proof in ACA_0 + Pi12-BI must use at least 2^[1000]
symbols.

CORRECTION: I stated

LEMMA 3. There is a primitive recursive function f:N^2 into N such that the
following holds. Let x be the godel number of a proof in ACA_0 + Pi12-BI of
a Sigma^0_1 sentence phi. There exists points y1 >' ... >' yp in <' such
that each |yi| <= |f(i)|, and phi has a witness <= p. Furthermore, f can be
presented in the calculus of primitive recursive functions by a presentation
with at most 2^1000 symbols.

I forgot to put x under the scope of x. This should read:

LEMMA 3. There is a primitive recursive function f:N^2 into N such that the
following holds. Let x be the godel number of a proof in ACA_0 + Pi12-BI of
a Sigma^0_1 sentence phi. There exists points y1 >' ... >' yp in <' such
that each |yi| <= |f(x,i)|, and phi has a witness <= p. Furthermore, f can
be presented in the calculus of primitive recursive functions by a
presentation with at most 2^1000 symbols.

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

HERE, we replace 6 labels by 3 labels in the Proposition. This is BEST
possible, because if we replace 6 labels by 2 labels, then the Proposition
becomes trivial, with a very small proof. This is because of the following
observation:

OBSERVATION. Let T1,T2,T3 be trees with vertices labeled from {1,2}, where
each T_i has at most i vertices. There exists 1 <= i < j <= 3 such that T_i
is inf preserving and label preserving embeddable into T_j.

So we consider

PROPOSITION. (THREE labels). There exists n >= 1 such that the following
holds. Let T_1,...,T_n be trees with vertices labeled from {1,2,3}, 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.

We sketch a proof of

THEOREM #. The above Proposition can be proved in strictly finite
mathematics. However, any such proof in ACA_0 + Pi12-BI must use at least
2^[1000] symbols.

The proof follows the previous one with 6 labels, but with a sharp
improvement on the "crucial combinatorial lemma 7" there. Lemma 7 asserts
the existence of a quite long sequence of 6 labeled trees with the relevant
bound, so that the "starting point" of an extremely long sequence of 2
labeled trees with the relevant bound, is large enough so as to encode the
proof theory of Sigma01 sentences in ACA_0 + Pi12-BI, for proofs of length
at most 2^[1000], in our usual way going back to my original finite forms of
Kruskal's theorem. We left 2 labels free for extending the "quite long
sequence" since the "quite long sequence" has length about 2^[1000] rather
than some much higher length associated with primitive recursion. For my
published account of "our usual way", see

H. Friedman, Internal finite tree embeddings, Reflections on the Foundations
of Mathematics: Essays in honor of Solomon Feferman, ed. Sieg, Sommer,
Talcott, Lecture Notes in Logic, volume 15, 62-93, 2002, ASL.

Here, in order to show that 3 labels suffice (best possible), we need to
construct a very long sequence of 3 labeled trees with the relevant bound,
so that the "starting point" of an extremely long sequence of unlabeled
trees with the relevant bound, is large enough so as to encode the proof
theory of Sigma01 sentences of ACA_0 + Pi12-BI, for proofs of length at most
2^[1000], in our usual way. Note that we are not left with any labels on the
trees extending our "very long sequence", since the "very long sequence"
will be of a length that is appropriately associated with far more than
primitive recursion.

First we start off with fourteen trees:

LEMMA 1. There exist T1,...,T14, with labels from {1,2,3}, with the
following properties.
i.  Each Ti has at most i vertices.
ii. There is no 1 <= i < j <= 10 such that Ti is inf preserving and label
preserving embeddable into Tj.
iii. Every Ti either has some vertex labeled 3, or at least two vertices
labeled 2. 

Proof: Take T1 to be the root labeled 3. Take T2 to be two connected
vertices labeled 2. Take T3 to be the root with 2, and two sons labeled 1.
Take T4 to have the vertices linearly ordered, with root 2 and higher
vertices 1. Take T5 to be the root with 1, and four sons with all 2's. Take
T6 to have root 1 with four sons, labeled 2,2,2,1, with the 1 having a son
labeled 1. Take T7 to have root 1, with sons 2,2,1, with the 1 having three
sons with 1's. Let T8 have root 1, with three sons 2,2,1, where the 1 has
two sons 1, and a grandson with 1. Let T9 have root 1, with three sons
labeled 2,2,1, with the 1 having a son, grandson, greatgrandson,
greatgreatgrandson, and greatgreatgreatgrandson, all labeled 1. Let T10,
T11, T12, T13, T14 result from T9 by successively chopping off the unique
terminal vertex labeled 1. QED

We are now free to use trees with exactly one 2, to bootstrap into Ackerman
level territory. For this purpose, we bring in

H. Friedman, Long Finite Sequences, Journal of Combinatorial Theory, Series
A 95, 102-144 (2001).

There we defined n(k) to be the longest length, n, of a sequence
x1,x2,...,xn drawn from {1,...,k}, such that the following holds. There is
no 1 <= i < j <= n/2 such that xi,...,x2i is a subsequence of xj,...,x2j.

In that paper, we showed that n(1) = 3, n(2) = 11, and gave a lower bound
for n(3). That lower bound was far more than, say, the usual binary
Ackermann function at 7100, which we write as A(7100). However, that lower
bound is not entirely safe for our purposes. However n(4) is incredibly
bigger, far bigger than, say, A(A(7100)), which is more than enough for what
we need. 

We don't really need to pack the punch into a single sequence using
consecutive blocks. For our purposes, we really only need the following
easier result.

LEMMA 2. There exists x1,x2,...,xp, where p = A(A(7000)), such that each xi
has length i+1, and no xi is a subsequence of xj.

Here's how we apply Lemma 2 to extend the T1,...,T14 of Lemma 1. Let
x1,...,xp, p = A(A(7000)), be given by Lemma 2.

Define 2 labeled trees S15,...,Sp+14 as follows. Let 15 <= i <= p+14. We
build Si from x_i-14 as follows.

First place i-8 linearly ordered vertices, v1,...,v_i-8, starting at the
root, with respective labels 1,...,1,2. These i-8 vertices are called the
SPINE of Si. The first i-13 of these vertices are called the ACTIVE SPINE of
Si. The last five of these vertices are called the INACTIVE SPINE of Si.

Let v1,...,vi-13 be the active spine of Si. Now, off of each vj in the
active spine of Si, put the four vertex tree Xj, all vertices labeled 1, as
follows. (The root of Xj will be the second of exactly two immediate
successors of vj in Si).

If xi(j) = 1, then Xj is linearly ordered. If xi(j) = 2, then Xj is a root
with 3 immediate successors. If xi(j) = 3, then Xj is a root with 2
immediate successors, one of them having 1 immediate successor. If xi(j) =
4, then Xj is a root with 1 immediate successor, which in turn has two
immediate successors.

Note that S15 has 15 vertices; i.e., |S15| = 15. For all 15 <= i <= p-14,
|Si+1| = |Si| + 5. Also note that Si has exactly one vertex labeled 2, which
is at the top of the spine of Si.

LEMMA 3. For all 15 <= i < j <= p+14, Si is not inf preserving and label
preserving embeddable into Sj.

Proof: Let i,j be a counterexample. The unique vertex labeled 2 in i must be
sent to the unique vertex labeled 2 in j. I.e., the top of the spine of Si
must be sent to the top of the spine of Sj. Hence the spine lees the top of
the spine, in Si, must be sent to the spine less the top of the spine, in
Sj. Since active spines consist of vertices with exactly two immediate
successors, the active spine of Si must be sent to the active spine of Sj,
in a direction preserving way. Of course, the inactive spine of Si must be
sent onto the inactive spine of Sj. Hence the corresponding four vertex
trees Xt in Si must be identical to the corresponding four vertex trees Xt
in Sj. From this, we see that the sequence x_i-14 is a subsequence of the
sequence x_j-14. This is a contradiction. QED

Now S15,...,Ap+14 is not quite what we want. Although S15 has 15 vertices,
already A16 has 20 vertices, instead of at most 19 vertices. The number of
vertices in the S's jumps by exactly 5 each time.

To fix this, we need to put four new trees Si*,Si**,Si***,Si**** in between
Si and Si+1. This is quite easy. Take these trees to have |Si|-1, |Si|-2.
|Si|-3, |Si|-4 vertices, respectively, by simply by shortening the inactive
spine of Si by 1 vertex each time (keeping the top vertex with label 2).

Thus we have shown the following.

LEMMA 4. There are 3 labeled trees T1,T2,...,Tp, where p = A(A(7000)), such
that each |Ti| <= i, each Ti has some vertex with label 3 or at least two
vertices with label 2, and for no 1 <= i < j <= p, is there an inf
preserving label preserving embedding from Ti into Tj.

As discussed earlier, we can then start an extremely long sequence of finite
trees at position p+1, starting with a tree with p+1 vertices, where all of
the vertices are labeled 1. This proves Theorem #.

To put this phenomenon in the same language as that of the "Long Fintie
Sequence" paper referenced above, we can define TR[k] as the longest
sequence T1,...,Tn of finite trees vertex labeled from {1,...,k}, where each
|Ti| <= i, and for no 1 <= i < j <= n, is Ti inf preserving and label
preserving embeddable into Tj.

TR[1] = 1, TR[2] = 2, TR[3] blows up well beyond predicativity as analyzed
by Feferman/Schutte.

You can of course study other growth rates, both higher and lower than the
identity function we have used.

Harvey Friedman  

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 272nd in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM
260. Pi01/simplification  12/3/05  3:11PM
261. Pi01/nicer  12/5/05  2:26AM
262. Correction/Restatement  12/9/05  10:13AM
263. Pi01/digraphs 1  1/13/06  1:11AM
264. Pi01/digraphs 2  1/27/06  11:34AM
265. Pi01/digraphs 2/more  1/28/06  2:46PM
266. Pi01/digraphs/unifying 2/4/06  5:27AM
267. Pi01/digraphs/progress  2/8/06  2:44AM
268. Finite to Infinite 1  2/22/06  9:01AM
269. Pi01,Pi00/digraphs  2/25/06  3:09AM
270. Finite to Infinite/Restatement  2/25/06  8:25PM
271. Clarification of Smith Article  3/22/06  5:58PM

Harvey Friedman