Kruskal's Theorem
   HOME

TheInfoList



OR:

In
mathematics Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
, Kruskal's tree theorem states that the set of finite
tree In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, e.g., including only woody plants with secondary growth, only ...
s over a well-quasi-ordered set of labels is itself well-quasi-ordered under
homeomorphic In mathematics and more specifically in topology, a homeomorphism ( from Greek roots meaning "similar shape", named by Henri Poincaré), also called topological isomorphism, or bicontinuous function, is a bijective and continuous function betw ...
embedding. A
finitary In mathematics and logic, an operation is finitary if it has finite arity, i.e. if it has a finite number of input values. Similarly, an infinitary operation is one with an infinite number of input values. In standard mathematics, an operat ...
application of the theorem gives the existence of the fast-growing TREE function. TREE(3) is largely accepted to be one of the largest simply defined finite numbers, dwarfing other large numbers such as
Graham's number Graham's number is an Large numbers, immense number that arose as an upper bound on the answer of a problem in the mathematical field of Ramsey theory. It is much larger than many other large numbers such as Skewes's number and Moser's number, bot ...
and
googolplex A googolplex is the large number 10, or equivalently, 10 or . Written out in ordinary decimal notation, it is 1 followed by 10100 zeroes; that is, a 1 followed by a googol of zeroes. Its prime factorization is 2 ×5. History In 1920, ...
.


History

The
theorem In mathematics and formal logic, a theorem is a statement (logic), statement that has been Mathematical proof, proven, or can be proven. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to esta ...
was
conjecture In mathematics, a conjecture is a conclusion or a proposition that is proffered on a tentative basis without proof. Some conjectures, such as the Riemann hypothesis or Fermat's conjecture (now a theorem, proven in 1995 by Andrew Wiles), ha ...
d by
Andrew Vázsonyi Andrew Vázsonyi (1916–2003), also known as Endre Weiszfeld and Zepartzatt Gozinto) was a Hungarian mathematician and operations researcher. He is known for Weiszfeld's algorithm for minimizing the sum of distances to a set of points, and for ...
and proved by ; a short proof was given by . It has since become a prominent example in
reverse mathematics Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
as a statement that cannot be proved in ATR0 (a
second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation of mathematics, foundation for much, but not all, ...
theory with a form of
arithmetical transfinite recursion In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. A precur ...
). In 2004, the result was generalized from trees to
graph Graph may refer to: Mathematics *Graph (discrete mathematics), a structure made of vertices and edges **Graph theory, the study of such graphs and their properties *Graph (topology), a topological space resembling a graph in the sense of discret ...
s as the
Robertson–Seymour theorem In graph theory, the Robertson–Seymour theorem (also called the graph minors theorem) states that the undirected graphs, partially ordered by the graph minor relationship, form a well-quasi-ordering. Equivalently, every family of graphs that is ...
, a result that has also proved important in reverse mathematics and leads to the even-faster-growing SSCG function, which dwarfs \text(3).


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 with a
root In vascular plants, the roots are the plant organ, organs of a plant that are modified to provide anchorage for the plant and take in water and nutrients into the plant body, which allows plants to grow taller and faster. They are most often bel ...
, and given vertices , , call a ''successor'' of if the unique path from the root to contains , and call an ''immediate successor'' of if additionally the path from to contains no other vertex. Take to be a
partially ordered set In mathematics, especially order theory, a partial order on a Set (mathematics), set is an arrangement such that, for certain pairs of elements, one precedes the other. The word ''partial'' is used to indicate that not every pair of elements need ...
. If , are rooted trees with vertices labeled in , we say that is ''inf-embeddable'' in and write T_1 \leq T_2 if there is an
injective map In mathematics, an injective function (also known as injection, or one-to-one function ) is a function (mathematics), function that maps Distinct (mathematics), distinct elements of its domain to distinct elements of its codomain; that is, im ...
from the vertices of to the vertices of such that: *For all vertices of , the label of precedes the label of F(v); *If is any successor of in , then F(w) is a successor of F(v); and *If , are any two distinct immediate successors of , then the path from F(w_1) to F(w_2) in contains F(v). Kruskal's tree theorem then states:
If is well-quasi-ordered, then the set of rooted trees with labels in is well-quasi-ordered under the inf-embeddable order defined above. (That is to say, given any infinite sequence of rooted trees labeled in , there is some i so that T_i \leq T_j.)


Friedman's work

For a
countable In mathematics, a Set (mathematics), set is countable if either it is finite set, finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function fro ...
label set , Kruskal's tree theorem can be expressed and proven using
second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation of mathematics, foundation for much, but not all, ...
. However, like
Goodstein's theorem In mathematical logic, Goodstein's theorem is a statement about the natural numbers, proved by Reuben Goodstein in 1944, which states that every Goodstein sequence (as defined below) eventually terminates at 0. Laurence Kirby and Jeff Paris showed ...
or the
Paris–Harrington theorem In mathematical logic, the Paris–Harrington theorem states that a certain claim in Ramsey theory, namely the strengthened finite Ramsey theorem, which is expressible in Peano arithmetic, is not provable in this system. That Ramsey-theoretic clai ...
, 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 Harvey Friedman may refer to: * Harvey Friedman (mathematician) Harvey Friedman (born 23 September 1948)Handbook of Philosophical Logic, , p. 38 is an American mathematical logician at Ohio State University in Columbus, Ohio. He has worked on ...
in the early 1980s, an early success of the field of reverse mathematics. In the case where the trees above are taken to be unlabeled (that is, in the case where has size one), Friedman found that the result was unprovable in ATR0, thus giving the first example of a predicative result with a provably impredicative proof. This case of the theorem is still provable by Π-CA0, but by adding a "gap condition" to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system. Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π-CA0.
Ordinal analysis In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory ha ...
confirms the strength of Kruskal's theorem, with the
proof-theoretic ordinal In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has ...
of the theorem equaling the
small Veblen ordinal In mathematics, the small Veblen ordinal is a certain large countable ordinal, named after Oswald Veblen. It is occasionally called the Ackermann ordinal, though the Ackermann ordinal described by is somewhat smaller than the small Veblen ordinal ...
(sometimes confused with the smaller
Ackermann ordinal In mathematics, the Ackermann ordinal is a certain large countable ordinal, named after Wilhelm Ackermann. The term "Ackermann ordinal" is also occasionally used for the small Veblen ordinal, a somewhat larger ordinal. There is no standard ...
).


Weak tree function

Suppose that P(n) is the statement: :There is some such that if is a finite sequence of unlabeled rooted trees where has i+n vertices, then T_i \leq T_j for some i. All the statements P(n) are true as a consequence of Kruskal's theorem and
Kőnig's lemma Kőnig's lemma or Kőnig's infinity lemma is a theorem in graph theory due to the Hungarian mathematician Dénes Kőnig who published it in 1927. It gives a sufficient condition for an infinite graph to have an infinitely long path. The computab ...
. For each ,
Peano arithmetic In mathematical logic, the Peano axioms (, ), also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nea ...
can prove that P(n) is true, but Peano arithmetic cannot prove the statement "P(n) is true for all ". Moreover, the length of the shortest
proof Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a co ...
of P(n) in Peano arithmetic grows phenomenally fast as a function of , far faster than any
primitive recursive function In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
or the
Ackermann function In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total function, total computable function that is not Primitive recursive function, primitive recursive. ...
, for example. The least for which P(n) holds similarly grows extremely quickly with '.


TREE function

By incorporating labels, Friedman defined a far faster-growing function. For a positive
integer An integer is the number zero (0), a positive natural number (1, 2, 3, ...), or the negation of a positive natural number (−1, −2, −3, ...). The negations or additive inverses of the positive natural numbers are referred to as negative in ...
', take \text(n) to be the largest ' so that we have the following: : There is a sequence of rooted trees labelled from a set of labels, where each ' has at most vertices, such that T_i \leq T_j does not hold for any i. The TREE sequence begins \text(1)=1, \text(2)=3, before \text(3) suddenly explodes to a value so large that many other "large" combinatorial constants, such as Friedman's ''n(4)'', ''n^(5)'', and
Graham's number Graham's number is an Large numbers, immense number that arose as an upper bound on the answer of a problem in the mathematical field of Ramsey theory. It is much larger than many other large numbers such as Skewes's number and Moser's number, bot ...
, are extremely small by comparison. A
lower bound In mathematics, particularly in order theory, an upper bound or majorant of a subset of some preordered set is an element of that is every element of . Dually, a lower bound or minorant of is defined to be an element of that is less th ...
for ''n(4)'', and, hence, an ''extremely'' weak lower bound for \text(3), is ''A^(1)''. Graham's number, for example, is much smaller than the lower bound ''A^(1)'', which is approximately g_, where g_x is Graham's function.


See also

*
Paris–Harrington theorem In mathematical logic, the Paris–Harrington theorem states that a certain claim in Ramsey theory, namely the strengthened finite Ramsey theorem, which is expressible in Peano arithmetic, is not provable in this system. That Ramsey-theoretic clai ...
*
Kanamori–McAloon theorem In mathematical logic, the Kanamori–McAloon theorem, due to , gives an example of an incompleteness in Peano arithmetic, similar to that of the Paris–Harrington theorem. They showed that a certain finitistic theorem in Ramsey theory is not prova ...
*
Robertson–Seymour theorem In graph theory, the Robertson–Seymour theorem (also called the graph minors theorem) states that the undirected graphs, partially ordered by the graph minor relationship, form a well-quasi-ordering. Equivalently, every family of graphs that is ...


Notes

: Friedman originally denoted this function by ''TR'' 'n'' : ''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'',...,x2''i'' is a subsequence of any later block x''j'',...,x2''j''. n(1) = 3, n(2) = 11, \,\textrm\, n(3) > 2 \uparrow^ 158386. : ''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 In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive. All primitive recursive functions are total ...
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 Bibliography * * * * * * * * {{Use dmy dates, date=March 2024 Mathematical logic Order theory Theorems in discrete mathematics Trees (graph theory) Wellfoundedness