[FOM] 440: Finite Phase Transitions
Harvey Friedman
friedman at math.ohio-state.edu
Sun Sep 26 13:15:06 EDT 2010
THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION.
######################################################################
FINITE PHASE TRANSITIONS
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
http://www.cs.nyu.edu/pipermail/fom/1998-July/001921.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002332.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002339.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002356.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002365.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002383.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002395.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002407.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002409.html
http://www.cs.nyu.edu/pipermail/fom/1998-October/002410.html
http://www.cs.nyu.edu/pipermail/fom/1998-November/002439.html
http://www.cs.nyu.edu/pipermail/fom/1998-November/002443.html
http://www.cs.nyu.edu/pipermail/fom/1999-March/002752.html
http://www.cs.nyu.edu/pipermail/fom/1999-May/003134.html
http://www.cs.nyu.edu/pipermail/fom/1999-July/003251.html
http://www.cs.nyu.edu/pipermail/fom/1999-July/003253.html
http://www.cs.nyu.edu/pipermail/fom/2006-March/010292.html
http://www.cs.nyu.edu/pipermail/fom/2006-March/010293.html
http://www.cs.nyu.edu/pipermail/fom/2006-March/010290.html
http://www.cs.nyu.edu/pipermail/fom/2006-March/010279.html
http://www.cs.nyu.edu/pipermail/fom/2006-March/010281.html
http://www.cs.nyu.edu/pipermail/fom/2006-April/010305.html
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
descriptive.
QUANTITATIVE APPROACH.
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
presented.
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.
QUALITATIVE APPROACH.
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
INTEGER OF T.
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) < ... .
AN EXAMPLE.
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
induction.
F(5) is greater than the proof theoretic integer of 3 quantifier
induction.
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 +
Sigma11-DC).
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
11:18AM
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
8:15PM
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
7:51PM
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
3:32PM
390: Finite Games, Vector Reduction, and Large Cardinals 2 2/14/09
10:27PM
391: Finite Games, Vector Reduction, and Large Cardinals 3 2/21/10
5:54AM
392: Finite Games, Vector Reduction, and Large Cardinals 4 2/22/10
9:15AM
393: Finite Games, Vector Reduction, and Large Cardinals 5 2/22/10
3:50AM
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