FOM: 27:Finite Trees/Predicativity:Sketches

Wed Jan 13 06:54:08 EST 1999

This is the 27th 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
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized Functions/Large Cardinals

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 give some sketches for the results presented in #22. In one case we have
to correct the formulation of the result. This posting is self contained.
These results represent and new level of naturalness and simplicity for
finite theorems that can only be proved by impredicative methods.

1. TREES WITH LABELS

We consider finite trees, in the sense of finite posets with a least
element, in which the set of predecessors of any vertex are linearly
ordered. The valence of a finite 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)).

The most basic form of Kruskal's theorem:

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

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

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

In the 1980's we considered a number of finite forms of Theorems 1.1 and
1.2, including the following. The height of a finite rooted tree is one
less than the length of the longest sequence from the root to a vertex.
Thus the finite rooted trees of height 0 consist of just the root.

THEOREM 1.3. For all k,n >= 1 there exists r >= 1 such that the following
holds. Let T_0,...,T_r be trees labeled from {1,2,...,n}, with valence <=
k, where the height of each T_i is i. Then there exists i < j and an inf
and label preserving embedding of T_i into T_j.

We proved the following:

THEOREM 1.4. Theorem 1.3 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 give three new finite versions involving only a single tree. The
versions differ only slightly, and the reader may prefer one or the other.

The height of a vertex in
a finite tree is the number of its strict 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.
We write T|>i for the set of all vertices of height > i.

THEOREM 1.5.  For all k,n >= 1 there exists r >= 1 such that the following
holds. Let T be a tree of height r and
valence <= k, labeled from {1,...,n}. There exists 0 <= i <= r and an inf
and label
preserving embedding of T|<=i into T, which moves every element of T|i.

THEOREM 1.6. For all k,n >= 1 there exists r >= 1 such that the following
holds. Let T be a tree of height r and
valence <= k, labeled from {1,...,n}. There exists 0 <= i <= r and an inf
and label
preserving embedding of T|<=i into T, which maps T|i into T|>i.

THEOREM 1.7. For all k,n >= 1 there exists r >= 1 such that the following
holds. Let T be a tree of height r and
valence <= k, labeled from {1,...,n}. There exists 0 <= i < j <= r and an
inf and label
preserving embedding of T|<=i into T|<=j, which maps T|i into T|j.

Obviously 1.7 implies 1.6 implies 1.5.

We now wish to show that Theorems 1.3, 1.5, 1.6, and 1.7 are all equivalent.

Proof sketch of 1.3 implies 1.7: Assume Theorem 1.3. Let k,n >= 1. Let r be
such that 1.3 holds for r,k,2n. T be a tree of height r and valence <= k
with labels from {1,2,...,n}. Consider the sequence of trees
T|<=0,T|<=1,...,T|<=r. Double the number of labels in these trees so that
you can tell whether or not a node in T|<=i lies in T|i by its label. By
1.3, there exists i < j such that T|<=i is inf and label preserving
embeddable into T|<=j, as modified with these extra labels. Therefore this
embedding must map T|i into T|j. QED.

Proof sketch of 1.5 implies 1.3: Assume 1.5, and let k,n >= 1. Let r,k,n+5
be as given by 1.5.

Now fix T_0,...,T_r, where each T_i has height i and valence <= k. We now
construct an appropriate single tree T of valence <= k, with labels
{1,...,n+5}. We then argue that since T obeys the conclusion of 1.5, then
T_0,...,T_r obeys the conclusion of 1.3. Wlog, k,r >= 3.

First put the root down with label n+1, and then two successors of the
root, x_0,y_0. Let x_0 have label n+2 and y_0 have label n+3. Then extend
x_0 by a series of r+1 successors, all with label n+4. Call these nodes
x_1,...,x_r+1. And extend y_0 by a series of r successors, all with label
n+5. Call these nodes y_1,...,y_r.

Place the tree T_i above x_i so that the root of T_i becomes the second
successor of x_i (the other successor being x_i+1).

Place the tree T_i+1 above y_i so that the root of T_i+1 becomes the second
successor of y_i (the other successor being y_i+1).

This completes the construction of the tree T. Note that one copy of T_0 is
placed in T, and two copies of each T_i, i >= 1, is placed in T.

Also note the following. On the x_0 side of T, the copy of the tree T_i has
root at level i+2 (level 0 is the root), and highest vertices at level
2i+2. And on the y_1 side of T, the copy of the tree T_i, i >= 1, has root
at level i+1, and highest vertices at level 2i+1. So highest vertices of
trees appear at every level from 2 through 2r+2. And 2r+2 is the highest
level in T.

Now let i >= 0 and h be an inf and label preserving embedding from T|<=i
into T which moves every element of T|i. By considering the labels, clearly
h is the identity on the root of T and on x_0 and y_0. So i >= 2. Hence i
is the level of the highest vertex of some copy of some T_j, 0 <= j <= r.
Therefore h moves some vertex of T_j.

We first assume that this T_j is placed above x_j. If h fixes x_j then
h(x_j+1) must lie at or above x_j+1, in which case h maps this T_j into
this T_j, and so is the identity on T_j, which is a contradiction.

Hence h moves x_j. It is clear that h(x_j) = x_j' for some j' > j. In fact,
by splitting, j < j' <= r. Hence h(x_j+1) must lie at or above x_j'+1. It
is now clear that the root of T_j must be sent into T_j' by h. Therefore, h
yields an inf and label preserving embedding from T_j into T_j'.

The case where T_j is placed above y_j-1 is handled similarly. QED.

2. FULL TREES WITH LABELS

We give some additional finite forms involving a single finite rooted tree
with labels. A finite tree is said to be full if and only if all maximal
nodes have the same height, and all nonmaximal nodes have the same
splitting. The following three finite forms are simply the specializations
of those given in section 1 to full rooted trees:

THEOREM 2.1.  For all k,n >= 1 there exists r >= 1 such that the following
holds. Let T be a full tree of height r and
valence k, labeled from {1,...,n}. There exists 0 <= i <= r and an inf and
label
preserving embedding of T|<=i into T, which moves every element of T|i.

THEOREM 2.2. For all k,n >= 1 there exists r >= 1 such that the following
holds. Let T be a full tree of height r and
valence k, labeled from {1,...,n}. There exists 0 <= i <= r and an inf and
label
preserving embedding of T|<=i into T, which maps T|i into T|>i.

THEOREM 2.3. For all k,n >= 1 there exists r >= 1 such that the following
holds. Let T be a full tree of height r and
valence k, labeled from {1,...,n}. There exists 0 <= i < j <= r and an inf
and label
preserving embedding of T|<=i into T|<=j, which maps T|i into T|j.

We wish to show that these Theorems are all equivalent to Theorem 1.3. It
suffices to show that 2.1 implies 1.5.

Proof sketch of 2.1 implies 1.5: Assume 2.1. Let k,n >= 1. Let r,k,n+1 be
as given by 2.1. Let T be a tree of height r and valence at most k, with
labels from {1,...,n}. Let T' be the full tree of height r and valence k,
with labels from {1,...,n+1} constructed as follows. First add new
immediate successors to every nonmaximal node in T so as to ensure that all
nonmaximal nodes in T have exactly k immediate successors. Then extend all
maximal nodes in T of height < r in order to complete the construction. All
new nodes are to have the label n+1.

By 2.1, let h be an inf and label preserving embedding from T'|<=i into T'
which moves every element of T'|i, where 0 <= i <= r. Since T is an initial
segment of T', we see that h maps T|<=i into T by consideration of the
labels. And obviously h moves every element of T|i. QED

3. TREES WITH NO LABELS

We now consider the versions of Theorems 1.5 - 1.7 without labels. This is
equivalent to setting n = 1.

Theorems 1.5 - 1.7 taken literally without labels are trivial. Just set r =
1 and use i = 0. Henceforth, we insist that i >= 1:

THEOREM 3.1.  For all k >= 1 there exists r >= 1 such that the following
holds. Let T be a tree of height r and
valence <= k. There exists 1 <= i <= r and an inf
preserving embedding of T|<=i into T, which moves every element of T|i.

THEOREM 3.2. For all k >= 1 there exists r >= 1 such that the following
holds. Let T be a tree of height r and
valence <= k. There exists 1 <= i <= r and an inf
preserving embedding of T|<=i into T, which maps T|i into T|>i.

THEOREM 3.3. For all k >= 1 there exists r >= 1 such that the following
holds. Let T be a tree of height r and
valence <= k. There exists 1 <= i < j <= r and an inf
preserving embedding of T|<=i into T|<=j, which maps T|i into T|j.

We will show that Theorems 3.2 and 3.3 are provably equivalent to Theorem
1.5, whereas Theorem 3.1 is still provable in EFA (exponential function
arithmetic). NOTE: In #22, we erroneously stated that 3.1 was also
equivalent.

Proof sketch of 3.1: Let k >= 1 and let T be a tree of height 2 and valence
<= k. If T has more than one node of height 1 then there are obviously
automorphisms of T|<=1 which move every element of T|1. And if T has
exactly one node, x, of height 1 then we can map T|<=1 into T by the
identity on the root, and x to any node strictly higher than x. QED

Let T be a finite tree of valence <=k with labels from {1,...,n}.

We define T' from T as follows. Let x be a vertex in T with label 1 <= i <=
n. Add (4kni)^2 new children of x with no children. Add 2kn(n-i+1) new
children of x with exactly one child each. Finally, in the case where x is
the root, throw in an additional (8kni)^8 children without any children.
Now remove all labels. This completes the construction of T'. [These
algebraic expressions are overkill, of course].

Note that hgt(T') = hgt(T)+2.

LEMMA 3.4. h is an inf, label, and root preserving map from T|i-2 into T.

Proof: Let x in T|i-2. Then x has at least two children. Hence h(x) in T.
Let the label of h(x) be j. The number of children of x with at least one
child is at least 2kn(n-i+1), and the number of children of h(x) with at
least one child is at most j + 2kn(n-j+1). Since j < 2kn, we see that i >=
j. The number of children of x is at least (4kni)^2 and the number of
children of h(x) is at most (4knj)^2 + 2kn(n+1) + k. Hence i <= j.
Therefore i = j. Finally, h must preserve the root because of its specially
large valence.

LEMMA 3.5. Let x,h(x) in T|i-2. Then there is a grandchild y of x such that
y,h(y) in T|i.

Proof: By Lemma 3.4, x and h(x) have the same label 1 <= i <= n. Any child
of x with exactly one child each must be sent at or above a child of h(x)
or at or above a
new child of h(x) with exactly one child. By counting, some child x' of x
with exactly one child is sent at or above a new child x'' of h(x) with
exactly one child. Hence the unique child of x' is sent to the unique child
of x'', and these respective grandchildren of x,h(x) lie in T|i.

LEMMA 3.6. For all x in T|i-2, h(x) in T|>i-2.

Proof: By Lemma 3.5, h(x) notin T|i-2. Hence h(x) in T|>i-2.

LEMMA 3.7. 2 <= i <= hgt(T)+2.

Proof: Since h is root preserving, i = 1 is impossible. Now use i >= 1.

LEMMA 3.8. h is an inf and label preserving embedding from T|<=j into T
which maps T|j into T|>j, where 0 <= j <= hgt(T).

Proof: By Lemmas 3.6 and 3.7, we can take j = i-2.

It is now clear how to derive 2.2 from 3.2. Recall that 2.2 implies 1.5.

Strictly speaking, we need to show that 1.5 implies 3.3 since 3.3 uses 1
and 2.3 uses 0. The proof that 1.5 implies 2.3 is easily modified by using
an additional label for the root.

4. STRUCTURED TREES

Structured finite rooted trees were also considered by Kruskal. Here a
linear ordering is assigned to all of the immediate successors of every
node. A structure preserving embedding is an embedding which preserves
structure. All of the results go through for structured trees where the
embeddings are required to preserve structure, except for the proof in EFA
of Theorem 3.1. In fact, in the structured context, 3.1 implies 3.2 for the
following reason. Suppose T is a structured finite rooted tree and h is an
inf and structure preserving embedding from T|<=i into T. Then for all x in
T|<=i, either h(x) = x or the height of h(x) is greater than the height of
x.

5. GAP CONDITION

We introduced the gap condition on embeddings between finite rooted trees
with finitely many labels in the 1980's. We say that an inf and label
preserving embedding h from T_1 into T_2 has the gap condition if and only
if for all x,y if y is an immediate successor of x in T_1, then the labels
of the nodes that are both strictly above h(x) and strictly below h(y) must
be numerically at least the label of y. [I also stated the gap condition in
the more general context of arbitrary labels].

The results of sections 1 and 2 can be reworked for gap condition
embeddings. The exactly analogous equivalences hold. The relevant formal
system is pi-1-1-CA_0, and the relevant proof theoretic ordinal is
phi_capitalomega_omega(0). Also structure can be added to the mix without
change.

6. GROWTH RATES AND LARGE INTEGERS

As discussed in posting #24, we can specify extremely large integers
(predicatively unfeasible in the sense of #24), by fixing k (or both k and
n) to be very small integers, and take the least n such that the conclusion
holds. We can do this for every new finite form discussed here (except
Theorem 3.1). Exact values of k and n that suffice need to be checked
carefully.