FOM: 24:Predicatively Unfeasible Integers

[Harvey Friedman]

This is the 24th 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

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

This posting is related to 19, 21, and 22.

***NOTE: In posting 22, Theorems 2,4,7,9, I forgot to require that i > 0.***

The incomprehensibly large integers from 19 and 21 are captured well within
Peano Arithmetic - they need pi-0-3 induction, as indicated there. We have
been looking for a comparably compelling example of a large integer which
can be captured only with some weak use of uncountable sets. More
specifically, a large integer which cannot be captured predicatively. We
give a number of examples which are closely related to the examples from 19
and 21; indeed, some of them can be viewed as an elaboration on n(3) from
19 and 21. However, it must be conceded that none are quite of the truly
"high school" flavor of n(3).

Informally, we say that an integer n is predicatively feasible if and only
if there is an algorithm M which produces an integer >= n, and where there
is a feasible predicative proof that M does produce an integer. We say that
n is predicatively unfeasible otherwise.

We take the following working condition *) on n as sufficient for
establishing that n is predicatively unfeasible:

*) there is no Turing machine TM which produces an integer >= n at the
empty tape, together with a proof in P that TM produces an integer at the
empty tape, with at most 2^100 symbols.

Here P is one of the standard formalizations of predicative mathematics,
such as Feferman's original IR, perhaps augmented by abbreviations. The
following condition will imply *) if we use any formalization P of this
kind:

**) there is no Turing machine TM which produces an integer >= n at the
empty tape, together with a proof in ATR_0 that TM produces an integer at
the empty tape,  with at most A[5] symbols.

Here A[5] is the Ackerman function at 5. This number is of course overkill,
but we do want to dominate all possible issues of abbreviation and
formalization. Recall that A[5] was used as a working criterion for
incomprehensibly large in "Long Finite Sequences" in
http://www.math.ohio-state.edu/foundations/manuscripts.html.

We now give several examples of predicatively unfeasible integers connected
with postings 19, 21, and 22.

1. THE ORIGINAL EXAMPLES FROM THE 1980's

My original finite form of Kruskal's theorem was:

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

I claimed that the least possible n was a gigantic number for very small k
such as even 11, but didn't publish a specific result. In retrospect, it
seems that in essence I was proving that for k = 11 the least such n obeys
**).

Rick Smith, "The consistency Strength of some finite forms of the Higman
and Kruskal theorems," in "Harvey Friedman's Research on the Foundations of
Mathematics", North-Holland, 1985, did publish one of my arguments
concerning some related statements. In essence, there is a sketch of the
following result. Consider

for all k >= 1 there exists n such that the following holds. Let
T_1,...,T_n be finite rooted trees with 6 labels such that each T_i has at
most i vertices. Then there exists i < j such that T_i is inf and label
preserving embeddable into T_j.

Then the least such n cannot be captured in pi-1-2-TI_0 by a proof with at
most 2^[100] symbols. This is a stronger condition than **).

2. FROM POSTING 22: unlabeled trees

***NOTE: In Theorems 2,4,7,9, of posting 22, I forgot to require that i > 0.***

Recall the following from posting 22:

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

We claim that k = 9 gets us to predicative unfeasibility. Probably this can
be lowered. I.e., let n be the height of the tallest rooted tree T of
valence <= 9 such that there is no inf preserving embedding from any
truncation T|<=i into T which moves every element of T|i, i > 0.

THEOREM 2.2. n has property **).

3. FROM POSTING 22: uniform binary trees with labels

There is another version of Theorem 2.1 that many may prefer. It involves
looking at only uniform trees. A uniform tree is a tree such that

i) all vertices other than the leaves have the same valence (number of
immediate successors);
ii) all leaves have the same height.

Finite uniform trees are very special and natural objects. Any two of the
same height are isomorphic. But obviously any one is inf preserving
embeddable into any other if and only if the height of the first is <= the
height of the second. This is of course not true when labels are involved.

Here is a variant of Theorem 2.1 for uniform trees.

THEOREM 3.1. Let n >> k,p and T be a finite k-ary uniform tree with p
labels. There exists i and an inf and label preserving embedding of T|<=i
into T, which moves every element of T|i.

THEOREM 3.2. Theorem 3.1 is provably equivalent, over EFA, to the
1-consistency of pi-1-2-TI_0.

We claim that setting k = 2 and p = 9 gets us to predicative unfeasibility.
Probably 9 can be lowered. I.e., let n be the height of the tallest uniform
binary tree T with 9 labels such that there is no inf and label preserving
embedding from any trunction T|<=i into T which moves every element of T|i.

THEOREM 3.3. n is predicatively unfeasible.

4. FROM POSTINGS 19 AND 21: unlabeled trees

Recall that a finite rooted tree is a finite poset with a least element in
which the set of predecessors of every vertex is linearly ordered. A finite
forest is a finite poset in which the set of predecessors of every vertex
is linearly ordered. An inf preserving embedding of one finite forest into
another is a one-one map h such that h(inf(x,y)) = inf(h(x),h(y)), where if
one side of the equation is undefined then both sides of the equation are
undefined.

Let T be a finite rooted tree and i <= j. We write T[i,j] for the forest of
vertices whose number of predecessors together with itself is in the
interval [i,j]. So T[1,2] consists of the root and all of its immediate
successors.

Here is a new kind of pi-0-2 independence result:

THEOREM 4.1. Let n >> k and T be a tree of height n with valence <= k. Then
there exists 1 <= i < j <= n/2 such that T[i,2i] is inf preserving
embeddable into T[j,2j].

THEOREM 4.2. Theorem 4.1 is provably equivalent, over EFA, to the
1-consistency of pi-1-2-TI_0.

We claim that setting k = 5 gets us to predicative unfeasibility. I.e., let
n be the height of the tallest rooted tree T of valence <= 5 such that
there is no inf preserving embedding from any T[i,2i] into another T[j,2j].

THEOREM 4.3. n has property **).

5. FROM POSTINGS 19 AND 21: uniform binary trees with labels

My favorite way of doing this might well be the following, since it is
closest in spirit to the tantalizing high school n(3).

THEOREM 5.1. Let n >> k,p and T be a uniform k-ary tree of height n with p
labels. Then there exists 1 <= i < j <= n/2 such that T[i,2i] is inf and
label preserving embeddable into T[j,2j].

THEOREM 5.2. Theorem 5.1 is provably equivalent, over EFA, to the
1-consistency of pi-1-2-TI_0.

We claim that setting k = 2 and p = 3 gets us to predicative unfeasibility.
I.e., let n be the height of the tallest uniform binary tree with 3 labels
such that there is no inf and label preserving embedding from any T[i,2i]
into another T[j,2j].

THEOREM 5.3. n has property **).

NOTE: If we replace "binary" by "unary", then this is exactly the precious
n(3), which is incomprehensibly large but clearly predicatively feasible.

6. OTHER RESULTS

One can also impose the gap condition, which drives things up higher. But
the main point here is to get as clean as possible examples of predicative
unfeasibility.

Now, for the sake of completeness, I attach a regular FOM posting of mine
of 11:57AM 10/15/98:

>Recall from my earlier postings that
>
>1. n(k) is defined to be the length of the longest sequence from {1,...,k}
>such that there are no two distinct blocks of the form x[i],...,x[2i], i >=
>k, such that the first is a subsequence of the second.
>
>2. m(k) is defined to be the length of the longest binary sequence such
>that there are no two distinct blocks of the form x[i],...,x[2i], i >= k,
>such that the first is a subsequence of the second.
>
>For each p >= 2, let B(p) be the length of the longest binary sequence such
>that there are no p distinct blocks of the form x[i],...,x[2i], where each
>block is a  subsequence of the later blocks. Each B(p) exists.
>
>As indicated in earlier postings, the results are:
>
>m(1) = 11, m(2) = 31, m(3) = 100, m(4) >= 187205.
>n(3) > A_7198(158386).
>
>What about B?
>
>B(2) = m(1) = n(2) = 11. B(3) > A_7198(158386).
>
>Here A_7198 is the 7198-th level of the Ackerman hierarchy, where the first
>level is doubling, the second level is exponentiation, and the third level
>is iterated exponentiation.
>
>Added 10/16/98: Let A(k) be the unary Ackerman function, A(k) = A_k(k).
>
>There are constants c,d such that m(k) <= A([ck+d]). Some detailed work
>needs to be done to get really small c,d.
>
>This is false for B. In fact, for k >= 2, B(2k-1) > AA...A(7198), where
>there are k A's. In particular, B(3) > A(A(7198)).