H. Friedman's finite miniaturization of Kruskal's tree theorem
Hey, guys. You like large numbers, don't you?Today's topic is about a huge number related to Kruskal's tree theorem in graph theory. This is an important theorem that leads to Nash-Williams' BQO theory, Robertson–Seymour's graph minor theorem, and so on.
Kruskal's tree theorem is, of course, a theorem about trees. A tree is a connected acyclic graph. A rooted tree is a tree with a distinguished vertex called a root. A rooted tree can be thought of as a lower semilattice. A sequence of rooted finite trees $T_1,T_2,\dots,T_\ell$ is called bad if there is no infimum-preserving injection from $T_i$ to $T_j$ whenever $i\lt j$.
Kruskal's tree theorem states that the length of a bad sequence of rooted finite trees must be finite.
Okay, that's good to know. It's finite. So, how large is this finite number? How long can a bad sequence be?
The answer is ... unimaginably large. A mathematical logician, Harvery Friedman, introduced the following number:
Definition. The number ${\bf tree}(n)$ is defined as the length of a longest bad sequence of rooted trees where the $i$th tree $T_i$ in this sequence has at most $n+i$ vertices.Friedman found that this yields extraordinary huge numbers. For instance, it is known that:
${\bf tree}(3)$ is greater than $10000000000$.
And,
${\bf tree}(4)$ is greater than Graham's number.
Here, Graham's number is known as "the largest number ever used in a serious mathematical proof" which is published in the 1980 Guinness Book of World Records.