# [FOM] 273:Sigma01/optimal/size

Harvey Friedman friedman at math.ohio-state.edu
Tue Mar 28 12:57:25 EST 2006

```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^ 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 and TREE = 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 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^ 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, 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^ 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. Also, numbers derived from Goodstein sequences or Paris/Harrington
Ramsey theory, although bigger than n(4), are also completely UNNOTICEABLE
in comparison to TREE.

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

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

```