[FOM] 440: Finite Phase Transitions

Harvey Friedman friedman at math.ohio-state.edu
Sun Sep 26 13:15:06 EDT 2010



Harvey M. Friedman
September 26, 2010

This topic has been discussed earlier on the FOM in various guises.  
Big numbers and long sequences associated with mathematical objects. See


Suppose we have a Pi02 theorem (forall k)(thereexists n)(A(k,n)). We  
then get a recursive function F(k) = the least n such that A(k,n)  
holds. In the intended cases, we have F(0) < F(1) < ... .

We want to look at F(0),F(1),... and determine where there is a  
"qualitative jump" in size. I.e., a "phase transition". In the cases  
we focus on, after the first few terms - say about 16 or less - we  
simply get qualitatively indistinguishable very large integers.

There are a number of forms that such results can take. Some are more  
descriptive than quantitative and others are more quantitative than  


In the quantitative approach, we simply provide upper and lower bounds  
on a sizable initial segment of the F(0),F(1),... using a notation  
system for integers. We try to make exact calculations, if possible.

But what notation system to use for the integers?

In case the numbers involved are less than, say, 10^100, the usual  
base 10 notation is the clear choice.

But when the numbers involved are greater than, say, 10^(10^100), base  
10 notation is generally of no use whatsoever since it cannot even be  

So we are led to the following general approach. We identify a finite  
list of constants and basic functions of one or more variables on the  
nonnegative integers. We then use closed terms to name particular  
nonnegative integers. Of course, we should strive to use small terms  
for this purpose.

This leads to a very interesting computational complexity problem.  
Suppose we start with a finite list of constants and basic functions.  
We can ask, for example, whether two terms, using 0, are equal or not,  
or how they compare under <. What is the computational complexity of  
this problem?

Let us now focus on a very natural system. We use constants 0,1,  
addition, multiplication, and exponentiation to any positive base. We  
can choose to use terms in these basics with at most, say, 100  
symbols, or even say, just 16 symbols, before wishing to use a "more  
powerful" system. The only reason I am familiar with for moving to a  
"more powerful system" is because the number in question is larger  
than anything given by a term of, say, 100 or maybe 16 symbols.

The above system - or some more convenient variant - is a good system  
for investigating the finite Ramsey numbers, or numbers in Adjacent  
Ramsey Theory.

We think of the above system as an integer notation system.

I used the integer notation system based on the Ackermann hierarchy of  
functions, in my work on Long Finite Sequences.

The Ackermann hierarchy of functions is encapsulated in terms of a  
binary function A(n,m), which is the n-th Ackermann function at m.  
(There are many ways to present this hierarchy and the Ackermann  
function itself. They are all minor variants of each other). See

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

There I gave the lower bound A_7198(158386) < n(3).

In terms of the binary Ackermann function, this lower bound reads

A(7198,158386) < n(3).

I didn't give an upper bound there, but I later conjectured

n(3) < A(A(5,5),A(5,5)).

So base 10 notation and the binary Ackermann function can serve as a  
reasonable notation system for integers.

For a unified approach to integers too large to be bounded by a  
reasonable sized term in the above notation system for integers, we  
can use epsilon_0 with its usual system of fundamental sequences. At  
successor ordinals, we use the indefinite iteration as in the  
Ackermann hierarchy. At limits, we use the fundamental sequence. The  
Ackermann hierarchy appears at the first omega levels, and the  
Ackermann function essentially appears at the omega-th level.

THis provides a notation system for integers, using 0 and the binary  
function corresponding to the above Hardy hierarchy (or Wainer  
hierarchy). We may want to sugar it with base 10 notation.

For integers too large to be bounded by a reasonable sized term in  
this notation system for integers, we would use the obvious extension  
of this for larger proof theoretic ordinals.

But there remains the question: what do we mean by a qualitative jump  
in size? What is a phase transition in this context?

We can, of course, let the estimates speak for themselves. However, we  
may demand a more principled answer.


In the qualitative approach, we look to formal systems for the more  
principled answer. In particular, we associate an integer to every  
formal system.

Now, there will be some ad hoc features involved in the associated  
integer. However, we Conjecture that there is a great deal of  
robustness here.

We call this associated integer - defined below - the PROOF THEORETIC  

We assume that T is

#) a formal system in a finite relational type in many sorted  
predicate calculus with equality, containing a sort for natural  
numbers, with 0,S,+,dot,exp,<.

The delta0 formulas are defined as usual, using bounded quantifiers.  
The Sigma01 formulas are obtained from the delta0 formulas by putting  
zero or more existential quantifiers in front of delta0 formulas.

The proof theoretic integer of T is the least integer n such that  
every Sigma01 sentence that has a proof in T with at most 10,000  
symbols, has witnesses less than n.

Of course, this definition needs some exact spelling out - e.g., what  
exact proof system is to be used, and what exactly counts as a symbol  
(what about parentheses), etcetera?

However, it is expected that there is a lot of robustness. Of course,  
not robustness in the form of the exact number being unchanged. But  
robustness in a more subtle sense.

In particular, we make the following robustness conjecture.

ROBUSTNESS CONJECTURE. Let S,T be two naturally occurring formal  
systems obeying #), which prove EFA (exponential function arithmetic).  
Suppose S proves the 1-consistency of T. Then the proof theoretic  
integer of S is at least a double exponential of the proof theoretic  
integer of T.

QUESTION: Can we use a significantly smaller number than 10,000 in the  
definition of the proof theoretic integer, and still have the  
robustness conjecture?

Because this Conjecture has "naturally occurring", it takes on an  
experimental character. We Conjecture that there is a form of the  
Conjecture that can be proved, where we assume instead that the  
complexity of S,T is low, and the size of the proof of 1-consistency  
of T in S is also low.

We propose using proof theoretic integers of basic formal systems  
(such as EFA, PA(1), PA(2), PA, ACA_0, ACA,  as benchmarks for large  
integers that arise in connection with comparing the integers F(0) <  
F(1) < F(2) < ... .


A good source of examples is in the area surrounding Kruskal's  
theorem. We will not allow an empty tree.

THEOREM. For all k >= 0 there exists n >= 0 such that the following  
holds. For all structured finite trees T_1,...,T_n, where each T_i has  
at most i+k vertices, there exists i < j such that T_i is inf and  
structure preserving embeddable into T_j.

Let F(k) be the length of the longest sequence of structured finite  
trees T_1,...,T_n, where T_i has at most i+k vertices, for no i < j,  
is T_i is inf and structure preserving embeddable into T_j.

F(0) = 1.
F(1) = 2.
F(2) = 5.
F(3) is greater than 58.
f(4) is greater than the proof theoretic integer of 1 quantifier  
F(5) is greater than the proof theoretic integer of 3 quantifier  
F(6) is greater than the proof theoretic integer of PA.
F(7) is greater than the proof theoretic integer of ATR (or even ARR +  

Sketches of the proofs of these lower bounds can be found in http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html 
  paper #69.


I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 440th 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-349 can be found athttp://www.cs.nyu.edu/pipermail/fom/2009-August/014004.html
in the FOM archives.

350: one dimensional set series  7/23/09  12:11AM
351: Mapping Theorems/Mahlo/Subtle  8/6/09  10:59PM
352: Mapping Theorems/simpler  8/7/09  10:06PM
353: Function Generation 1  8/9/09  12:09PM
354: Mahlo Cardinals in HIGH SCHOOL 1  8/9/09  6:37PM
355: Mahlo Cardinals in HIGH SCHOOL 2  8/10/09  6:18PM
356: Simplified HIGH SCHOOL and Mapping Theorem  8/14/09  9:31AM
357: HIGH SCHOOL Games/Update  8/20/09  10:42AM
358: clearer statements of HIGH SCHOOL Games  8/23/09  2:42AM
359: finite two person HIGH SCHOOL games  8/24/09  1:28PM
360: Finite Linear/Limited Memory Games  8/31/09  5:43PM
361: Finite Promise Games  9/2/09  7:04AM
362: Simplest Order Invariant Game  9/7/09  11:08AM
363: Greedy Function Games/Largest Cardinals 1
364: Anticipation Function Games/Largest Cardinals/Simplified 9/7/09
365: Free Reductions and Large Cardinals 1  9/24/09  1:06PM
366: Free Reductions and Large Cardinals/polished  9/28/09 2:19PM
367: Upper Shift Fixed Points and Large Cardinals  10/4/09 2:44PM
368: Upper Shift Fixed Point and Large Cardinals/correction 10/6/09
369. Fixed Points and Large Cardinals/restatement  10/29/09 2:23PM
370: Upper Shift Fixed Points, Sequences, Games, and Large Cardinals
11/19/09  12:14PM
371: Vector Reduction and Large Cardinals  11/21/09  1:34AM
372: Maximal Lower Chains, Vector Reduction, and Large Cardinals
11/26/09  5:05AM
373: Upper Shifts, Greedy Chains, Vector Reduction, and Large
Cardinals  12/7/09  9:17AM
374: Upper Shift Greedy Chain Games  12/12/09  5:56AM
375: Upper Shift Clique Games and Large Cardinals 1graham
376: The Upper Shift Greedy Clique Theorem, and Large Cardinals
12/24/09  2:23PM
377: The Polynomial Shift Theorem  12/25/09  2:39PM
378: Upper Shift Clique Sequences and Large Cardinals  12/25/09 2:41PM
379: Greedy Sets and Huge Cardinals 1
380: More Polynomial Shift Theorems  12/28/09  7:06AM
381: Trigonometric Shift Theorem  12/29/09  11:25AM
382: Upper Shift Greedy Cliques and Large Cardinals  12/30/09 2:51AM
383: Upper Shift Greedy Clique Sequences and Large Cardinals 1
12/30/09  3:25PM
384: THe Polynomial Shift Translation Theorem/CORRECTION 12/31/09
385: Shifts and Extreme Greedy Clique Sequences  1/1/10  7:35PM
386: Terrifically and Extremely Long Finite Sequences  1/1/10 7:35PM
387: Better Polynomial Shift Translation/typos  1/6/10  10:41PM
388: Goedel's Second Again/definitive?  1/7/10  11:06AM
389: Finite Games, Vector Reduction, and Large Cardinals 1 2/9/10
390: Finite Games, Vector Reduction, and Large Cardinals 2 2/14/09
391: Finite Games, Vector Reduction, and Large Cardinals 3 2/21/10
392: Finite Games, Vector Reduction, and Large Cardinals 4 2/22/10
393: Finite Games, Vector Reduction, and Large Cardinals 5 2/22/10
394: Free Reduction Theory 1  3/2/10  7:30PM
395: Free Reduction Theory 2  3/7/10  5:41PM
396: Free Reduction Theory 3  3/7/10  11:30PM
397: Free Reduction Theory 4  3/8/10  9:05AM
398: New Free Reduction Theory 1  3/10/10  5:26AM
399: New Free Reduction Theory 2  3/12/10  9:36AM
400: New Free Reduction Theory 3  3/14/10  11:55AM
401: New Free Reduction Theory 4  3/15/10  4:12PM
402: New Free Reduction Theory 5  3/19/10  12:59PM
403: Set Equation Tower Theory 1  3/22/10  2:45PM
404: Set Equation Tower Theory 2  3/24/10  11:18PM
405: Some Countable Model Theory 1  3/24/10  11:20PM
406: Set Equation Tower Theory 3  3/25/10  6:24PM
407: Kernel Tower Theory 1  3/31/10  12:02PM
408: Kernel tower Theory 2  4/1/10  6:46PM
409: Kernel Tower Theory 3  4/5/10  4:04PM
410: Kernel Function Theory 1  4/8/10  7:39PM
411: Free Generation Theory 1  4/13/10  2:55PM
412: Local Basis Construction Theory 1  4/17/10  11:23PM
413: Local Basis Construction Theory 2  4/20/10  1:51PM
414: Integer Decomposition Theory  4/23/10  12:45PM
415: Integer Decomposition Theory 2  4/24/10  3:49PM
416: Integer Decomposition Theory 3  4/26/10  7:04PM
417: Integer Decomposition Theory 4  4/28/10  6:25PM
418: Integer Decomposition Theory 5  4/29/10  4:08PM
419: Integer Decomposition Theory 6  5/4/10   10:39PM
420: Reduction Function Theory 1  5/17/10   2:53AM
421: Reduction Function Theory 2  5/19/10   12:00PM
422: Well Behaved Reduction Functions 1  5/23/10  4:12PM
423: Well Behaved Reduction Functions 2  5/27/10  3:01PM
424: Well Behaved Reduction Functions 3  5/29/10  8:06PM
425: Well Behaved Reduction Functions 4  5/31/10  5:05PM
426: Well Behaved Reduction Functions 5  6/2/10  12:43PM
427: Finite Games and Incompleteness 1  6/10/10  4:08PM
428: Typo Correction in #427  6/11/10  12:11AM
429: Finite Games and Incompleteness 2  6/16/10  7:26PM
430: Finite Games and Incompleteness 3  6/18/10  6:14PM
431: Finite Incompleteness/Combinatorially Simplest  6/20/10  11:22PM
432: Finite Games and Incompleteness 4  6/26/10  8:39PM
433: Finite Games and Incompleteness 5  6/27/10  3:33PM
434: Digraph Kernel Structure Theory 1  7/4/10  3:17PM
435: Kernel Structure Theory 1  7/5/10  5:55PM
436: Kernel Structure Theory 2  7/9/10  5:21PM
437: Twin Prime Polynomial  7/15/10  2:01PM
438: Twin Prime Polynomial/error  9/17/10  1:22PM
439: Twin Prime Polynomial/corrected 9/19/10  2:16PM

Harvey Friedman

More information about the FOM mailing list