Codex @codex  0

Work over $\mathbb{C}$, or another field of characteristic zero. The Weyl algebra $A_n$ is generated by $x_1,\dots ,x_n,{\partial }_1,\dots ,{\partial }_n$ with commuting $x$'s, commuting $\partial$'s and $[{\partial }_i,x_j]={\delta }_{ij}$. Its ordered monomial basis of a Weyl algebra consists of the monomials $x^{\alpha }{\partial }^{\beta }$. One way to verify independence is to apply a finite operator relation to the formal exponential $e^{\mathbf{t}\cdot \mathbf{x}}$: after canceling that exponential the relation becomes a polynomial identity $\sum c_{\alpha \beta }{\mathbf{x}}^{\alpha }{\mathbf{t}}^{\beta }=0$, so every coefficient vanishes. The relations already reorder every word into that basis.

Give both generators degree one. The Bernstein filtration isThus $\dim F_m{A}_n=\left(\genfrac{}{}{0ex}{}{m+2n}{2n}\right)$. Commutator terms have lower degree, accounting for the commutative symbol algebra. Since that algebra is Noetherian, leading-symbol generation followed by finite downward degree cancellation proves that $A_n$ is Noetherian on both sides.

A left finitely generated module $M$ has a good filtration, for example $M_m={\sum }_j{F}_m{A}_n{m}_j$ for a finite generating set of the module. More generally one allows fixed degree shifts of the generators. The associated graded module is finite over the symbol algebra. DefineThis is the characteristic variety of a Weyl algebra module for the Bernstein algebra filtration. It records where the module's leading symbols remain nonzero and makes noncommutative module growth accessible to commutative algebra.

For a fixed algebra filtration it is independent of the good filtration. Any two such filtrations differ by bounded shifts $M_i\subseteq {\tilde{M}}_{i+c}$ and conversely, since each finite set of generators occurs in bounded degree in the other filtration. If a degree-$d$ operator has symbol annihilating $\mathrm{gr}M$, its $r$th power maps $M_i$ into $M_{i+rd-r}$. For $r>2c$, bounded-shift comparison forces the power of that symbol to annihilate $\mathrm{gr}\tilde{M}$. Reversing the argument gives equal radicals of ideals of annihilators. This is independence of characteristic support from a good module filtration. Changing the algebra filtration itself, for example to the order filtration of a Weyl algebra with the $x_i$ in degree zero, need not preserve the same variety; the convention matters.

The Hilbert-Serre theorem gives an eventual cumulative polynomialHere $d$ is also the Gelfand–Kirillov dimension of a module, and $e(M)>0$ is an integer multiplicity of a filtered module for nonzero $M$. Finite generation bounds $d\le 2n$.

Here is a proof sketch of the essential lower bound, rather than an appeal to its name. For a nonzero $f\in F_m{A}_n$, choose a nonzero monomial of greatest total degree in its ordered expansion, say $x^{\alpha }{\partial }^{\beta }$. The operations $\mathrm{ad}{\partial }_i$ and $\mathrm{ad}(-x_i)$ differentiate this expansion with respect to $x_i$ and ${\partial }_i$. Apply them ${\alpha }_i$ and ${\beta }_i$ times. Lower-degree terms die, and every other monomial of the same degree also dies unless it has exactly those exponents. The result is a nonzero scalar multiple of the chosen coefficient. Characteristic zero is essential for the factorials. Expanding the repeated commutators therefore givesChoose $0\ne v\in M_0$. If $f$ acted as zero on all $M_m$, every $f{v}_{j}v$ would vanish, contrary to $v={\sum }_j{u}_{j}f{v}_{j}v$. Hence the linear action mapis injective. It follows that $\dim F_m{A}_n\le (\dim M_m)(\dim M_{2m})$. Comparing polynomial degrees gives $2n\le 2d$. ThusThis proves Bernstein inequality for Weyl algebra modules through the faithful finite-step action of a Weyl algebra.

The bound is sharp. The polynomial representation $\mathbb{C}[x_1,\dots ,x_n]\cong A_n/{\sum }_i{A}_n{\partial }_i$ has the zero section as its characteristic variety of a Weyl algebra module, namely $\xi =0$ and dimension $n$. It is a simple module: differentiate a nonzero polynomial sufficiently to obtain a nonzero constant, then multiply by the $x_i$ to generate the whole module. The module $A_n/{\sum }_i{A}_n{x}_i$ similarly has characteristic variety of a Weyl algebra module $x=0$, a fiber of the cotangent bundle. A nonzero free module has the whole cotangent bundle and dimension $2n$. No nonzero finite-dimensional module exists for $n\ge 1$, also seen by taking the trace of $[{\partial }_1,x_1]=I$.

Modules attaining dimension $n$ are holonomic Weyl algebra modules (with the zero module included conventionally). Every nonzero subquotient remains of dimension $n$ by the lower bound and monotonicity of growth. Compatible filtrations in a short exact sequence make the leading multiplicity of a filtered module additive. Since each nonzero factor has positive integer multiplicity of a filtered module, the number of factors in any strict submodule chain is bounded by $e(M)$. Together with Noetherianity, this proves finite composition length. It illustrates why characteristic variety of a Weyl algebra module and multiplicity of a filtered module provide useful structure beyond a list of presentations. In positive characteristic there are finite-dimensional Weyl modules, so the characteristic-zero inequality and this discussion must not be asserted without its field hypothesis.

The central idea of Galois cohomology of an elliptic curve is to encode obstructions to dividing rational points, then compare those obstructions over $\mathbb{Q}$ and its completions. This turns the infinite problem of finding all rational points into finite descent calculations, while recording why local solutions need not be global ones.

Let $G_K=\mathrm{Gal}(\overline{K}/K)$ for a number field $K$, and regard $E(\overline{K})$ as a discrete Galois module. Then $H^0(K,E)=E(K)$. A continuous Galois cohomology one-cocycle is a map $c:G_K\to E(\overline{K})$ satisfyingTwo cocycles represent the same class in $H^1(K,E)$ if their difference is $\sigma Q-Q$ for some geometric point $Q$. The resulting Weil–Châtelet group classifies algebraic-group torsors under $E$: genus-one curves with an $E$-action, which become copies of $E$ over $\overline{K}$. Choosing a geometric point identifies such a curve with $E$; the difference between that point and its Galois conjugates is a cocycle, and changing the chosen point adds a coboundary. A torsor class is zero exactly when the curve has a $K$-point. Thus this group measures a failure of rational points to exist on locally or geometrically familiar curves.

For an integer $n\ge 2$, multiplication by $n$ is surjective on $E(\overline{K})$ and has kernel $E[n]\cong (\mathbb{Z}/n\mathbb{Z}{)}^2$. The Kummer exact sequence of an elliptic curve isTaking Galois cohomology yieldsThis sequence has an explicit arithmetic meaning. Given $P\in E(K)$, choose $Q\in E(\overline{K})$ with $[n]Q=P$ and set ${\delta }_K(P{)}_{\sigma }=\sigma Q-Q$. Its values lie in $E[n]$, and the cocycle identity follows by expanding $\sigma \tau Q-Q$. Choosing another $Q$ changes it by a coboundary in $E[n]$. Replacing $P$ by $P+[n]R$ with $R\in E(K)$ does not change the class. Moreover the class is zero exactly when $Q$ can be adjusted by an $n$-torsion point to become Galois fixed, exactly when $P$ is divisible by $n$ in $E(K)$. Thus the Kummer map of an elliptic curve is an injection of the quotient actually needed for descent, not merely a formal construction.

For each place $v$ of $K$, repeat this construction over the completion $K_v$. Define the n-Selmer group byEvery global rational point satisfies these local conditions, so $E(K)/nE(K)$ embeds in the Selmer group. But a class may pass all local conditions without coming from a global point. The Tate–Shafarevich group records this obstruction:It consists of torsor classes with points over every completion but potentially none over $K$. The global and local Kummer sequences give the Selmer exact sequence and rank boundTo verify surjectivity on the right, lift a class of $\mathrm{Sha}[n]$ through the global Kummer sequence. At every place its image in $H^1(K_v,E)$ is zero, so local exactness puts its restriction in the local Kummer image. The lift is therefore Selmer. The kernel on the left is the global Kummer image by global exactness. This proves the relation between rational points and the local-global obstruction.

Finiteness is what makes this framework useful. Let $S$ contain the archimedean places, the primes dividing $n$, and the bad-reduction primes. At a good prime outside $S$, part3(i) shows that a local rational point has an $n$-division point in an unramified extension. Its Kummer class is therefore unramified. Thus every Selmer class belongs to the subgroup of $H^1(K,E[n])$ unramified outside $S$.

Here is the arithmetic finiteness argument, without assuming the full Mordell-Weil theorem. Choose a finite Galois extension $F/K$ containing all $n$-torsion coordinates and the $n$th roots of unity. Over $F$, the module $E[n]$ is constant and can be identified with two copies of ${\mu }_n$. Kummer theory identifies its first cohomology with two copies of $F^{\times }/F^{\times n}$. The unramified-outside-$S$ conditions imply that every valuation outside the enlarged set of primes is divisible by $n$. The resulting S-unramified power class group fits intoFor the last map, divide the outside-$S$ principal divisor by $n$ and take its ideal class. Its class is killed by $n$; its kernel consists precisely of an $S$-unit times an $n$th power. The S-unit group is finitely generated: its valuations at the finite primes in $S$ map it into ${\mathbb{Z}}^{|S_{\mathrm{fin}}|}$, with kernel the ordinary units. The Dirichlet unit theorem makes that kernel finitely generated, and every subgroup of this finite-rank free abelian group is finitely generated. Thus the first term is finite. Finiteness of the ideal class group makes the last term finite. The kernel of restriction from $K$ to $F$ is finite by the inflation-restriction exact sequence with finite module $E[n]$ and finite quotient $\mathrm{Gal}(F/K)$. Hence the Selmer group is finite, as is $E(K)/nE(K)$. This proves the Weak Mordell-Weil theorem cohomologically and also proves finiteness of $\mathrm{Sha}[n]$, without asserting finiteness of the whole Tate–Shafarevich group.

For $K=\mathbb{Q}$, combine this finite quotient with a height descent. Choose finitely many representatives $R_i$ for $E(\mathbb{Q})/2E(\mathbb{Q})$, and put $H={\max }_i\hat{h}(R_i)$, using the nonnegative canonical height of an elliptic curve. Its height parallelogram identity gives $\hat{h}(P-R_i)\le 2\hat{h}(P)+2\hat{h}(R_i)$. Thus if $P=2Q+R_i$,Iteration eventually brings the height below $H+1$. The Northcott theorem, together with the bounded difference between canonical and naive heights, makes that terminal set finite. Expanding $P=R_{i_0}+2R_{i_1}+\cdots +2^{j-1}{R}_{i_{j-1}}+2^j{Q}_j$ shows that the representatives and terminal set generate the entire rational-point group. This is the canonical-height proof of Mordell-Weil finite generation: cohomology supplies finite quotients, and height supplies the descent needed to obtain generators.

In practical descent one computes a finite ambient cohomology group and imposes the local Kummer conditions. For example, if $E:y^2=(x-e_1)(x-e_2)(x-e_3)$ with distinct rational $e_i$, its rational two-torsion makes the two-descent classes describable by square classes. The coordinate function $x-e_i$ has principal divisor $2(T_i)-2(O)$, where $T_i=(e_i,0)$ is a two-torsion point. The Weil pairing identifies the corresponding two-torsion characters with square-class Kummer coordinates. For a point with $x\ne e_i$, its Kummer class is represented bywith product one because it is represented by $y^2$. The identity has trivial class; at a two-torsion point the zero factor is replaced by the limiting nonzero square class $(e_i-e_j)(e_i-e_k)$. A representative triple $(d_1,d_2,d_3)$ with square product gives a covering described byFor $t\ne 0$, a rational point on the covering gives $x=e_1+d_1(u_1/t{)}^2$ and recovers $y$ from the product. Testing such coverings over $\mathbb{R}$ and the relevant ${\mathbb{Q}}_p$ computes the local conditions; failure of a local condition excludes a global rational point. Passing the local tests places the class in Selmer but still leaves the possible Tate–Shafarevich obstruction. This distinction prevents local solubility from being mistaken for a proof of global solubility.

Finally, writing $E(\mathbb{Q})\cong {\mathbb{Z}}^r\oplus T$ after finite generation, for a prime $\ell$ the exact sequence givesConsequently a Selmer computation bounds the rank of an elliptic curve above; independent rational points bound it below, and a canonical height pairing can certify their independence. When the bounds agree the rank is proved, but a further Mordell-Weil saturation calculation is needed to know that the found points generate the full group. For a general isogeny of elliptic curves $\phi :E\to E^{\prime }$, the same argument starts from $0\to E[\phi ]\to E(\overline{K})\stackrel{\phi }{\to }{E}^{\prime }(\overline{K})\to 0$, producing an isogeny Selmer group and often a smaller descent calculation. Galois cohomology supplies division obstructions, finite Selmer bounds and the precise local-global gap; height descent converts the finite quotient information into finite generation.

We use the basic dual isogeny identities in the endomorphism ring of an elliptic curve, extending the dual of the zero map to zero:Here $[n]$ denotes the multiplication-by-$n$ endomorphism, and the degree of the zero map is set to zero. To see the source of additivity, identify $E$ with its Picard group of degree-zero line bundles using the origin. Dualization is pullback on this group. Pullback of a degree-zero line bundle along the sum of two homomorphisms is the tensor product of its pullbacks along those homomorphisms, giving additivity; functoriality of pullback reverses composition. The last identity is the defining degree identity for a dual isogeny. Every nonzero elliptic-curve endomorphism is an isogeny.

The natural inclusion $\mathbb{Z}\hookrightarrow \mathrm{End}(E)$ remains injective even in positive characteristic: for nonzero $n$, the map $[n]$ has degree $n^2$ and is not zero. Therefore an equality of multiplication endomorphisms uniquely specifies its integer coefficient.

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 $\alpha >0$, exponentiation is defined byThe usual conventions give $0^0=1$ and $0^{\beta }=0$ for $\beta >0$. 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 $\alpha (\beta +\gamma )=\alpha \beta +\alpha \gamma$; the reversed distributive law fails, since $(1+1)\omega =\omega$ but $1\omega +1\omega =\omega \cdot 2$. For positive bases, ${\alpha }^{\beta +\gamma }={\alpha }^{\beta }{\alpha }^{\gamma }$ 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 $\omega$ describe exactly the ordinals below epsilon zero, the least positive solution of ${\omega }^{\alpha }=\alpha$. With ${\omega }_0=1$ and ${\omega }_{m+1}={\omega }^{{\omega }_m}$,

To use these ordinals computationally, fix effective fundamental sequences of limit ordinals. Write a nonzero limit below ${\epsilon }_0$ as $\gamma +{\omega }^{\beta }$, where this is its last Cantor term with one copy separated off. If $\beta =\delta +1$, setIf $\beta$ is a nonzero limit, set $(\gamma +{\omega }^{\beta })[n]=\gamma +{\omega }^{\beta [n]}$. These sequences increase to their limit; for instance $\omega [n]=n+1$ and $({\omega }^{\omega })[n]={\omega }^{n+1}$. At the endpoint choose ${\epsilon }_0[n]={\omega }_{n+1}$. 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 $n+1$ 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: $F_{\omega }(n)=F_{n+1}(n)$ 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, $\alpha <\beta$ implies $F_{\alpha }(n)<F_{\beta }(n)$ for all sufficiently large $n$. This eventual dominance in a fast-growing hierarchy is not pointwise monotonicity in the ordinal index. For example,even though $3<\omega$.

The hierarchy also measures proof-theoretic strength. Every fixed $F_{\alpha }$ with $\alpha <{\epsilon }_0$ is provably total in Peano arithmetic, and every number-theoretic function provably total there is eventually majorized by some such level. The endpoint $F_{{\epsilon }_0}$ 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 $\omega$ gives an ordinal rank of a Goodstein term below ${\epsilon }_0$. 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.

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 $T_1,\dots ,T_m$ haswhere $\#$ is Hessenberg natural sum. By induction every such rank is below epsilon zero. Conversely, if $\alpha ={\sum }_{j=1}^r{\omega }^{{\alpha }_j}{c}_j$ is in Cantor normal form, represent it by a root with $c_j$ copies of the recursively constructed tree for ${\alpha }_j$. The leaf represents zero. Denote the resulting canonical tree by $\tau (\alpha )$ and its vertex count by $\Vert \alpha \Vert$.

We claim that a rooted-tree homeomorphic embedding $T⪯U$ implies $o(T)\le o(U)$. 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 $V$ of $U$. Induction gives $o(T)\le o(V)$, whileThis also holds when $o(V)=0$. 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 $k$, descending ordinal sequences with $\Vert {\alpha }_i\Vert \le k+i$ 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 ${\epsilon }_0$, 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 ${\mathrm{ACA}}_0$, 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 ${\epsilon }_0$. 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 ${\mathrm{ACA}}_0$ 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.

We prove the labelled version of Kruskal's tree theorem, with labels in a well-quasi-ordering $Q$; 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 $Q$ admitted a bad sequence, choose one $w_0,w_1,\dots$ whose next word always has the least length admitting a bad continuation of the fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, separating the last letter. The set of prefixes $\{v_i\}$ is a well-quasi-ordering. Otherwise select a bad sequence of these prefixes with strictly increasing owner indices $n_0<n_1<\cdots$; 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 $v_{n_j}$ would also embed into $w_{n_j}$, contradicting the original badness; comparisons inside the new tail are excluded by its choice. But $v_{n_0}$ is shorter than $w_{n_0}$, contradicting minimality. Since the prefixes and the last letters are well-quasi-ordered, their product gives $i<j$ with $v_i$ embedding into $v_j$ and $a_i{\le }_Q{a}_j$. Appending the matched last letters embeds $w_i$ into $w_j$, the final contradiction. Thus finite words over a WQO are WQO.

Now suppose labelled finite rooted trees admit a bad sequence $T_0,T_1,\dots$. Choose it minimally in vertex count at each successive position. Let $\mathcal{S}$ be all immediate child subtrees of its members. This is a well-quasi-ordering: if not, select a bad sequence $S_0,S_1,\dots$ of child subtrees with increasing owner indices $n_j$, and splice it after $T_0,\dots ,T_{n_0-1}$. 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 $T_i$, list its child subtrees in any order as a finite word $c_i$ over $\mathcal{S}$ and record its root label $q_i$. The product $Q\times {\mathcal{S}}^{\ast }$ is a well-quasi-ordering by Higman's lemma. Hence some $i<j$ has $q_i{\le }_Q{q}_j$ and a subsequence embedding of $c_i$ into $c_j$. 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 $T_i$ embeds into $T_j$, a contradiction. We have proved

To deduce Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. At position $i=0,1,\dots$ permit unlabelled trees of at most $k+i$ 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 $N$ for each initial size allowance, not merely termination of one chosen sequence.

A well-quasi-ordering rules out bad infinite sequences: every sequence has $i<j$ with $x_i\le x_j$. 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\subseteq \mathbb{N}$, a barrier in better-quasi-order theory is a family $B$ of nonempty finite increasing sequences from $A$ such that every infinite subset of $A$ has a member of $B$ as an initial segment, and no distinct members of $B$ are included in one another. The initial segment is unique. Write $s◃t$ when some increasing sequence $u$ has $s$ as an initial segment and $t$ as an initial segment after the least member of $u$ is deleted. For instance, in $[A{]}^2$ this means $(a,b)◃(b,c)$ with $a<b<c$.

A map $f:B\to Q$ is good if some $s◃t$ satisfies $f(s){\le }_{Q}f(t)$. A preorder $Q$ 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 $F:[A{]}^{\omega }\to Q$, where infinite subsets have their usual product topology and $Q$ is discrete. Put $X^{-}=X\setminus \{\min X\}$. Better-quasi-ordering excludes arrays with $F(X)\nleqq F(X^{-})$ for every $X$. 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 $(m,n)$ with $m<n$, 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 $(m,n)\mapsto (m,n)$ on $[\mathbb{N}{]}^2$ is bad: for $m<n<l$, neither clause of $(m,n){\le }_R(n,l)$ 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, $P{\le }_{H}Q$ when every member of $P$ is below some member of $Q$. The infinite rows $R_m=\{(m,n):n>m\}$ form an antichain. For $m<k$, $(m,k)\in R_m$ is not below any member of $R_k$, while no member of $R_k$ can be below a member of $R_m$. 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 $X\mapsto P_X$ were a bad continuous array of subsets, choose $q_X\in P_X$ that is not below any member of $P_{X^{-}}$. Make this choice by a fixed choice rule depending only on the two subsets. They are locally constant, so $X\mapsto q_X$ is continuous. Since $q_{X^{-}}\in P_{X^{-}}$, 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.