[FOM] 289:Integer Thresholds in FFF

[Harvey Friedman]

My original finite form of Kruskal's theorem, now usually called FFF,
asserts the following:

FFF. For all c >= 0 there exists n so large that the following holds. For
all trees T1,...,Tn with each |Ti| <= i+c, there exists 1 <= i < j <= n such
that Ti is inf preserving embeddable into Tj.

This can also be stated as follows. Any preference seems to be subjective.

FFF. Let c >= 1. There is a longest sequence of trees T1,...,Tn with each
|Ti| = i+c-1 such that for no 1 <= i < j <= n, is Ti inf preserving
embeddable into Tj.

Let us write the length of the longest such sequence as FFF(c).

FFF(1) = 1.
FFF(2) = 2.
FFF(3) = 5.

FFF(4) is entirely under control by logically very rudimentary methods.
FFF(4) looks to be quite time consuming to compute exactly without the help
of a computer. I have fooled around with this for a while, and came to the
conclusion that it should come in well under 100.

If one is going to develop the relevant computer program for this sort of
problem, one should have a more general class of numbers to calculate. Here
is a proposal.

FFF(T). Let T be a finite tree. There is a longest sequences of trees
T1,...,Tn, where T1 = T and each |Ti| <= i+|T|-1, such that for no 1 <= i <
j <= n, is Ti inf preserving embeddable into Tj.

One can hope to work out what this longest length is for various small T, by
computer. 

For FFF(5), things get way out of control for a computer. Any proof that
FFF(5) exists in PA must use at least A(10) symbols, where A is a common
presentation of the unary form of the Ackermann function. FFF(5) is greater
than all least witnesses of Sigma01 sentences provably true in PA using at
most A(10) symbols.

For FFF(6), the lower bounds are much sharper. Any proof that FFF(5) exists
in ATR must use at least A(10) symbols, where A is a common presentation of
the unary form of the Ackermann function. FFF(5) is greater than all least
witnesses of Sigma01 sentences provably true in ATR using at most A(10)
symbols. 

FFF(5) can be proved to exist in ACA using at most 10,000 symbols.

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 289th 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
273: Sigma01/optimal/size  3/28/06  12:57PM
274: Subcubic Graph Numbers  4/1/06  11:23AM
275: Kruskal Theorem/Impredicativity  4/2/06  12:16PM
276: Higman/Kruskal/impredicativity  4/4/06  6:31AM
277: Strict Predicativity  4/5/06  1:58PM
278: Ultra/Strict/Predicativity/Higman  4/8/06  1:33AM
279: Subcubic graph numbers/restated  4/8/06  3:14AN
280: Generating large caridnals/self embedding axioms  5/2/06  4:55AM
281: Linear Self Embedding Axioms  5/5/06  2:32AM
282: Adventures in Pi01 Independence  5/7/06
283: A theory of indiscernibles  5/7/06  6:42PM
284: Godel's Second  5/9/06  10:02AM
285: Godel's Second/more  5/10/06  5:55PM
286: Godel's Second/still more  5/11/06  2:05PM
287: More Pi01 adventures  5/18/06  9:19AM
288: Discrete ordered rings and large cardinals  6/1/06  11:28AM

Harvey Friedman