[FOM] 271:Clarification of Smith Article

[Harvey Friedman]

In http://www.cs.nyu.edu/pipermail/fom/2006-March/010233.html I cited the
following result (Theroem 2) from

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, Scedrov, Simpson, pp. 119-136, 1985.

THEOREM 1. 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 2. Theorem 1 can be proved in strictly finite mathematics. However,
any such proof in ACA_0 + Pi12-BI must use at least 2^[1000] symbols.

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

In light of the formulations in Rathjen and Weiermann (see below), here we
use ACA_0 + Pi12-BI, instead of the Pi12-TI_0 there.

There are some typos and unclear points at the end of the Smith article,
where this result is proved.

First of all, the paper Friedman and Pearce never appeared, but the
following paper appeared instead:

H. Friedman and M. Sheard, Elementary descent recursion and proof theory,
Annals of Pure and Applied Logic 71 (1995), pp. 1-45.

This paper has the cited material - with some different notation - except
for the needed connection between ACA_0 + Pi12-BI and ATI(<'), where <' is
the standard notation system for the proof theoretic ordinal
theta_capitalomega_0(0).

We want to clarify two aspects of the proof of Theorem 2 above in the Smith
paper. Theorem 2 above appears as Theorem 15 in Smith. Actually, in the
statement of Theorem 15, and elsewhere in Section 4 of Smith, psi_Q(1)
should be psi_Q(2).

Let us first extract what we need to know about the proof theory of
ACA_0 + Pi12-BI. The theory has been analyzed in terms of the proof
theoretic ordinal theta_capitalomega_0(0). E.g., look at

Title: Proof-theoretic investigations on Kruskal's theorem.
Authors: M. Rathjen and A. Weiermann.
Annals of Pure and Applied Logic, 60, 49--88 (1993).

We need some pretty crude information about this analysis. The following is
enough.

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.

In the above, | | is the norm function on the notation system, as also used
in the reference 

#) 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.

Now let <* be the natural well ordering of the first epsilon number after
theta_capitalomega_0(0).

Using the arguments in Smith or #), we easily obtain the following from
Lemma 3:

LEMMA 4. 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| <= (2^(1000x))+i and phi has a witness <= p.

We now apply Lemma 4 to the Sigma^0_1 sentence: Theorem 1.

LEMMA 5. Let x be the godel number of a proof in ACA_0 + Pi12-BI of Theorem
1. There exist points y1 >* ... >* yp in <* such that each |yi| <=
(2^(1000x))+i and phi has a witness <= p.

Using the arguments in Smith or #), we can use tree representations of the
y's to obtain the following.

LEMMA 6. Let x be the godel number of a proof in ACA_0 + Pi12-BI of Theorem
1. There exist {1,2} labeled trees T1,...,Tp such that each Ti has at most
(2^(1000x))+i vertices, and for no i < j is Ti inf preserving and label
preserving embeddable into Tj, and Theorem 1 has a witness <= p.

Define 2^[n] as an exponential stack of 2's of height n.

CRUCIAL COMBINATORIAL LEMMA 7. There exist {2,3,4,5} labeled trees
S1,...,Sq, q = 2^[1008], such that each Si uses a label from {3,4,5,6}, each
Si has at most i vertices, and for no i < j is Ti inf preserving and label
preserving embeddable into Tj.

We will postpone the poof of Lemma 7. The following is immediate from Lemmas
6 and 7:

LEMMA 8. Let x be the godel number of a proof in ACA_0 + Pi12-BI of Theorem
1. Suppose x <= 2^[1006]. There exist {1,...,6} labeled trees T1,...,Tp such
that each Ti has at most i vertices, and for no i < j is Ti inf preserving
and label preserving embeddable into Tj, and Theorem 1 has a witness <= p.

But if we read Theorem 1, then the conclusion of Lemma 8 is absurd. Hence
Theorem 1 has no proof in ACA_0 + Pi12-BI with godel number x. Hence Theorem
1 has no proof in ACA_0 + Pi12-BI with fewer than 2^[1000] symbols.

It remains to prove Lemma 7.

PROOF OF LEMMA 7. This appears as essentially Lemma 21 in Smith. There are
some typos and slight inaccuracies, and so we correct the argument.

Let S1 be the tree with only the root, labeled 6. Let S2 be the tree with
two vertices, both labeled 5. Let S3,...,S26 be all trees with 3 linearly
ordered vertices, all labeled from {2,3,4}, but not all the same. Let
S27,...,S1330 be nonisomorphic trees consisting of a root and 29 immediate
successors, where the vertices are labeled from {2,3,4}, so that not all
vertices are 2. The number of 29 element multisets from {2,3,4} is 29 x 15 =
435. This is multiplied by 3 for the root, and then we delete 1, which
results in 1304 trees.

We will define S1331,...,Sq, where q = 2^[1008]. Each tree has a root
labeled 1, and two sons. The left son is labeled 3, and the right son is
labeled 2. Off of each of these two sons is a long linearly ordered chain of
vertices. All of the vertices off of the left son are labeled 3, and all of
the vertices off of the right son are labeled from {1,2}.

Clearly S1 does not go into any later tree, since 6 is not used later. Also,
since 5 is not used later, S2 also does not go into any later tree.
S3,...,S26 can't go into any of S27,...,S1330 since the latter have no paths
of length 3. Also S3,...,S26 can't go into any of S1331,...,Sq because the
roots of the latter are labeled 1, and on the left we have only 3's, and on
the right we have only 1'2 and 2's. The S27,...,S1330 can't go into any
S1331,...,Sq because of splitting.

We start with the left chain off the root being of length 1008. So far we
have 1010 vertices. We can add 23 additional vertices off of the right son,
and use any labeling from {1,2}, provided not all 1's. In this way, we have
2^23 trees.  

For the next set of trees, we make the left chain of one less length - 1007.
Then we have room for (at least) 2^2^23 more vertices.

We can continue in this way, for another 1008 stages, for a total number of
trees more than the 2^[1000] required. QED


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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 271st 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

Harvey Friedman