Kruskal's tree theorem

In mathematics, Kruskal's tree theorem states that the set of finite trees over a well-quasi-ordered set of labels is itself well-quasi-ordered under homeomorphic embedding.

History

The

).

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 ${\displaystyle {\text{TREE}}(3)}$. A finitary application of the theorem gives the existence of the fast-growing TREE function.

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 T with a

, and given vertices v, w, call w a successor of v if the unique path from the root to w contains v, and call w an immediate successor of v if additionally the path from v to w contains no other vertex.

Take X to be a partially ordered set. If T₁, T₂ are rooted trees with vertices labeled in X, we say that T₁ is inf-embeddable in T₂ and write ${\displaystyle T_{1}\leq T_{2}}$ if there is an

F from the vertices of T₁ to the vertices of T₂ such that:

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

Kruskal's tree theorem then states:

If X is well-quasi-ordered, then the set of rooted trees with labels in X is well-quasi-ordered under the inf-embeddable order defined above. (That is to say, given any infinite sequence T₁, T₂, … of rooted trees labeled in X, there is some ${\displaystyle i<j}$ so that ${\displaystyle T_{i}\leq T_{j}}$.)

Friedman's work

For a

Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π¹
₁-CA₀.

Weak tree function

Suppose that ${\displaystyle P(n)}$ is the statement:

There is some m such that if T₁, ..., T_m is a finite sequence of unlabeled rooted trees where T_i has ${\displaystyle i+n}$ vertices, then ${\displaystyle T_{i}\leq T_{j}}$ for some ${\displaystyle i<j}$.

All the statements ${\displaystyle P(n)}$ are true as a consequence of Kruskal's theorem and Kőnig's lemma. For each n, Peano arithmetic can prove that ${\displaystyle P(n)}$ is true, but Peano arithmetic cannot prove the statement "${\displaystyle P(n)}$ is true for all n".^[7] Moreover, the length of the shortest proof of ${\displaystyle P(n)}$ in Peano arithmetic grows phenomenally fast as a function of n, far faster than any primitive recursive function or the Ackermann function, for example.^{[citation needed]} The least m for which ${\displaystyle P(n)}$ holds similarly grows extremely quickly with n.

Define ${\displaystyle {\text{tree}}(n)}$, the weak tree function, as the largest m so that we have the following:

There is a sequence T₁, ..., T_m of unlabeled rooted trees, where each T_i has at most ${\displaystyle i+n}$ vertices, such that ${\displaystyle T_{i}\leq T_{j}}$ does not hold for any ${\displaystyle i<j\leq m}$.

It is known that ${\displaystyle {\text{tree}}(1)=2}$, ${\displaystyle {\text{tree}}(2)=5}$, ${\displaystyle {\text{tree}}(3)\geq 844,424,930,131,960}$ (about 844 trillion), ${\displaystyle {\text{tree}}(4)\gg g_{64}}$ (where ${\displaystyle g_{64}}$ is Graham's number), and ${\displaystyle {\text{TREE}}(3)}$ (where the argument specifies the number of labels; see below) is larger than ${\displaystyle \mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{8}(7)}(7)}(7)}(7)}(7).}$

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

By incorporating labels, Friedman defined a far faster-growing function.^[8] For a positive integer n, take ${\displaystyle {\text{TREE}}(n)}$^[a] to be the largest m so that we have the following:

There is a sequence T₁, ..., T_m of rooted trees labelled from a set of n labels, where each T_i has at most i vertices, such that ${\displaystyle T_{i}\leq T_{j}}$ does not hold for any ${\displaystyle i<j\leq m}$.

The TREE sequence begins ${\displaystyle {\text{TREE}}(1)=1}$, ${\displaystyle {\text{TREE}}(2)=3}$, then suddenly, ${\displaystyle {\text{TREE}}(3)}$ explodes to a value that is so big that many other "large" combinatorial constants, such as Friedman's ${\displaystyle n(4)}$, ${\displaystyle n^{n(5)}(5)}$, and

for ${\displaystyle n(4)}$, and, hence, an extremely weak lower bound for ${\displaystyle {\text{TREE}}(3)}$, is ${\displaystyle A^{A(187196)}(1)}$.^[c][9] Graham's number, for example, is much smaller than the lower bound ${\displaystyle A^{A(187196)}(1)}$. It is approximately ${\displaystyle g_{3\uparrow ^{187196}3}}$, where ${\displaystyle g_{x}}$ is Graham's function.

See also

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

Notes

^{^ a} Friedman originally denoted this function by TR[n].

^{^ 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.^[10] ${\displaystyle n(1)=3,n(2)=11,\,{\textrm {and}}\,n(3)>2\uparrow ^{7197}158386}$.

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)).

References

Citations

Bibliography

• Friedman, Harvey M. (2002), Internal finite tree embeddings. Reflections on the foundations of mathematics (Stanford, CA, 1998), Lect. Notes Log., vol. 15, Urbana, IL: Assoc. Symbol. Logic, pp. 60–91,
  MR 1943303
• MR 1129778
• MR 0111704
• Marcone, Alberto (2001), "Wqo and bqo theory in subsystems of second order arithmetic" (PDF), Reverse Mathematics, 21: 303–330
• S2CID 251095188
• Rathjen, Michael; Weiermann, Andreas (1993), "Proof-theoretic investigations on Kruskal's theorem" (PDF), Annals of Pure and Applied Logic, 60 (1): 49–88,
  MR 1212407
• Simpson, Stephen G. (1985), "Nonprovability of certain combinatorial properties of finite trees", in Harrington, L. A.; Morley, M.; Scedrov, A.; et al. (eds.), Harvey Friedman's Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland, pp. 87–117
• Smith, Rick L. (1985), "The consistency strengths of some finite forms of the Higman and Kruskal theorems", in Harrington, L. A.; Morley, M.; Scedrov, A.; et al. (eds.), Harvey Friedman's Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland, pp. 119–136