Use the reverse absorption order on the incline:This is exactly the relation given by the pairs . Indeed, if and , then by additive idempotence, associativity and commutativity. Conversely expresses as , so is one of these pairs.
Additive idempotence gives , hence reflexivity. If and , thenso the relation is transitive. In fact it is antisymmetric as well: and , together with commutativity, imply . Thus the relation is a partial order, and therefore a quasi-order. It is the reverse of the usual join order of an incline; keeping this reversal is essential for the well-quasi-ordering conclusion.
Both operations are order-preserving for this order. If , then by additive idempotence, while distributivity gives . The multiplicative absorption identity also saysThus multiplying a monomial by another factor moves upward in the reverse absorption order.
Suppose the incline is generated by . Repeated distributivity, followed by commutativity and additive idempotence, expresses every element as a finite nonempty sumNo multiplicative identity is assumed: a zero exponent means that the corresponding generator is omitted, and every displayed monomial has at least one factor. Different supports may represent the same element; uniqueness is unnecessary.
Associate to its upward-closed exponent setIf , each monomial of is either equal to, or a multiplicative extension of, a monomial of . It is absorbed by that earlier monomial, and hence by the full sum . Adding the terms of one at a time givesFor equal exponent vectors the first absorption is additive idempotence; for strictly larger vectors it is the incline's multiplicative absorption. Thus the issue is to prove that exponent upsets are well-quasi-ordered by reverse inclusion, not merely to apply Dickson's lemma to individual exponents.
We prove the reverse-inclusion well-quasi-ordering of monomial ideals, equivalently of all upward-closed subsets of , by induction on . For the sets are tails and the empty set; reverse inclusion orders their endpoints as , a well-order. The case , if needed for the induction, is just a finite family.
For an upset , let . These are upsets of and satisfy . They stabilize. Indeed the union has a finite minimal basis by Dickson's lemma: an infinite set of minimal elements would be an antichain in the componentwise well-quasi-ordering of . Each basis element appears in some slice, and after the largest of these finitely many indices the slice contains the entire upset .
Choose a stabilization index , and encode by the finite word and the final slice . The induction hypothesis makes slices a well-quasi-ordering by reverse inclusion. Higman's lemma, proved in Question 3 below, makes their finite words a well-quasi-ordering; finite product closure of well-quasi-orderings also compares the final slices. Thus in every infinite sequence of upsets there are earlier and later with a strictly increasing matching of the earlier pre-stabilization slices into the later ones, such thatSince and the -slices increase, for . For , . Therefore , completing the induction.
Now choose one finite support for each term of an arbitrary infinite sequence in the finitely generated incline. The result supplies with , and the preceding absorption calculation gives . Hence every finitely generated incline is well-quasi-ordered by the specified reverse absorption order. The proof allows all additional algebraic identifications among the generators.
A well-quasi-ordering rules out bad infinite sequences: every sequence has with . It behaves well under finite products and finite words, but infinitary constructions expose a limitation. Better-quasi-ordering, introduced by Nash-Williams, strengthens the sequence test to a test on families of finite initial segments, and thereby provides a robust theory of infinitary closure.
For an infinite , a barrier in better-quasi-order theory is a family of nonempty finite increasing sequences from such that every infinite subset of has a member of as an initial segment, and no distinct members of are included in one another. The initial segment is unique. Write when some increasing sequence has as an initial segment and as an initial segment after the least member of is deleted. For instance, in this means with .
A map is good if some satisfies . A preorder is a better-quasi-ordering when every such barrier map is good. Singleton barriers recover ordinary infinite sequences, soEquivalently, take a continuous array in better-quasi-order theory , where infinite subsets have their usual product topology and is discrete. Put . Better-quasi-ordering excludes arrays with for every . A barrier map gives a locally constant array by reading the unique initial segment; the converse uses refinement of the front of finite segments on which a continuous map becomes constant. This viewpoint makes the shift, rather than mere inclusion of subsets, central.
The implication is strict. The Rado order consists of pairs with , ordered byIt is a well-quasi-ordering. In any infinite sequence, either the first coordinates are unbounded, giving a later first coordinate above the earlier second coordinate, or one first coordinate occurs infinitely often and its second coordinates have a nondecreasing pair. But the barrier map on is bad: for , neither clause of holds. Thus the Rado order is WQO but not BQO.
The same example explains why strengthening the definition is useful. Order subsets by the Hoare domination preorder, when every member of is below some member of . The infinite rows form an antichain. For , is not below any member of , while no member of can be below a member of . Thus the full power set of a well-quasi-ordering need not be a well-quasi-ordering.
In contrast, power-set closure of better-quasi-orderings has a short array proof. If were a bad continuous array of subsets, choose that is not below any member of . Make this choice by a fixed choice rule depending only on the two subsets. They are locally constant, so is continuous. Since , it is a bad array into the original better-quasi-ordering, a contradiction. Empty subsets cannot be the source of a bad comparison. Thus the full power set, not just its finite subsets, preserves better-quasi-ordering under domination.
Further examples and closure principles show the scope of the theory. Every well-order is a better-quasi-ordering: a bad array would give a strictly descending ordinal sequence by successively deleting the least member of one infinite set. Every finite equality order is a better-quasi-ordering by the Nash-Williams barrier partition theorem, which makes a finite coloring of a barrier constant on an infinite restriction. The same theorem proves closure under finite products: color a bad product array by the first coordinate in which the shifted comparison fails, and pass to a homogeneous infinite restriction to obtain a bad coordinate array. Finite disjoint unions work by first homogenizing the component.
Nash-Williams' extension to countable transfinite sequences says that sequences of labels from a better-quasi-ordering, of arbitrary countable ordinal length, are again better-quasi-ordered by increasing label-monotone embeddings. It is an infinitary counterpart of Higman's lemma. Its formulation and logical strength are studied in arxiv.org/abs/math/9408204 . The point is not that every closure proof becomes elementary, but that barriers and continuous arrays supply the stable induction and partition framework absent from ordinary sequence tests. The modern account arxiv.org/pdf/1604.05866 develops this framework and the barrier partition theorem.
We prove the labelled version of Kruskal's tree theorem, with labels in a well-quasi-ordering ; the unlabelled result is its one-label case. A label-monotone tree embedding is an injective map of finite rooted trees preserving lowest common ancestors and increasing labels. Its root may map below the host root, and an edge may map to a path. These conventions distinguish rooted-tree homeomorphic embedding from the stricter adjacency-preserving relation, which is not well-quasi-ordered.
We will use two elementary consequences of well-quasi-ordering. Every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence: color pairs by whether the earlier element precedes the later one, apply Ramsey's theorem, and exclude an all-bad infinite set. Restricting successively in each coordinate proves finite product closure of well-quasi-orderings.
For completeness, here is the required proof of Higman's lemma. If finite words over admitted a bad sequence, choose one whose next word always has the least length admitting a bad continuation of the fixed prefix. No word is empty. Write , separating the last letter. The set of prefixes is a well-quasi-ordering. Otherwise select a bad sequence of these prefixes with strictly increasing owner indices ; this is possible because every finite initial set of owners supplies only finitely many prefixes, and a bad sequence cannot repeat a word. Thenis bad. An earlier original word embedding into would also embed into , contradicting the original badness; comparisons inside the new tail are excluded by its choice. But is shorter than , contradicting minimality. Since the prefixes and the last letters are well-quasi-ordered, their product gives with embedding into and . Appending the matched last letters embeds into , the final contradiction. Thus finite words over a WQO are WQO.
Now suppose labelled finite rooted trees admit a bad sequence . Choose it minimally in vertex count at each successive position. Let be all immediate child subtrees of its members. This is a well-quasi-ordering: if not, select a bad sequence of child subtrees with increasing owner indices , and splice it after . Every child subtree embeds into its owner, so a comparison from the prefix to the tail would contradict original badness. The splice is bad and its first replacement is strictly smaller, contradicting the minimal bad sequence choice.
For each , list its child subtrees in any order as a finite word over and record its root label . The product is a well-quasi-ordering by Higman's lemma. Hence some has and a subsequence embedding of into . Match the roots and use the chosen subtree embeddings in distinct target branches. Their union preserves lowest common ancestors and labels, and stretches only edge paths. Thus embeds into , a contradiction. We have proved
To deduce Friedman's finite form of Kruskal's theorem, fix . At position permit unlabelled trees of at most vertices. Up to isomorphism only finitely many trees are possible at each position. Form the finite bad-sequence tree whose nodes are finite bad sequences satisfying these bounds, ordered by extension. It is finitely branching. If there were arbitrarily long admissible bad sequences, König infinity lemma would give an infinite branch, contradicting Kruskal's tree theorem. ThereforeOne can instead use a fixed finite set of labels, giving a correspondingly parameterized finite statement by exactly the same proof. The crucial feature is a uniform bound for each initial size allowance, not merely termination of one chosen sequence.
The consistency implication needs more than the fact that the finite tree statement is unprovable in Peano arithmetic. Its mechanism is a concrete encoding of ordinal descent by bad finite-tree sequences, combined with the controlled-termination form of Gentzen ordinal reduction for arithmetic.
First define the natural-sum ordinal rank of a finite rooted tree. A leaf has rank zero, and a tree with immediate child subtrees haswhere is Hessenberg natural sum. By induction every such rank is below epsilon zero. Conversely, if is in Cantor normal form, represent it by a root with copies of the recursively constructed tree for . The leaf represents zero. Denote the resulting canonical tree by and its vertex count by .
We claim that a rooted-tree homeomorphic embedding implies . If the roots match, the source child subtrees embed into distinct target branches. By induction their ranks do not decrease; exponentiation and Hessenberg natural sum preserve these comparisons, and additional target branches only increase the sum. If the source root maps below the host root, its entire image lies in an immediate subtree of . Induction gives , whileThis also holds when . Thus the claim follows by induction on the host tree. In particular,
Consequently Friedman's finite form of Kruskal's theorem supplies slow well-ordering below epsilon zero: for each , descending ordinal sequences with have uniformly bounded length. Otherwise their canonical trees would be arbitrarily long admissible bad sequences. The notation system and its comparisons are primitive recursive, and there are only finitely many notations of bounded norm.
The proof-theoretic input is the following precise miniaturization lemma: for the standard effective Cantor normal form notation system below , slow well-ordering with linear norm control implies the formal consistency statement for Peano arithmetic. The Friedman–Smith controlled-termination theorem, stated in its general ordinal-analysis form in Section 2.2 of formal.hknu.ac.kr/Publi/kruskalJKMS.pdf , supplies this implication over arithmetical comprehension theory , whose first-order part is conservative over Peano arithmetic. This is an established proof-theoretic lemma, separate from the elementary tree-rank calculation above.
Here is why that lemma is a consistency result. Gentzen ordinal reduction for arithmetic assigns an alleged arithmetic contradiction an effective ordinal below . Reducing cuts and induction inferences preserves the contradictory end-sequent while strictly decreasing the assigned ordinal. A terminal normal derivation of a contradiction is excluded by inspection of the rules. The miniaturization argument converts this reduction/induction analysis into finite controlled descents: a contradictory proof would yield arbitrarily long descending notation sequences with a common initial allowance and linear norm control. Slow well-ordering excludes these. The control conversion is substantive; ordinary proof reductions must not simply be asserted to have linear-size growth. Gentzen's ordinal-reduction framework is discussed in math.stanford.edu/~feferman/papers/reductive.pdf .
Combining the coding with that precise termination lemma givesThus the finite combinatorial principle proves that no PA proof of a contradiction exists in the specified arithmetic metatheory. If consistent Peano arithmetic proved FFF, it would also prove its own formal consistency statement: the displayed implication is arithmetical and the first-order conservativity of transfers it to PA. This contradicts the Gödel second incompleteness theorem. It is the consistency implication, rather than unprovability by itself, that explains the strength of the finite tree principle.
Ordinal arithmetic describes the order types of well-ordered constructions. Its operations are defined by transfinite recursion, continuous in their right argument at limits. For addition,For multiplication,and, for , exponentiation is defined byThe usual conventions give and for . Ordinal addition concatenates orders, while ordinal multiplication takes a succession of copies of the left factor indexed by the right factor.
Ordinal addition and ordinal multiplication are associative but generally not commutative; exponentiation is not an associative operation. For example,The distributive identity is ; the reversed distributive law fails, since but . For positive bases, follows from the recursive definitions. These are order-type identities, not an extension of commutative integer arithmetic.
Every nonzero ordinal has a unique Cantor normal formComparisons are lexicographic in the exponent/coefficient list. Adding a later ordinal can erase smaller final terms of the earlier one, explaining noncommutativity. Hessenberg natural sum instead aligns equal exponents and adds their coefficients, producing a commutative operation. Finite recursive expressions formed from zero, sums and powers of describe exactly the ordinals below epsilon zero, the least positive solution of . With and ,
To use these ordinals computationally, fix effective fundamental sequences of limit ordinals. Write a nonzero limit below as , where this is its last Cantor term with one copy separated off. If , setIf is a nonzero limit, set . These sequences increase to their limit; for instance and . At the endpoint choose . The shift by one is a convention; changing it changes exact finite values, so it must be specified.
The fast-growing hierarchy now combines iteration at successors with diagonalization at limits:The superscript denotes repeated function composition, not exponentiation. ThusThe next level iterates an exponential-growth function times, yielding tower-like growth; further finite levels iterate the corresponding higher growth. Each fixed finite level is primitive recursive, and every unary primitive recursive function is eventually dominated by a sufficiently high finite level. The first limit diagonalizes over all of them: has Ackermannian growth and is not primitive recursive. Further limits give diagonals over already transfinite stretches of the hierarchy.
Transfinite induction proves totality for every fixed ordinal index in the chosen well-founded notation system: limit evaluation passes to a smaller index, while successor evaluation performs finitely many calls at the preceding index. For the standard fundamental sequences, implies for all sufficiently large . This eventual dominance in a fast-growing hierarchy is not pointwise monotonicity in the ordinal index. For example,even though .
The hierarchy also measures proof-theoretic strength. Every fixed with is provably total in Peano arithmetic, and every number-theoretic function provably total there is eventually majorized by some such level. The endpoint is a total recursive function in the usual mathematical metatheory but its totality is not provable in consistent PA. The classification is established in epub.ub.uni-muenchen.de/3843/1/3843.pdf . The distinction is between separately proving each fixed lower level and proving one uniform diagonal statement covering all lower levels; a theory cannot interchange those quantifiers without additional strength.
A related example is Goodstein's theorem. Changing the base in a hereditary base representation can increase the natural number dramatically, but replacing that base by gives an ordinal rank of a Goodstein term below . Subtracting one strictly decreases this rank, so an infinite nonterminating process would give an impossible ordinal descent. This illustrates the central connection: ordinal descent proves termination while fast-growing hierarchies measure how long finite terminating processes can last. The size of intermediate natural numbers need not resemble the simplicity of their ordinal termination measure.
Articles by others on the same topic
There are currently no matching articles.