[FOM] 273:Sigma01/optimal/size

[Harvey Friedman]

We make some remarks concerning
http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html

The issue has arisen concerning the actual size of the number implicit in
the Proposition discussed in
http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html

PROPOSITION. (THREE labels). There exists n >= 1 such that the following
holds. Let T_1,...,T_n be trees with vertices labeled from {1,2,3}, 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.

In http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html we sketched a
proof of

THEOREM #. The above Proposition can be proved in strictly finite
mathematics. However, any such proof in ACA_0 + Pi12-BI must use at least
2^[1000] symbols.

We forgot to address the issue of size.

Let TREE[k] be the length n of the longest sequence of trees T_1,...,T_n
with vertices labeled from {1,...,k}, where each T_i has at most i vertices,
and no T_i is inf preserving and label preserving embeddable into a later
T_j. 

Note that TREE[1] = 1 and TREE[2] = 2.

One of our many finite forms of Kruskal's theorem asserts that

for all k, TREE[k] exists.

This function eventually dominates every provably recursive function of the
system ACA_0 + Pi12-BI. Furthermore,

THEOREM ##. TREE[3] is greater than the halting time of any Turing machine
initialized with a blank tape, which can be proved to halt in ACA_0 +
Pi12-BI by a proof with at most 2^[1000] symbols.

To see this, recall that in
http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html we used

LEMMA. 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(x,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.

NOTE: (In http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html I wrote
|f(x,i)|, which is  just f(x,i).

In http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html we let x be
the godel number of a proof in ACA_0 + Pi12-BI of the Proposition above, and
showed that  we constructed an appropriate very long sequence of 3 labeled
trees whose length is at least that of than any y1 >' ... >' yp in <' such
that each |yi| <= f(x,i).

In the Smith article,

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.

we already used a form of the Lemma to derive a lower bound on the size of
TREE[6], as in the present Proposition ##.

The idea is straightforward. Let TM be a Turing machine which can be proved
to halt in ACA_0 + Pi12-BI by a proof with at most 2^[1000] symbols, at the
blank tape. Apply the Lemma to the Sigma01 sentence "TM halts". The long
sequence of 3 labeled trees constructed in
http://www.cs.nyu.edu/pipermail/fom/2006-March/010260.html is longer than
the relevant p's in the Lemma, and so longer than the halting time of TM.
QED

http://www.cs.nyu.edu/pipermail/fom/2006-March/010271.html mentions Graham's
number.

Graham's number is upper bounded by the value of the 4th (I may be off by 1)
function in the Ackermann hierarchy at a fairly small argument.

In http://www.cs.nyu.edu/pipermail/fom/1998-October/002339.html we discussed
the numbers n(3) and n(4), which appear in my paper

H. Friedman, Long Finite Sequences, Journal of Combinatorial Theory, Series
A 95, 102-144 (2001).

In http://www.cs.nyu.edu/pipermail/fom/1998-October/002339.html I wrote

"THEOREM 3. n(3) > A_7198(158386).

I have a lower bound for n(4). Write A(t) = A_t(t).

THEOREM 4. n(4) is greater than AA...A(1), where there are A(L) A's.
Recall that L >= 187196. "

Here A_7198 is the 7198-th function in the Ackermann hierarchy.

Of course, Graham's number has some special mathematical significance of a
different kind than my numbers. So Graham's number of course REMAINS quite
important, despite its PUNY size.

It is easily seen that n(4) is completely UNNOTICEABLE in comparison to
TREE[3]. Also, numbers derived from Goodstein sequences or Paris/Harrington
Ramsey theory, although bigger than n(4), are also completely UNNOTICEABLE
in comparison to TREE[3].

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 273rd 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
271. Clarification of Smith Article  3/22/06  5:58PM
272. Sigma01/optimal  3/24/06  1:45PM

Harvey Friedman