View source for Kruskal's tree theorem

{{short description|Well-quasi-ordering of finite trees}}
{{Redirect|TREE||Tree (disambiguation)}}
In [[mathematics]], '''Kruskal's tree theorem''' states that the set of finite [[tree (graph theory)|tree]]s over a [[well-quasi-ordering|well-quasi-ordered]] set of labels is itself well-quasi-ordered under [[homeomorphism (graph theory)|homeomorphic]] embedding. 

==History==
The [[theorem]] was [[conjecture]]d by [[Andrew Vázsonyi]] and [[mathematical proof|proved]] by {{harvs|txt=yes|year= 1960 |authorlink=Joseph Kruskal|last=Kruskal|first=Joseph}}; a short proof was given by  {{harvs|txt=yes|year= 1963|authorlink=Crispin St. J. A. Nash-Williams|last=Nash-Williams|first=Crispin}}. It has since become a prominent example in [[reverse mathematics]] as a statement that cannot be proved in ATR<sub>0</sub> (a [[second-order arithmetic]] theory with a form of [[arithmetical transfinite recursion]]).

In 2004, the result was generalized from trees to [[graph (discrete mathematics)|graph]]s as the [[Robertson–Seymour theorem]], a result that has also proved important in reverse mathematics and leads to the even-faster-growing [[Friedman's SSCG function|SSCG function]], which dwarfs <math>\text{TREE}(3)</math>. A [[finitary]] application of the theorem gives the existence of the fast-growing '''TREE function'''. '''TREE(3)''' is largely accepted to be one of the large finite numbers, dwarfing other large numbers such as [[Graham's number]] and [[googolplex]].<ref>{{Cite web |date=2017-10-20 |title=The Enormity of the Number TREE(3) Is Beyond Comprehension |url=https://www.popularmechanics.com/science/math/a28725/number-tree3/ |access-date=2025-02-04 |website=Popular Mechanics |language=en-US}}</ref>

==Statement==
The version given here is that proven by Nash-Williams; Kruskal's formulation is somewhat stronger. All trees we consider are finite.

Given a tree {{mvar|T}} with a [[rooted tree|root]], and given vertices {{mvar|v}}, {{mvar|w}}, call {{mvar|w}} a ''successor'' of {{mvar|v}} if the unique path from the root to {{mvar|w}} contains {{mvar|v}}, and call {{mvar|w}} an ''immediate successor'' of {{mvar|v}} if additionally the path from {{mvar|v}} to {{mvar|w}} contains no other vertex.

Take {{mvar|X}} to be a [[partially ordered set]]. If {{math|''T''<sub>1</sub>}}, {{math|''T''<sub>2</sub>}} are rooted trees with vertices labeled in {{mvar|X}}, we say that {{math|''T''<sub>1</sub>}} is ''inf-embeddable'' in {{math|''T''<sub>2</sub>}} and write <math>T_1 \leq T_2</math> if there is an [[injective map]] {{mvar|F}} from the vertices of {{math|''T''<sub>1</sub>}} to the vertices of {{math|''T''<sub>2</sub>}} such that:

*For all vertices {{mvar|v}} of {{math|''T''<sub>1</sub>}}, the label of {{mvar|v}} precedes the label of <math>F(v)</math>;
*If {{mvar|w}} is any successor of {{mvar|v}} in {{math|''T''<sub>1</sub>}}, then <math>F(w)</math> is a successor of <math>F(v)</math>; and
*If {{math|''w''<sub>1</sub>}}, {{math|''w''<sub>2</sub>}} are any two distinct immediate successors of {{mvar|v}}, then the path from <math>F(w_1)</math> to <math>F(w_2)</math> in {{math|''T''<sub>2</sub>}} contains <math>F(v)</math>.

Kruskal's tree theorem then states:
<blockquote>If {{mvar|X}} is [[well-quasi-ordering|well-quasi-ordered]], then the set of rooted trees with labels in {{mvar|X}} is well-quasi-ordered under the inf-embeddable order defined above. (That is to say, given any infinite sequence {{math|''T''<sub>1</sub>, ''T''<sub>2</sub>, …}} of rooted trees labeled in {{mvar|X}}, there is some <math>i<j</math> so that <math>T_i \leq T_j</math>.)</blockquote>

==Friedman's work==
For a [[countable set|countable]] label set {{mvar|X}}, Kruskal's tree theorem can be expressed and proven using [[second-order arithmetic]]. However, like [[Goodstein's theorem]] or the [[Paris–Harrington theorem]], some special cases and variants of the theorem can be expressed in subsystems of second-order arithmetic much weaker than the subsystems where they can be proved. This was first observed by [[Harvey Friedman (mathematician)|Harvey Friedman]] in the early 1980s, an early success of the {{nowrap|then-nascent}} field of reverse mathematics. In the case where the trees above are taken to be unlabeled (that is, in the case where {{mvar|X}} has size one), Friedman found that the result was unprovable in [[arithmetical transfinite recursion|ATR<sub>0</sub>]],<ref>{{harvnb|Simpson|1985|at=Theorem 1.8}}</ref> thus giving the first example of a [[impredicativity|predicative]] result with a provably impredicative proof.<ref>{{harvnb|Friedman|2002|p=60}}</ref> This case of the theorem is still provable by Π{{su|p=1|b=1}}-CA<sub>0</sub>, but by adding a "gap condition"<ref>{{harvnb|Simpson|1985|at=Definition 4.1}}</ref> to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system.<ref>{{harvnb|Simpson|1985|at=Theorem 5.14}}</ref><ref>{{harvnb|Marcone|2005|pp=8–9}}</ref> Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π{{su|p=1|b=1}}-CA<sub>0</sub>.

[[Ordinal analysis]] confirms the strength of Kruskal's theorem, with the [[proof-theoretic ordinal]] of the theorem equaling the [[small Veblen ordinal]] (sometimes confused with the smaller [[Ackermann ordinal]]).{{sfn|Rathjen|Weiermann|1993}}

==Weak tree function==
Suppose that <math>P(n)</math> is the statement:

:There is some {{mvar|m}} such that if {{math|''T''<sub>1</sub>, ..., ''T''<sub>''m''</sub>}} is a finite sequence of unlabeled rooted trees where {{Mvar|T<sub>i</sub>}} has <math>i+n</math> vertices, then <math>T_i \leq T_j</math> for some <math>i<j</math>.

All the statements <math>P(n)</math> are true as a consequence of Kruskal's theorem and [[Kőnig's lemma]]. For each {{Mvar|n}}, [[Peano axioms|Peano arithmetic]] can prove that <math>P(n)</math> is true, but Peano arithmetic cannot prove the statement "<math>P(n)</math> is true for all {{Mvar|n}}".<ref name="SmiA">{{harvnb|Smith|1985|p=120}}</ref>  Moreover, the length of the shortest [[formal proof|proof]] of <math>P(n)</math> in Peano arithmetic grows phenomenally fast as a function of {{Mvar|n}}, far faster than any [[primitive recursive function]] or the [[Ackermann function]], for example.{{citation needed|date=May 2023}} The least {{Mvar|m}} for which <math>P(n)</math> holds similarly grows extremely quickly with ''{{Mvar|n}}''.

Define <math>\text{tree}(n)</math>, the weak tree function, as the largest {{Mvar|m}} so that we have the following:

: There is a sequence {{math|''T''<sub>1</sub>, ..., ''T''<sub>''m''</sub>}} of unlabeled rooted trees, where each ''{{Mvar|T<sub>i</sub>}}'' has at most <math>i+n</math> vertices, such that <math>T_i \leq T_j</math> does not hold for any <math>i<j\leq m</math>.

It is known that <math>\text{tree}(1)=2</math>, <math>\text{tree}(2)=5</math>, <math>\text{tree}(3) \geq 844,424,930,131,960</math> (about 844&nbsp;trillion), <math>\text{tree}(4) \gg g_{64}</math> (where <math>g_{64}</math> is [[Graham's number]]), and <math>\text{TREE}(3)</math> (where the argument specifies the number of ''labels''; see [[#TREE function|below]]) is larger than <math>\mathrm{tree}^{\mathrm{tree}^{\mathrm{tree}^{\mathrm{tree}^{\mathrm{tree}^{8}(7)}(7)}(7)}(7)}(7).</math>

To differentiate the two functions, "TREE" (with all caps) is the big TREE function, and "tree" (with all letters in lowercase) is the weak tree function.

==TREE function==
[[File:TREE(3) sequence.png|thumb|alt=Sequence of trees where each node is colored either green, red, blue|A sequence of rooted trees labelled from a set of 3 labels (blue < red < green). The {{mvar|n}}th tree in the sequence contains at most {{mvar|n}} vertices, and no tree is inf-embeddable within any later tree in the sequence. {{Math|TREE(3)}} is defined to be the longest possible length of such a sequence.]]

By incorporating labels, Friedman defined a far faster-growing function.<ref>{{Cite web |last=Friedman |first=Harvey |date=28 March 2006 |title=273:Sigma01/optimal/size |url=http://www.cs.nyu.edu/pipermail/fom/2006-March/010279.html |access-date=8 August 2017 |website=[[Ohio State University]] Department of Maths}}</ref> For a positive [[integer]] ''{{Var|{{math|n}}}}'', take <math>\text{TREE}(n)</math>{{ref label|TR|a|^ a}} to be the largest ''{{Var|{{math|m}}}}'' so that we have the following:

: There is a sequence {{math|''T''<sub>1</sub>, ..., ''T''<sub>''m''</sub>}} of rooted trees labelled from a set of {{mvar|n}} labels, where each ''{{Mvar|T<sub>i</sub>}}'' has at most {{Mvar|i}} vertices, such that <math>T_i \leq T_j</math> does not hold for any <math>i<j\leq m</math>.

The TREE sequence begins <math>\text{TREE}(1)=1</math>, <math>\text{TREE}(2)=3</math>, before <math>\text{TREE}(3)</math> suddenly explodes to a value so large that many other "large" combinatorial constants, such as Friedman's ''<math>n(4)</math>'', ''<math>n^{n(5)}(5)</math>'', and [[Graham's number]],{{ref label|n_k|b|^ b}} are extremely small by comparison. A [[lower bound]] for ''<math>n(4)</math>'', and, hence, an ''extremely'' weak lower bound for <math>\text{TREE}(3)</math>, is ''<math>A^{A(187196)}(1)</math>''.{{ref label|Ackermann|c|^ c}}<ref>{{Cite web |last=Friedman |first=Harvey M. |date=1 June 2000 |title=Enormous Integers In Real Life |url=https://u.osu.edu/friedman.8/files/2014/01/EnormousInt.12pt.6_1_00-23kmig3.pdf |access-date=8 August 2017 |website=[[Ohio State University]]}}</ref> Graham's number, for example, is much smaller than the lower bound ''<math>A^{A(187196)}(1)</math>'', which is approximately <math>g_{3 \uparrow^{187196} 3}</math>, where <math>g_x</math> is [[Graham's number|Graham's function]].

==See also==
*[[Paris–Harrington theorem]]
*[[Kanamori–McAloon theorem]]
*[[Robertson–Seymour theorem]]

==Notes==
:{{note label|TR|a|^ a}} Friedman originally denoted this function by ''TR''[''n''].
:{{note label|n_k|b|^ b}} ''n''(''k'') is defined as the length of the longest possible sequence that can be constructed with a ''k''-letter alphabet such that no block of letters x<sub>''i''</sub>,...,x<sub>2''i''</sub> is a subsequence of any later block x<sub>''j''</sub>,...,x<sub>2''j''</sub>.<ref>{{Cite web |last=Friedman |first=Harvey M. |date=8 October 1998 |title=Long Finite Sequences |url=https://u.osu.edu/friedman.8/files/2014/01/LongFinSeq98-2f0wmq3.pdf |access-date=8 August 2017 |website=[[Ohio State University]] Department of Mathematics |pages=5, 48 (Thm.6.8)}}</ref> <math>n(1) = 3, n(2) = 11, \,\textrm{and}\, n(3) > 2 \uparrow^{7197} 158386</math>.
:{{note label|Ackermann|c|^ c}} ''A''(''x'') taking one argument, is defined as ''A''(''x'', ''x''), where ''A''(''k'', ''n''), taking two arguments, is a particular version of [[Ackermann's function]] defined as: ''A''(1, ''n'') = 2''n'', ''A''(''k''+1, 1) = ''A''(''k'', 1), ''A''(''k''+1, ''n''+1) = ''A''(''k'', ''A''(''k''+1, ''n'')).

==References==
'''Citations'''
{{reflist}}
'''Bibliography'''
* {{Cite book
 |last=Friedman |first=Harvey M. |author-link=Harvey Friedman (mathematician)
 |editor-last=Sieg |editor-first=Wilfried
 |editor-last2=Feferman |editor-first2=Solomon |editor-link2=Solomon Feferman
 |title=Reflections on the foundations of mathematics: essays in honor of Solomon Feferman
 |publisher=[[AK Peters]]
 |year=2002
 |isbn=978-1-56881-170-3
 |series=Lecture notes in logic
 |volume=15
 |location=Natick, Mass
 |pages=60–91
 |chapter=Internal finite tree embeddings
 |mr=1943303
 |chapter-url=https://books.google.com/books?id=o-dhDwAAQBAJ&pg=PA60
}}
* {{Cite journal
 |last=H. Gallier |first=Jean |author-link=Jean Gallier
 |date=September 1991
 |title=What's so special about Kruskal's theorem and the ordinal Γ<sub>0</sub>? A survey of some results in proof theory
 |url=http://www.cis.upenn.edu/~jean/kruskal.pdf
 |journal=[[Annals of Pure and Applied Logic]]
 |volume=53 |issue=3 |pages=199–260
 |doi=10.1016/0168-0072(91)90022-E |doi-access=free
 |mr=1129778
}} 
* {{Cite journal
 |last=Kruskal |first=J. B. |author-link=Joseph Kruskal
 |date=May 1960
 |title=Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
 |url=https://www.ams.org/journals/tran/1960-095-02/S0002-9947-1960-0111704-1/S0002-9947-1960-0111704-1.pdf
 |journal=[[Transactions of the American Mathematical Society]]
 |publisher=[[American Mathematical Society]]
 |volume=95 |issue=2 |pages=210–225
 |doi=10.2307/1993287
 |jstor=1993287
 |mr=0111704
}}
* {{Cite journal
 |last=Marcone |first=Alberto
 |editor-last=Simpson |editor-first=Stephen G.
 |year=2005
 |title=WQO and BQO theory in subsystems of second order arithmetic
 |url=https://users.dimi.uniud.it/~alberto.marcone/wqobqo.pdf
 |journal=Reverse Mathematics
 |series=Lecture Notes in Logic
 |location=Cambridge
 |publisher=[[Cambridge University Press]]
 |volume=21 |pages=303–330
 |doi=10.1017/9781316755846.020
 |isbn=978-1-316-75584-6
}}
* {{Cite journal
 |last=Nash-Williams |first=C. St. J. A. |author-link=Crispin St. J. A. Nash-Williams
 |date=October 1963
 |title=On well-quasi-ordering finite trees
 |url=https://www.cs.umd.edu/~gasarch/COURSES/752/S22/slides/nashwilliams.pdf
 |journal=[[Mathematical Proceedings of the Cambridge Philosophical Society]]
 |volume=59 |issue=4 |pages=833–835
 |bibcode=1963PCPS...59..833N
 |doi=10.1017/S0305004100003844
 |issn=0305-0041
 |mr=0153601
 |s2cid=251095188
}}
* {{Cite journal
 |last1=Rathjen |first1=Michael
 |last2=Weiermann |first2=Andreas
 |date=February 1993
 |title=Proof-theoretic investigations on Kruskal's theorem
 |url=https://core.ac.uk/download/pdf/82187099.pdf
 |journal=[[Annals of Pure and Applied Logic]]
 |volume=60 |issue=1 |pages=49–88
 |doi=10.1016/0168-0072(93)90192-G
 |mr=1212407
}}
* {{Cite book
 |last=Simpson |first=Stephen G. |author-link=Steve Simpson (mathematician)
 |editor-last=Friedman |editor-first=Harvey
 |editor-last2=Harrington |editor-first2=L. A.
 |editor-last3=Scedrov |editor-first3=A.
 |editor-last4=Simpson |editor-first4=S. G.
 |display-editors=3
 |title=Harvey Friedman's research on the foundations of mathematics
 |publisher=[[North-Holland (imprint)|North-Holland]]
 |year=1985
 |isbn=978-0-444-87834-2
 |series=Studies in logic and the foundations of mathematics
 |location=Amsterdam ; New York
 |pages=87–117
 |chapter=Nonprovability of certain combinatorial properties of finite trees
}}
* {{Cite book
 |last=Smith |first=Rick L.
 |editor-last=Friedman |editor-first=Harvey |editor-link=Harvey Friedman (mathematician)
 |editor-last2=Harrington |editor-first2=L. A.
 |title=Harvey Friedman's research on the foundations of mathematics
 |year=1985
 |publisher=[[North-Holland (imprint)|North-Holland]]
 |isbn=978-0-444-87834-2
 |series=Studies in logic and the foundations of mathematics
 |volume=117
 |location=Amsterdam ; New York
 |pages=119–136
 |chapter=The Consistency Strengths of Some Finite Forms of the Higman and Kruskal Theorems
 |doi=10.1016/s0049-237x(09)70157-0
}}

{{Large numbers}}
{{Order theory}}
{{Use dmy dates|date=March 2024}}


[[Category:Mathematical logic]]
[[Category:Order theory]]
[[Category:Theorems in discrete mathematics]]
[[Category:Trees (graph theory)]]
[[Category:Wellfoundedness]]