[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^[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
More information about the FOM
mailing list