Kruskal's tree theorem

Last updated

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.

Contents

History

The theorem was conjectured by Andrew Vázsonyi and proved by JosephKruskal  ( 1960 ); a short proof was given by CrispinNash-Williams  ( 1963 ). It has since become a prominent example in reverse mathematics as a statement that cannot be proved in ATR0 (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 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 root, 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 T1, T2 are rooted trees with vertices labeled in X, we say that T1 is inf-embeddable in T2 and write T1T2 if there is an injective map F from the vertices of T1 to the vertices of T2 such that

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 T1, T2, … of rooted trees labeled in X, there is some i < j so that TiTj.)

Friedman's work

For a countable label set 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 then-nascent field of reverse mathematics. In the case where the trees above are taken to be unlabeled (that is, in the case where X has size one), Friedman found that the result was unprovable in ATR0, [1] thus giving the first example of a predicative result with a provably impredicative proof. [2] This case of the theorem is still provable by Π1
1
-CA0, but by adding a "gap condition" [3] to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system. [4] [5] Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π1
1
-CA0.

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).[ citation needed ]

Weak tree function

Suppose that P(n) is the statement:

There is some m such that if T1, ..., Tm is a finite sequence of unlabeled rooted trees where Ti has i + n vertices, then Ti Tj for some i < j.

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

Define tree(n), the weak tree function, as the largest m so that we have the following:

There is a sequence T1, ..., Tm of unlabeled rooted trees, where each Ti has at most i + n vertices, such that Ti Tj does not hold for any i < j  m.

It is known that tree(1) = 2, tree(2) = 5, and tree(3)  844424930131960, tree(4) > Graham's number (by a lot) but TREE(3) (where the argument specifies the number of labels; see below) is larger than

To differentiate the two functions, "TREE" with all letters capitalized is the big TREE function and "tree" with all letters in lowercase is the weak tree function.

TREE function

A sequence of rooted trees labelled from a set of 3 labels (blue < red < green). The nth tree in the sequence contains at most n vertices, and no tree is inf-embeddable within any later tree in the sequence. TREE(3) is defined to be the longest possible length of such a sequence. TREE(3) sequence.png
A sequence of rooted trees labelled from a set of 3 labels (blue < red < green). The nth tree in the sequence contains at most n vertices, and no tree is inf-embeddable within any later tree in the sequence. TREE(3) is defined to be the longest possible length of such a sequence.

By incorporating labels, Friedman defined a far faster-growing function. [7] For a positive integer n, take TREE(n) [a] to be the largest m so that we have the following:

There is a sequence T1, ..., Tm of rooted trees labelled from a set of n labels, where each Ti has at most i vertices, such that Ti Tj does not hold for any i < j  m.

The TREE sequence begins TREE(1) = 1, TREE(2) = 3, then suddenly TREE(3) explodes to a value that is so big that many other "large" combinatorial constants, such as Friedman's n(4), nn(5)(5), and Graham's number, [b] are extremely small by comparison. A lower bound for n(4), and hence an extremely weak lower bound for TREE(3), is AA(187196)(1). [c] [8] Graham's number, for example, is much smaller than the lower bound AA(187196)(1). It is approximately , where gx is Graham's function.

See also

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 xi,...,x2i is a subsequence of any later block xj,...,x2j. [9] .
^ 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)).

Related Research Articles

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 eventually terminates at 0. Laurence Kirby and Jeff Paris showed that it is unprovable in Peano arithmetic. This was the third example of a true statement about natural numbers that is unprovable in Peano arithmetic, after the examples provided by Gödel's incompleteness theorem and Gerhard Gentzen's 1943 direct proof of the unprovability of ε0-induction in Peano arithmetic. The Paris–Harrington theorem gave another example.

<span class="mw-page-title-main">Kőnig's lemma</span> Mathematical result on infinite trees

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 computability aspects of this theorem have been thoroughly investigated by researchers in mathematical logic, especially in computability theory. This theorem also has important roles in constructive mathematics and proof theory.

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 contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones.

In graph theory, the Robertson–Seymour 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 closed under minors can be defined by a finite set of forbidden minors, in the same way that Wagner's theorem characterizes the planar graphs as being the graphs that do not have the complete graph K5 or the complete bipartite graph K3,3 as minors.

In mathematics, specifically order theory, a well-quasi-ordering or wqo on a set is a quasi-ordering of for which every infinite sequence of elements from contains an increasing pair with

<span class="mw-page-title-main">Cayley's formula</span> Number of spanning trees of a complete graph

In mathematics, Cayley's formula is a result in graph theory named after Arthur Cayley. It states that for every positive integer , the number of trees on labeled vertices is .

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

In mathematical logic, the Paris–Harrington theorem states that a certain combinatorial principle in Ramsey theory, namely the strengthened finite Ramsey theorem, which is expressible in Peano arithmetic, is not provable in this system. The combinatorial principle is however provable in slightly stronger systems.

Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction, as long as a certain other system used in the proof does not contain any contradictions either. This other system, today called "primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0", is neither weaker nor stronger than the system of Peano axioms. Gentzen argued that it avoids the questionable modes of inference contained in Peano arithmetic and that its consistency is therefore less controversial.

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

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 Ackermann (1951) is somewhat smaller than the small Veblen ordinal.

In mathematics, specifically in graph theory and number theory, a hydra game is a single-player iterative mathematical game played on a mathematical tree called a hydra where, usually, the goal is to cut off the hydra's "heads" while the hydra simultaneously expands itself. Hydra games can be used to generate large numbers or infinite ordinals or prove the strength of certain mathematical theories.

In computability theory, computational complexity theory and proof theory, a fast-growing hierarchy is an ordinal-indexed family of rapidly increasing functions fα: NN. A primary example is the Wainer hierarchy, or Löb–Wainer hierarchy, which is an extension to all α < ε0. Such hierarchies provide a natural way to classify computable functions according to rate-of-growth and computational complexity.

In computability theory, computational complexity theory and proof theory, the slow-growing hierarchy is an ordinal-indexed family of slowly increasing functions gα: NN. It contrasts with the fast-growing hierarchy.

In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, , together with induction for formulas with bounded quantifiers.

In mathematics, Gödel's speed-up theorem, proved by Gödel, shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems.

In mathematics, especially mathematical logic, graph theory and number theory, the Buchholz hydra game is a type of hydra game, which is a single-player game based on the idea of chopping pieces off a mathematical tree. The hydra game can be used to generate a rapidly growing function, , which eventually dominates all recursive functions that are provably total in "", and the termination of all hydra games is not provably total in .

In mathematics, S2S is the monadic second order theory with two successors. It is one of the most expressive natural decidable theories known, with many decidable theories interpretable in S2S. Its decidability was proved by Rabin in 1969.

References

Citations

  1. Simpson 1985, Theorem 1.8
  2. Friedman 2002, p. 60
  3. Simpson 1985, Definition 4.1
  4. Simpson 1985, Theorem 5.14
  5. Marcone 2001, p. 8–9
  6. Smith 1985, p. 120
  7. Friedman, Harvey (28 March 2006). "273:Sigma01/optimal/size". Ohio State University Department of Maths. Retrieved 8 August 2017.
  8. Friedman, Harvey M. (1 June 2000). "Enormous Integers In Real Life" (PDF). Ohio State University. Retrieved 8 August 2017.
  9. Friedman, Harvey M. (8 October 1998). "Long Finite Sequences" (PDF). Ohio State University Department of Mathematics. pp. 5, 48 (Thm.6.8). Retrieved 8 August 2017.

Bibliography