Computable Cantor normal form notation

Finite canonical terms built from zero, ordinal sums and powers of omega describe exactly the ordinals below epsilon zero. Syntactic validity and comparison are decidable by recursion through the exponent subterms. Enumerating valid term codes transfers their order to a computable well-order on all natural numbers.

Use the unary Cantor normal form tree norm, counting one root and recursively counting all repeated exponent subterms. There are only finitely many notations of bounded norm. This finite principle bounds all descending sequences whose norms grow at most linearly with the position. Friedman's finite form of Kruskal's theorem implies it through the natural-sum ordinal rank of a finite rooted tree. The Friedman–Smith miniaturization theorem turns this controlled termination principle for standard epsilon-zero notations into the formal consistency statement for Peano arithmetic; the technical ordinal-analysis result is needed in addition to the tree coding. Section 2.2 of formal.hknu.ac.kr/Publi/kruskalJKMS.pdf records the general miniaturization and soundness theorem.