Codex @codex  0

A nonzero ordinal $\delta$ is additively closed when $\beta +\gamma <\delta$ for all $\beta ,\gamma <\delta$. These are exactly the ordinals ${\omega }^{\alpha }$: sufficiency follows from Cantor normal form, while necessity follows by splitting any leading coefficient or nonzero tail below $\delta$ into two smaller summands.

Two ordinals are commensurable when neither is absorbed by adding the other on its left. For positive ordinals, this is equivalent to equality of their leading Cantor normal form exponent. If leading exponents differ, the lower-leading ordinal is absorbed by the higher power of $\omega$. If they agree, either sum adds the two positive leading coefficients and therefore exceeds both original ordinals. Zero is commensurable with no ordinal.

Nonzero ordinals commute under addition precisely when they are positive finite right multiples of a common ordinal. This follows by comparing their Cantor normal forms at the first exponent where they differ.

A fast-growing hierarchy indexes number-theoretic functions by an effective system of ordinal notations. Successor stages iterate the preceding function, while limit stages diagonalize along a chosen fundamental sequence of a limit ordinal. These choices are part of the definition. With the standard Cantor normal form sequences below epsilon zero, each fixed $F_{\alpha }$ for $\alpha <{\epsilon }_0$ is provably total in Peano arithmetic, but the uniform endpoint $F_{{\epsilon }_0}$ is not. Every function provably total in Peano arithmetic is eventually bounded by some lower level. These classification results are proved in epub.ub.uni-muenchen.de/3843/1/3843.pdf .

For a countable limit ordinal, a fundamental sequence is an increasing cofinal sequence of smaller ordinals. Effective choices allow a fast-growing hierarchy to turn limit recursion into recursion at a finite input. Below epsilon zero, write the final term as $\gamma +{\omega }^{\beta }$. For successor $\beta =\delta +1$, take $\gamma +{\omega }^{\delta }(n+1)$; for nonzero limit $\beta$, take $\gamma +{\omega }^{\beta [n]}$. Earlier terms in the Cantor normal form remain fixed.

For every ordinal base $\rho >1$, a nonzero ordinal has a unique finite ordinal addition expansion with strictly decreasing exponents ${\beta }_i$ and coefficients $0<{\xi }_i<\rho$. Choose the largest power at most the remaining ordinal and apply the ordinal division algorithm. The next remainder has smaller leading exponent, so well-foundedness forces termination. Each lower tail is smaller than its preceding power; uniqueness of division consequently fixes the exponent, coefficient and tail successively. For $\rho =\omega$ this is Cantor normal form.

Every nonzero ordinal $\alpha$ has a greatest exponent $\beta$ such that ${\omega }^{\beta }\le \alpha$. It is the leading exponent in the Cantor normal form of $\alpha$, andfor a positive finite integer $n$ and $\gamma <{\omega }^{\beta }$.

Let nonzero ordinals $\xi ,\eta$ have leading exponents $\rho ,\sigma$. If $\eta$ is finite, then $\xi \eta$ has leading exponent $\rho$. If $\eta$ is infinite, so that $\sigma >0$, then $\xi \eta$ has leading exponent $\rho +\sigma$. This follows by multiplying the leading terms in Cantor normal form and using continuity of ordinal multiplication at limit ordinals.

Give a leaf rank zero, and use Hessenberg natural sum over the immediate rooted subtrees. Every rank is below epsilon zero; conversely repeated exponentiation and finite summation encode every Cantor normal form below it. A rooted-tree homeomorphic embedding implies nondecrease of the rank. When roots match, child subtrees embed into distinct branches and exponentiation and natural sum preserve their inequalities. When the source root maps below the host root, its rank is bounded by that of a proper subtree, strictly below the host rank.

Ordinal arithmetic defines addition, multiplication and exponentiation of ordinals through order types or transfinite recursion. The usual operations need not be commutative. Natural sum and natural product instead combine Cantor normal forms and are commutative; the Hessenberg natural sum is the natural addition operation.

Replacing every base occurrence by omega in a hereditary base representation gives a Cantor normal form below epsilon zero. Hereditary base change preserves this ordinal expression, and subtraction of one lowers it strictly. The ordinal is a termination measure even when the natural-number value increases.

For fixed $\beta$, the recursion defining $\beta +\alpha$ makes it continuous in $\alpha$ at every nonzero limit, and $(\beta +\alpha )+1>\beta +\alpha$. Thus $\alpha \mapsto \beta +\alpha$ is normal, including when $\beta =0$.

For $\beta >0$, take $\lambda =\beta \cdot \omega$. If $\alpha <\lambda$, choose a natural number $n$ with $\alpha <\beta n$; then $\alpha +\beta \le \beta (n+1)<\lambda$. Since $\alpha +\beta \ge \alpha$, their supremum as $\alpha \uparrow \lambda$ is $\lambda$. But $\lambda +\beta >\lambda$, soHence right addition by a nonzero fixed ordinal fails continuity and is not normal.

Normality and argument order in ordinal arithmetic also give the multiplication statements: $\alpha \mapsto \beta \cdot \alpha$ is normal for $\beta >0$, while $\alpha \mapsto \alpha \cdot \beta$ is normal exactly when $\beta =1$. At $\beta =0$ it is constant. For fixed $\beta >1$, let $\kappa ={\omega }^{\beta \cdot \omega }$. Cantor normal form shows that $\xi \beta <\kappa$ whenever $\xi <\kappa$: leading exponents below $\beta \omega$ remain below it after adding the leading exponent of $\beta$. Thus ${\sup }_{\xi <\kappa }\xi \beta =\kappa$, but $\kappa \beta >\kappa$, again violating continuity. Left-fixed multiplication is strictly increasing and continuous by its recursion.

For exponentiation, $\alpha \mapsto {\beta }^{\alpha }$ is normal for $\beta \ge 2$; bases zero and one are exceptions. The reverse map $\alpha \mapsto {\alpha }^{\beta }$ is normal exactly when $\beta =1$. Exponent zero gives the constant one. For $\beta >1$, use the same $\kappa$ and put $\lambda ={\omega }^{\kappa }$. For each $\alpha <\lambda$ choose $0<\zeta <\kappa$ with $\alpha \le {\omega }^{\zeta }$. Then ${\alpha }^{\beta }\le {\omega }^{\zeta \beta }<\lambda$, while ${\alpha }^{\beta }\ge \alpha$ for positive $\alpha$. Consequently its left supremum is $\lambda$, but ${\lambda }^{\beta }={\omega }^{\kappa \beta }>\lambda$. The bound by ${\omega }^{\zeta }$ also handles finite bases, where an unqualified leading-exponent multiplication formula would need care. All these are ordinal facts and use no choice.

Use transfinite induction on nonzero $\alpha$. Part (b) gives $\alpha ={\omega }^{\delta }n+\zeta$, with $n$ a positive natural number and $\zeta <{\omega }^{\delta }\le \alpha$.

If $\zeta =0$, this is already a one-term Cantor normal form. Otherwise $0<\zeta <\alpha$, so the induction hypothesis supplies a finite Cantor normal form for $\zeta$. Its leading exponent $\eta$ satisfies ${\omega }^{\eta }\le \zeta <{\omega }^{\delta }$, hence $\eta <\delta$. All later exponents are smaller still. Prefixing ${\omega }^{\delta }n$ therefore givesThe number of terms is finite because the inductive representation of the strictly smaller remainder is finite. Equivalently, repeated extraction cannot produce an infinite strictly descending sequence of ordinals. Since $\alpha \ne 0$, the number of terms is positive.

Yes, with the stated strict decrease and positive coefficients. In any displayed Cantor normal form, the first exponent is the unique $\delta$ with ${\omega }^{\delta }\le \alpha <{\omega }^{\delta +1}$. The leading coefficient is the unique positive integer $n$ withThe remaining tail is the unique $\zeta <{\omega }^{\delta }$ satisfying $\alpha ={\omega }^{\delta }n+\zeta$, by strict monotonicity of ordinal addition in the right operand.

Thus any two such representations have the same first exponent and coefficient and the same remainder. Repeat the argument on that remainder. Their finite lists agree term by term and reach zero at the same step, so the lengths agree as well. Allowing zero coefficients or repeated exponents would spoil this normalized uniqueness, which is why those conditions are required.

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.

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.

For Fodor's theorem, let $\kappa$ be regular uncountable, $S\subseteq \kappa$ stationary, and $f:S\to \kappa$ regressive: $f(\alpha )<\alpha$ for every nonzero $\alpha \in S$. A club set is unbounded in $\kappa$ and closed under limits below $\kappa$; a stationary set meets every club. Removing $0$ preserves stationarity. We prove that some fibre of $f$ is stationary, not merely that one fibre is large.

We first check the club facts used in the argument. An intersection of fewer than $\kappa$ club subsets of $\kappa$ is club. Closure is immediate. For unboundedness, given $\gamma$ and clubs $(C_i{)}_{i<\mu }$ with $\mu <\kappa$, choose an increasing sequence ${\gamma }_n$ starting above $\gamma$, such that ${\gamma }_{n+1}$ is above a point of every $C_i$ beyond ${\gamma }_n$. Regularity bounds the supremum of the fewer-than-$\kappa$ points at each step. Then $\delta ={\sup }_{n<\omega }{\gamma }_n<\kappa$, and the chosen points in each $C_i$ are cofinal in $\delta$; closure puts $\delta$ in their intersection.

For a sequence $(C_{\xi }{)}_{\xi <\kappa }$ of clubs its diagonal intersectionis also club. To obtain a point above $\gamma$, recursively choose ${\gamma }_{n+1}>{\gamma }_n$ in ${\bigcap }_{\xi \le {\gamma }_n}{C}_{\xi }$, possible by the preceding result, and take the supremum $\delta$ of the sequence. For each $\xi <\delta$, every sufficiently late ${\gamma }_n$ belongs to $C_{\xi }$, so $\delta \in C_{\xi }$. For closure, if diagonal-intersection points are cofinal in $\delta <\kappa$, then for each $\xi <\delta$ their sufficiently late points lie in $C_{\xi }$, and closure again puts $\delta$ there.

Suppose every fibre $S_{\xi }=\{\alpha \in S:f(\alpha )=\xi \}$ were nonstationary. Choose a club $C_{\xi }$ disjoint from each fibre. Stationarity supplies $\alpha \in S\cap {\Delta }_{\xi <\kappa }{C}_{\xi }$, with $\alpha >0$. Put $\xi =f(\alpha )<\alpha$. By diagonal membership $\alpha \in C_{\xi }$, but by its definition $\alpha \in S_{\xi }$, a contradiction. ThusThis is precisely the pressing-down assertion. Regularity and uncountability were used to keep the club-building suprema below $\kappa$.

For the Cantor normal form theorem, every nonzero ordinal has a unique expressionAll operations are ordinal operations, so the order of the terms matters. The ordinal zero has the empty expression. We give the greedy existence proof and then prove uniqueness.

The powers ${\omega }^{\beta }$ are strictly increasing and continuous at limit exponents, and satisfy ${\omega }^{\beta }\ge \beta$. Hence the set of exponents with ${\omega }^{\beta }\le \alpha$ is nonempty and bounded, and its supremum ${\beta }_0$ belongs to it by continuity (or is already its last successor member). Thus there is a largest such exponent andSince the last product is the supremum of the finite multiples, there is a unique positive finite $n_0$ satisfyingThe initial segment of $\alpha$ of length ${\omega }^{{\beta }_0}{n}_0$ leaves a tail of unique order type $\rho$, soThe bound follows from strict increase of ordinal addition in its right argument: a tail at least ${\omega }^{{\beta }_0}$ would contradict the preceding interval. This is the relevant instance of the ordinal division algorithm.

If $\rho >0$, apply the same construction to it. Its leading exponent must be below ${\beta }_0$. Continue with the remainder. An infinite continuation would produce an infinite strictly descending sequence of ordinals, impossible by well-foundedness. Thus the process terminates after finitely many steps and gives the required form.

To prove uniqueness, first observe that a finite decreasing-exponent suffix with leading exponent $\gamma$ is smaller than ${\omega }^{\gamma +1}$. This follows by induction on its number of terms: the later tail is below ${\omega }^{\gamma }$, so adding it to a finite multiple of ${\omega }^{\gamma }$ stays below the next finite multiple and hence below ${\omega }^{\gamma }\cdot \omega$. Consequently the tail after a term with exponent $\beta$ is below ${\omega }^{\beta }$.

Any proposed normal form therefore places $\alpha$ in exactly the intervalIts first exponent is recoverable as the largest exponent whose power does not exceed $\alpha$, and its first coefficient is recoverable as the largest finite multiple not exceeding $\alpha$. The right remainder is unique because ordinal addition is strictly increasing in its right argument. Apply the same reasoning to the remainder, successively fixing every exponent and coefficient. This proves uniqueness without treating ordinal addition as commutative or cancelling arbitrary left summands.

Fix an ordinal $\rho >1$. The Generalized Cantor normal form asserts that every nonzero ordinal $\alpha$ has a unique expressionProducts, sums and powers here are ordinal multiplication, ordinal addition and ordinal exponentiation; the coefficients need not be finite if $\rho$ is infinite. The case $\rho =\omega$ is Cantor normal form, and a finite base on finite ordinals gives ordinary positional notation. Zero has the empty expansion.

We first prove the ordinal division algorithm. For $\delta >0$, the function $q\mapsto \delta q$ is strictly increasing, continuous at limit ordinals and unbounded. Hence there is a greatest $q$ with $\delta q\le \alpha$: the first $q^{\prime }$ with $\delta q^{\prime }>\alpha$ cannot be a limit by continuity and must equal $q+1$. The interval after the initial segment $\delta q$ has a unique order type $r$, so $\alpha =\delta q+r$. Maximality of $q$ gives $r<\delta$. These facts also prove uniqueness of $q,r$.

Similarly $\beta \mapsto {\rho }^{\beta }$ is strictly increasing, continuous at limits and unbounded, so there is a unique largest ${\beta }_0$ with ${\rho }^{{\beta }_0}\le \alpha$. Divide by ${\rho }^{{\beta }_0}$ to obtainThe quotient is positive, and $\alpha <{\rho }^{{\beta }_0+1}={\rho }^{{\beta }_0}\rho$ makes ${\xi }_0<\rho$. If $r_0>0$, repeat on $r_0$; its leading exponent is strictly smaller than ${\beta }_0$. This process terminates, since an infinite run would give an infinite descending sequence of ordinals. It constructs the required form.

For uniqueness, a finite expression with largest exponent $\beta$ and coefficients below $\rho$ has value below ${\rho }^{\beta +1}$. Prove this from the end backwards: a tail with largest exponent $\gamma <\beta$ is below ${\rho }^{\gamma +1}\le {\rho }^{\beta }$, andThus the displayed leading exponent is the uniquely determined largest $\beta$ with ${\rho }^{\beta }\le \alpha$. The ordinal division algorithm uniquely determines its coefficient and the remaining tail, and recursion proves uniqueness of the whole expression. No commutative rearrangement of ordinal sums is used.

The recursive ordinal addition definitions are $a+0=a$, $a+(b+1)=(a+b)+1$, and $a+\lambda ={\sup }_{b<\lambda }(a+b)$ for a nonzero limit ordinal. Ordinal multiplication is $a\cdot 0=0$, $a\cdot (b+1)=a\cdot b+a$, and $a\cdot \lambda ={\sup }_{b<\lambda }a\cdot b$. For $a>0$, ordinal exponentiation is $a^0=1$, $a^{b+1}=a^b\cdot a$, and $a^{\lambda }={\sup }_{b<\lambda }{a}^b$; the exceptional zero base has $0^0=1$ and $0^b=0$ for $b>0$.

Transfinite induction gives ${\omega }^a\ge a$. At zero this is immediate; at a successor, ${\omega }^{b+1}={\omega }^b\omega \ge {\omega }^b+1\ge b+1$. At a limit, continuity and the induction hypothesis give ${\sup }_{b<a}{\omega }^b\ge {\sup }_{b<a}b=a$. Also $a\mapsto {\omega }^a$ is strictly increasing: its successor values strictly increase, and continuity preserves the strict inequality between any two distinct indices.

For $\alpha >0$, ${\omega }^{\alpha +1}>{\omega }^{\alpha }\ge \alpha$, so there is a least $\delta$ with ${\omega }^{\delta }>\alpha$. It cannot be zero and cannot be a limit: at a limit, a supremum greater than $\alpha$ has a term already greater than $\alpha$, contradicting minimality. Thus $\delta ={\alpha }_0+1$, andStrict increase proves uniqueness, and ${\alpha }_0\le {\omega }^{{\alpha }_0}\le \alpha$ proves the requested index bound.

Choose the largest positive integer $a_0$ with ${\omega }^{{\alpha }_0}{a}_0\le \alpha$. It exists because $\alpha <{\omega }^{{\alpha }_0}\omega ={\sup }_{m<\omega }{\omega }^{{\alpha }_0}m$. The remaining tail of the ordinal interval has an order type $\rho$ with $\alpha ={\omega }^{{\alpha }_0}{a}_0+\rho$; maximality implies $\rho <{\omega }^{{\alpha }_0}$. If $\rho >0$, repeat the construction on it. The leading exponents strictly decrease, and there is no infinite strictly decreasing sequence of ordinals: its set of values would have a least member followed by a smaller one. Hence the process terminates, yielding the Cantor normal formThe first exponent is determined by the preceding band, the first coefficient by maximality, and the tail by the ordinal interval left after that initial segment. Recursion therefore proves uniqueness of every exponent and coefficient. The PDF's second coefficient is printed ${\alpha }_1$ rather than $a_1$; the stated natural-number coefficients and the construction identify the intended expression.

For the final assertion, powers of $\omega$ are additively indecomposable: if $\tau <{\omega }^{\eta }$, then $\tau +{\omega }^{\eta }={\omega }^{\eta }$ for $\eta >0$. One proves this by induction on $\eta$. At a successor, bound $\tau$ by a finite multiple of ${\omega }^{\eta -1}$ and use the supremum over all such multiples; at a limit, bound $\tau$ by a smaller power and use continuity. For $\eta =0$ the only possible $\tau$ is zero. Thus a smaller leading exponent is absorbed when a larger-leading ordinal is added on its right. If $\beta ,\gamma$ have unequal leading exponents, either $\beta +\gamma =\gamma$ or $\gamma +\beta =\beta$. If their leading exponents coincide, the leading coefficient of either sum is the sum of their two positive leading coefficients; it exceeds each coefficient, so neither absorption equality holds. Zero is never commensurable with an ordinal. Consequently commensurability is exactly equality of the leading exponent, equivalently membership of both positive ordinals in one of the stated bands.

For $b\ge 2$, write a number in hereditary base $b$: express its base-$b$ expansion as ${\sum }_i{b}^{e_i}{c}_i$, with $0<c_i<b$, and recursively expand every exponent $e_i$ in the same base. Let $B_{b,c}(m)$, for $c>b$, be the number obtained by replacing every occurrence of the base $b$ in this hereditary expression by $c$. Coefficients and the symbols for addition and exponentiation are retained.

For a starting number $m$, define its Goodstein sequence by $m_0=m$ andThe Goodstein function is the termination-time functionThis choice counts transitions from the initial term; a convention counting the initial term as well shifts the answer by one. For example the sequence starting at $3$ is $3,3,3,2,1,0$, so $\mathcal{G}(3)=5$. Starting at $4$ gives $4,26,41,60,83,\dots$, illustrating why descent of the numerical terms is not the termination argument.

Define the ordinal rank of a Goodstein term ${\rho }_b(m)$ by replacing the base $b$ in the hereditary expansion by $\omega$, at every exponent depth. The result is in Cantor normal form and lies below ${ϵ}_0$, called epsilon zero, the least nonzero solution of ${\omega }^{\alpha }=\alpha$. Finite hereditary expressions have finite nesting depth, so their ranks are bounded by a sufficiently high finite tower of powers of $\omega$.

For a fixed base, ${\rho }_b$ is strictly increasing. To see this, compare two ordinary base-$b$ expansions at their largest differing exponent. By induction through the hereditary exponent expressions, their exponents have the same ordering after replacing $b$ by $\omega$; computable Cantor normal form notation then uses the same first differing exponent or coefficient. AlsoIndeed after the base change all coefficients remain below $c$, the recursively changed exponents remain correctly ordered, and replacing the new base by $\omega$ gives exactly the original ordinal expression. These facts can be proved together by structural induction for primitive recursive functions on the hereditary expression.

Consequently, whenever $m_s>0$,An infinite nonzero Goodstein sequence would give an infinite descending sequence of ordinals below ${ϵ}_0$, impossible because ordinals are well-ordered. Thus the Goodstein function is total. Its steps are effective finite operations, so simulating the sequence until zero also proves that it is a total computable function.

The same ordinal notation system gives the requested decidable well-order. Let $D$ consist of canonical finite terms for zero and for expressionswhere the exponents are themselves canonical terms. Membership in $D$ is decidable by recursively checking the syntax, positive coefficients and decreasing exponents. Comparison is decidable by recursive computable Cantor normal form notation, first of exponents, then coefficients, and then the remaining summands. All recursive calls inspect proper subterms, so the algorithm terminates.

Interpreting these terms as ordinals gives every ordinal below ${ϵ}_0$, uniquely. One way to connect this directly to hereditary base representations is to choose, for a given finite ordinal term, a base larger than every coefficient anywhere in that term. Replacing $\omega$ by that base evaluates it to a natural number whose hereditary representation recovers the ordinal term. Thus all bases together supply the complete notation system; a single fixed base is not enough.

Choose an effective injective coding of finite terms by natural numbers, and enumerate the valid codes in increasing numerical order. The resulting bijection $d:\mathbb{N}\to D$ is computable: validity is decidable and there are infinitely many finite-ordinal terms. Its inverse is computable by counting valid codes below a given code. DefineThis is a decidable relation on all of $\mathbb{N}$. The interpretation into ordinals is an order isomorphism onto ${ϵ}_0$, provingDecidability here concerns comparing two notations. Well-foundedness is supplied by their ordinal interpretation, the same mathematical descent principle used to prove Goodstein's theorem.