{"history":[],"article":{"id":"a6a8ac49-9216-4488-96b0-40631721f0f0","title":"Kruskal's tree theorem","slug":"kruskal-s-tree-theorem","content":":::summary\n:::\n\n# \nIn [mathematics](https://bliptext.com/articles/mathematics), **Kruskal's tree theorem** states that the set of finite [trees](https://bliptext.com/articles/tree-graph-theory) over a [well-quasi-ordered](https://bliptext.com/articles/well-quasi-ordering) set of labels is itself [well-quasi-ordered](https://bliptext.com/articles/well-quasi-ordering) under [homeomorphic](https://bliptext.com/articles/homeomorphism-graph-theory) embedding.\n\n# History\nThe [theorem](https://bliptext.com/articles/theorem) was [conjectured](https://bliptext.com/articles/conjecture) by [Andrew Vázsonyi](https://bliptext.com/articles/andrew-v-zsonyi) and [proved](https://bliptext.com/articles/mathematical-proof) by ; a short proof was given by.\nIt has since become a prominent example in [reverse mathematics](https://bliptext.com/articles/reverse-mathematics) as a statement that cannot be proved in ATR0 (a [second-order arithmetic](https://bliptext.com/articles/second-order-arithmetic) theory with a form of [arithmetical transfinite recursion](https://bliptext.com/articles/arithmetical-transfinite-recursion)).\nIn 2004, the result was generalized from trees to [graphs](https://bliptext.com/articles/graph-discrete-mathematics) as the [Robertson–Seymour theorem](https://bliptext.com/articles/robertson-seymour-theorem), a result that has also proved important in reverse mathematics and leads to the even-faster-growing [SSCG function](https://bliptext.com/articles/friedman-s-sscg-function), which dwarfs.\nA [finitary](https://bliptext.com/articles/finitary) application of the theorem gives the existence of the fast-growing **TREE function**.\n\n# Statement\nThe version given here is that proven by Nash-Williams; Kruskal's formulation is somewhat stronger.\nAll trees we consider are finite.\nGiven a tree T with a [root](https://bliptext.com/articles/rooted-tree), and given vertices v, w, call w a successor of v if the unique path from the [root](https://bliptext.com/articles/rooted-tree) to w contains v, and call w an immediate successor of v if additionally the path from v to w contains no other vertex.\nTake X to be a [partially ordered set](https://bliptext.com/articles/partially-ordered-set).\nIf\nT1\n,\nT2\nare rooted trees with vertices labeled in X, we say that\nT1\nis inf-embeddable in\nT2\nand write if there is an [injective map](https://bliptext.com/articles/injective-map) F from the vertices of\nT1\nto the vertices of\nT2\nsuch that:\nT1\n, the label of v precedes the label of F(v);\nT1\n, then F(w) is a successor of F(v); and\nw1\n,\nw2\nare any two distinct immediate successors of v, then the path from F(w_1) to F(w_2) in\nT2\ncontains F(v).\nKruskal's tree theorem then states:\n\"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\nT1, T2, …\nof rooted trees labeled in X, there is some i