FOM: 22:Finite Trees/Impredicativity

[Harvey Friedman]

This is the 21st in a series of self contained postings to fom
covering a wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM

A complete archiving of fom, message by message, is available at
http://www.math.psu.edu/simpson/fom/
Also, my series of self contained postings (only) is archived at
http://www.math.ohio-state.edu/foundations/manuscripts.html

We regard this as a very strong improvement on the work in "Finite trees
and impredicativity," 5/24/97, that is currently on my website. This will
be replaced by a later version (with a later date) in a few weeks.

We present new finite tree theorems (in pi-0-2 form) which can only be
proved by impredicative methods. The methods are not beyond ZFC - that will
be the subject of a new round of improved results in later postings within
a month. They are proved in pi-1-1-CA; or in some cases in pi-1-2-TI. The
former is stronger than the latter in the sense that the pi-1-1
consequences are properly more inclusive, even though the latter is not a
subsystem of the former.

These new tree theorems follow fairly easily from various forms of
Kruskal's tree theorems (or Higman's earlier theorems which are closely
related). However, they are in a sense more elemental, in that they concern
only the structure of a SINGLE TREE. There are clearly of independent
interest. This was not clearly the case for our original finite forms of
Kruskal's theorem.

We consider finite rooted trees, which are finite posets with a least
element, in which the set of predecessors of any vertex are linearly
ordered. The valence of a finite rooted tree is the least k such that every
vertex has at most k immediate successors.

There is the obvious notion of inf. We are especially interested in inf
preserving embeddings from T_1 into T_2. This is a one-one map h such that
h(inf(x,y)) = inf(h(x),h(y)).

We also consider omega trees. These are infinite rooted trees, which are
infinite posets with a least element, in which the set of predecessors of
any vertex are linearly ordered and finite, and also where every vertex has
at most finitely many immediate successors.

The most basic form of Kruskal's theorem:

THEOREM 1. For all finite rooted trees T_1,T_2,..., there exists i < j and
an inf preserving embedding from T_i into T_j.

Here is our version involving only a single tree. The height of a vertex in
a tree (finite or not) is the number of predecessors. Thus the height of
the root is 0. We write T|<=i for the subtree consisting of all vertices of
height <= i. We write T|i for the set of all vertices of height exactly i.

THEOREM 2. For all omega trees T, there exists i and an inf preserving
embedding of T|<=i into T, which moves every element of T|i.

THEOREM 3. Theorems 1 and 2 are provably equivalent in RCA_0. They are
equivalent to pi-1-1 reflection on pi-1-2-TI_0 within RCA_0, or that
phi_capitalomega^omega(0) is well ordered.

Now for the finite version.

THEOREM 4. Let n >> k and T be a finite rooted tree of height n and valence
<= k. There exists i and an inf preserving embedding of T|<=i into T, which
moves every element of T|i.

THEOREM 5. Theorem 4 is provably equivalent in EFA (exponential function
arithmetic) to the 1-consistency of pi-0-1-TI_0, or EFA +
ATI(<phi_capitalomega^omega(0)). The growth rate of >> represents a
provably recursive function of ATI(phi_capitalomega^omega(0)) that
eventually dominates every provably recursive function of
ATI(<phi_capitalomega^omega(0)).

We now consider trees with vertices labeled from {1,...,r}. A stronger form
of Kruskal's theorem (due to Kruskal) is as follows:

THEOREM 6. For all r >= 1 and finite rooted trees T_1,T_2,... labeled from
{1,...,r}, there exists i < j and an inf and label preserving embedding
from T_i into T_j.

We can extend Theorems 2-5 for such labeled trees as follows.

THEOREM 7. For all r >= 1 and omega trees T labeled from {1,...,r}, there
exists i and an inf and label preserving embedding of T|<=i into T, which
moves every element of T|i.

THEOREM 8. Theorems 6 and 7 are provably equivalent in RCA_0, even for any
fixed r.

THEOREM 9.  Let n >> k,r and T be a finite rooted tree of height n and
valence <= k, labeled from {1,...r}. There exists i and an inf and label
preserving embedding of T|<=i into T, which moves every element of T|i.

THEOREM 10. Theorem 9 is provably equivalent in EFA (exponential function
arithmetic) to the 1-consistency of pi-0-1-TI_0, or EFA +
ATI(<phi_capitalomega^omega(0)). The growth rate of >> represents a
provably recursive function of ATI(phi_capitalomega^omega(0)) that
eventually dominates every provably recursive function of
ATI(<phi_capitalomega^omega(0)).

I introduced the gap condition on embeddings between trees with labels. In
this context of labels from {1,...,r}, the gap condition is formulated as
follows. Let T1,T2 be trees labeled from {1,...,r}, y be an immediate
successor of x in T1, and h be inf and label preserving from T1 into T2.
Then h(y) is a successor of h(x) in T2, but not necessarily an immediate
successor. The successors of h(x) along the path from h(x) to but not
including h(y) is called a gap. The gap condition requires that the labels
along this gap be numerically <= the label of h(y).

THEOREM 11. For all r >= 1 and finite rooted trees T_1,T_2,... labeled from
{1,...,r}, there exists i < j and an inf and label preserving embedding
from T_i into T_j with the gap condition.

We can extend Theorems 2-5 for such labeled trees as follows.

THEOREM 12. For all r >= 1 and omega trees T labeled from {1,...,r}, there
exists i and an inf and label preserving embedding of T|<=i into T with the
gap condition, which moves every element of T|i.

THEOREM 13. Theorems 6 and 7 are provably equivalent in RCA_0, even for any
fixed r. They are provably equivalent to pi-1-1 reflection on pi-1-1-CA_0,
and also phi_capitalomega_omega(0) is well ordered.

THEOREM 14.  Let n >> k,r and T be a finite rooted tree of height n and
valence <= k, labeled from {1,...r}. There exists i and an inf and label
preserving embedding of T|<=i into T with the gap condition, which moves
every element of T|i.

THEOREM 15. Theorem 14 is provably equivalent in EFA (exponential function
arithmetic) to the 1-consistency of pi-1-1-CA_0, or EFA +
ATI(<phi_capitalomega_omega(0)). The growth rate of >> represents a
provably recursive function of ATI(phi_capitalomega_omega(0)) that
eventually dominates every provably recursive function of
ATI(<phi_capitalomega_omega(0)).

Structure can be added to the trees without changing any of the results.
Here structure is a technical term which means that the set of all
immediate successors of every vertex is assigned a linear ordering. One
requires structure preservation of the embeddings. This is a setup
originally due to Kruskal.