FOM: 25:Long Walks

[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
24:Predicatively Unfeasible Integers  11/10/98  10:44PM

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 consider finite and infinite sequences from the lattice set Z^k in k
dimensions. We say that (x_1,...,x_k) points outward to (y_1,...,y_k) if
and only if for each 1 <= i <= k, either 0 <= x_i <= y_i or 0 >= x_i >= y_i.

We begin with an infinitary theorem.

THEOREM 1. Let k >= 1. In any infinite sequence from Z^k, some term points
outward to a later term.

We now consider finite sequences where consecutive terms are close
together, then we can obtain such upper bounds. Any such sequence can be
considered to be a "walk," although the usual notion of walk in the
literature is more specific (see below).

THEOREM 2. Let k,r >= 1 and x in Z^k. There is a longest sequence from Z^k
starting with x, such that the Euclidean distance between consecutive terms
is at most r, and no term points outward to any later term.

How long is this longest sequence? Let 2^[n] be an exponential stack of 2's
of length n. Let 2^[n](m) be an exponential stack of 2's of length n with m
on top. Thus 2^[n] = 2^[n](1).

THEOREM 3. Let n be the length of the longest sequence from Z^3 starting
with (1,1,1), such that the Euclidean distance between consecutive terms is
at most 3, and no term points outward to any later term. Then 2^[7] < n <
2^[25].

THEOREM 4. Let r >= 3 and x in Z+^3. Let n be the length of the longest
sequence from Z^3 starting with x, such that the Euclidean distance between
consecutive terms is at most r, and no term points outward to any later
term. Then 2^[7](max(r-2,x)) < n < 2^[25](max(r-2,x)).

Define the usual Ackerman hierarchy of functions from Z+ into Z+ by: A_1 to
be doubling, A_2 is exponentiation, A_3 is iterated exponentiation,
etcetera.

THEOREM 5. Fix k >= 1. Let n be the length of the longest sequence from Z^k
starting with (1,...,1), such that the sup norm distance between
consecutive terms is at most 1, and no term points outward to any later
term. Then n > A_k-1(k-1).

THEOREM 6. Let k >= 2 and r >= 1. Define F(k,r) to be the length of the
longest sequence from Z^k starting at a vector of Euclidean norm at most r,
such that the Euclidean distance between consecutive terms is at most r,
and no term points outward to any later term. Then F_k(r) is strictly
dominated by a multiple iteration of A_k-1, where the length of the
iteration depends only on k.

The usual definition of walk in Z^k is a sequence from Z^k such that the
Euclidean distance between consecutive terms is exactly 1. A centered walk
is a walk whose first term is the origin. The analogous results hold
provided we look only at terms of the form x_4i:

THEOREM 7. Let n be the length of the longest centered walk x in Z^3 such
that for no i < j does x_4i point outward to x_4j. Then 2^[7] < n < 2^[25].

THEOREM 8. Fix k >= 1. Let n be the length of the longest centered walk x
in Z^k such that for no i < j does x_4i point outward to x_4j. Then n >
A_k-1(k-1).

THEOREM 9. Let k >= 2 and r >= 1. Define F(k,r) to be the length of the
longest centered walk x from Z^k such that for no i < j does x_ri point
outward to x_rj. Then F(k,r) is strictly dominated by a multiple iteration
of A_k-1, where the length of the iteration depends only on k.

These results are fairly crude, and are expected to be improved. But they
give a reasonable idea of the relationship between the Ackerman hierarchy
and the length of such walks in dimensions >= 3. Dimension 2 is also pretty
interesting, and will be taken up in a later posting.