Kruskal's tree theorem#Friedman's finite form

The theorem was conjectured by Andrew Vázsonyi and 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₀ (a second-order arithmetic theory with a form of arithmetical transfinite recursion).

In 2004, the result was generalized from trees to graphs as the Robertson–Seymour theorem, a result that has also proved important in reverse mathematics and leads to the even-faster-growing SSCG function, which dwarfs $\backslash text\{TREE\}(3)$.

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 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₁}}, {{math|T₂}} are rooted trees with vertices labeled in {{mvar|X}}, we say that {{math|T₁}} is inf-embeddable in {{math|T₂}} and write $T\_1\; \backslash leq\; T\_2$ if there is an injective map {{mvar|F}} from the vertices of {{math|T₁}} to the vertices of {{math|T₂}} such that:

• For all vertices {{mvar|v}} of {{math|T₁}}, the label of {{mvar|v}} precedes the label of $F(v)$;
• If {{mvar|w}} is any successor of {{mvar|v}} in {{math|T₁}}, then $F(w)$ is a successor of $F(v)$; and
• If {{math|w₁}}, {{math|w₂}} are any two distinct immediate successors of {{mvar|v}}, then the path from $F(w\_1)$ to $F(w\_2)$ in {{math|T₂}} contains $F(v)$.

Kruskal's tree theorem then states:

If {{mvar|X}} is 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₁, T₂, …}} of rooted trees labeled in {{mvar|X}}, there is some

For a 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 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 ATR₀,{{harvnb|Simpson|1985|at=Theorem 1.8}} thus giving the first example of a predicative result with a provably impredicative proof.{{harvnb|Friedman|2002|p=60}} This case of the theorem is still provable by Π{{su|p=1|b=1}}-CA₀, but by adding a "gap condition"{{harvnb|Simpson|1985|at=Definition 4.1}} to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system.{{harvnb|Simpson|1985|at=Theorem 5.14}}{{harvnb|Marcone|2005|pp=8–9}} Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π{{su|p=1|b=1}}-CA₀.

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}}

Suppose that $P(n)$ is the statement:

:There is some {{mvar|m}} such that if {{math|T₁, ..., T_m}} is a finite sequence of unlabeled rooted trees where {{Mvar|T_i}} has $i+n$ vertices, then $T\_i\; \backslash leq\; T\_j$ for some

All the statements $P(n)$ are true as a consequence of Kruskal's theorem and Kőnig's lemma. For each {{Mvar|n}}, Peano arithmetic can prove that $P(n)$ is true, but Peano arithmetic cannot prove the statement "$P(n)$ is true for all {{Mvar|n}}".{{harvnb|Smith|1985|p=120}} Moreover, the length of the shortest proof of $P(n)$ 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 $P(n)$ holds similarly grows extremely quickly with {{Mvar|n}}.

File:TREE(3) sequence.png

By incorporating labels, Friedman defined a far faster-growing function.{{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}} For a positive integer {{Var|{{math|n}}}}, take $\backslash text\{TREE\}(n)${{ref label|TR|a|^ a}} to be the largest {{Var|{{math|m}}}} so that we have the following:

: There is a sequence {{math|T₁, ..., T_m}} of rooted trees labelled from a set of {{mvar|n}} labels, where each {{Mvar|T_i}} has at most {{Mvar|i}} vertices, such that $T\_i\; \backslash leq\; T\_j$ does not hold for any

The TREE sequence begins $\backslash text\{TREE\}(1)=1$, $\backslash text\{TREE\}(2)=3$, before $\backslash text\{TREE\}(3)$ suddenly explodes to a value so large that many other "large" combinatorial constants, such as Friedman's $n(4)$, $n^\{n(5)\}(5)$, and Graham's number,{{ref label|n_k|b|^ b}} are extremely small by comparison. A lower bound for $n(4)$, and, hence, an extremely weak lower bound for $\backslash text\{TREE\}(3)$, is $A^\{A(187196)\}(1)$.{{ref label|Ackermann|c|^ c}}{{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}} Graham's number, for example, is much smaller than the lower bound $A^\{A(187196)\}(1)$, which is approximately $g\_\{3\; \backslash uparrow^\{187196\}\; 3\}$, where $g\_x$ is Graham's function.

• Paris–Harrington theorem
• Kanamori–McAloon theorem
• Robertson–Seymour theorem

:{{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_i,...,x_2i is a subsequence of any later block x_j,...,x_2j.{{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)}} $n(1)\; =\; 3,\; n(2)\; =\; 11,\; \backslash ,\backslash textrm\{and\}\backslash ,\; n(3)\; >\; 2\; \backslash uparrow^\{7197\}\; 158386$.

:{{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) = 2n, A(k+1, 1) = A(k, 1), A(k+1, n+1) = A(k, A(k+1, n)).

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 Γ₀? 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

|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

|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