Preorder

A preorder is a set equipped with a reflexive and transitive relation; unlike a partial order, distinct elements may be mutually comparable in both directions.

For subsets of a preorder, Hoare domination means every source element has some greater or equal target element: $S{\le }_{H}T⟺\forall s\in S\exists t\in T(s\le t)$. It is reflexive and transitive. If the base is a well-quasi-ordering, its finite subsets are well-quasi-ordered by this relation; arbitrary subsets need not be, as the Rado order shows.

Finite subsets of a well-quasi-ordering, compared by Hoare domination preorder, form a well-quasi-ordering. Enumerate each finite subset as a word and apply Higman lemma: a subsequence embedding with increased letters supplies a domination witness for every source element. This does not assert the same result for the full power set.

A preorder is a well-quasi-ordering if every infinite sequence has indices $i<j$ with $x_i\le x_j$. An infinite sequence with no such pair is a bad sequence. This formulation handles combinatorial embedding relations that need not be antisymmetric on syntactic codes.

Every infinite sequence in a well-quasi-ordering has an infinite subsequence all of whose earlier terms precede its later terms. Some term must have infinitely many later terms above it: otherwise choose each new index outside the finitely many upper-cone index sets of the terms already chosen, producing a bad sequence. Apply the same observation successively inside the infinite upper-cone subsequence. Each restriction preserves all earlier inequalities, proving the assertion.

A finite Cartesian product of well-quasi-orderings is well-quasi-ordered in the componentwise order. Every infinite sequence in one well-quasi-order has an infinite nondecreasing subsequence: colour pairs by whether they are ordered, apply Ramsey's theorem, and exclude an all-bad subsequence. Restrict successively to such a subsequence in each coordinate. The same argument, or the infinite pigeonhole principle, proves closure under finite disjoint unions with no cross-component comparisons.

A quasi-order is better-quasi-ordered if every array into it from every barrier in better-quasi-order theory is good: some barrier members $s◃t$ satisfy $f(s)\le f(t)$. Singleton barriers recover the usual infinite-sequence condition for a well-quasi-ordering. The stronger condition is useful for infinitary closure operations for which well-quasi-ordering alone fails. Equivalently one may use continuous maps from infinite subsets of an infinite subset of the natural numbers, with the discrete topology on the range, and compare $X$ with $X\setminus \{\min X\}$.

If $Q$ is a better-quasi-ordering, its full power set is better-quasi-ordered by the Hoare domination preorder. A bad continuous array of subsets would allow a choice of $q_X\in A_X$ not below any member of $A_{X^{-}}$, where $X^{-}$ deletes the least element. Choose this witness as a fixed function of the two locally constant subsets. Then $X\mapsto q_X$ is a bad continuous array in better-quasi-order theory into $Q$, a contradiction. Empty source subsets cannot occur in a bad array because they precede every subset.

A continuous array takes infinite subsets of an infinite $A\subseteq \omega$, in the ordinary topology on infinite subsets, to a discrete preorder $Q$. It is bad if $F(X)\nleqq F(X\setminus \{\min X\})$ for every infinite $X$. A barrier in better-quasi-order theory array induces such a continuous array by evaluating its unique barrier initial segment. The continuous-array and barrier formulations of better-quasi-ordering are equivalent, using refinement of fronts to barriers in the reverse direction.

A barrier on an infinite $A\subseteq \mathbb{N}$ is a family of nonempty finite increasing sequences, viewed as finite subsets, no one contained properly in another, such that every infinite subset of $A$ has a member of the family as an initial segment. Write $s◃t$ if there is a finite increasing sequence $u$ of which $s$ is an initial segment and of which $t$ is an initial segment after its first term is deleted. This shift relation underlies the good-array definition of better-quasi-ordering.

Every finite coloring of a barrier in better-quasi-order theory has an infinite restriction on which all barrier members have the same color. It extends finite-dimensional Ramsey's theorem from fixed-length subsets to variable-length initial segments. A proof proceeds by well-founded induction on the initial-segment tree and a fusion construction selecting successively nested infinite tails. It implies that every finite set with the equality order is a better-quasi-ordering. The barrier/front partition proof is given in Section 3.2 of arxiv.org/pdf/1604.05866 .

The Rado order has domain $R=\{(m,n)\in {\mathbb{N}}^2:m<n\}$ and $(m,n){\le }_R(k,l)$ iff either $m=k$ and $n\le l$, or $n<k$. It is a well-quasi-ordering: either one row recurs infinitely in a sequence, or the first coordinates are unbounded and yield a cross-row comparison. Its infinite rows form an infinite antichain under Hoare domination preorder, showing that arbitrary-subset lifting need not preserve well-quasi-ordering.

The barrier in better-quasi-order theory $[\omega {]}^2$ has shifts $\{m,n\}◃\{n,l\}$ for $m<n<l$. Map each pair to the corresponding element of the Rado order. Neither clause of $(m,n){\le }_R(n,l)$ holds: the first coordinates differ, and the second coordinate of the first pair equals, rather than precedes, the first coordinate of the second. Thus this array is bad, although the Rado order is a well-quasi-ordering. It separates better-quasi-ordering from well-quasi-ordering.

If $Q$ is a well-quasi-ordering, its finite words form a well-quasi-ordering under subsequence embedding with coordinatewise increase of letters. A minimal bad sequence proof removes the last letter of selected words whose last letters form a nondecreasing subsequence, then contradicts minimality. The result implies finite-subset lifting of a well-quasi-order under Hoare domination preorder.

A bad sequence in a preorder is an infinite sequence with no indices $i<j$ satisfying $x_i\le x_j$. A preorder is a well-quasi-ordering precisely when no such sequence exists.

A minimal bad sequence chooses each successive object of least possible natural-number size among choices that admit an infinite bad continuation of the already fixed prefix. Replacing its next object by a strictly smaller one cannot leave a bad sequence. This contradiction principle proves Higman lemma and the labelled version of Kruskal's tree theorem.

Given a size bound with finitely many possible objects at each position, put finite bad sequences in a tree ordered by extension. The tree is finitely branching. Arbitrarily long bad sequences would give an infinite bad sequence by König infinity lemma. This compactness argument converts an infinite well-quasi-ordering theorem into a uniform finite length bound.

Finite rooted trees are well-quasi-ordered by rooted-tree homeomorphic embedding. Consequently every infinite sequence contains an earlier tree embedding into a later one. Size-controlled finite forms follow by applying König infinity lemma to the finitely branching tree of bad prefixes.

Finite rooted trees labelled in a well-quasi-ordering are a well-quasi-ordering under label-monotone tree embedding. A minimal bad sequence argument makes the collection of proper rooted subtrees a well-quasi-ordering; Higman lemma then compares their child lists while the root labels are compared in the label order.

For every natural parameter $k$, there is a finite length $N$ such that every sequence of $N$ finite rooted trees satisfying $|T_i|\le k+i$ has an earlier tree homeomorphically embedding into a later tree. It is a true finite-combinatorial principle unprovable in Peano arithmetic and in arithmetical transfinite recursion theory. Each fixed-parameter instance can still be verified by a sufficiently large finite search.