= Slow well-ordering below epsilon zero
{title2=$\forall k\ \exists N\ \forall(\alpha_i)_{i<N}\ (\|\alpha_i\|\le k+i\Rightarrow\exists i<j\ \alpha_i\le\alpha_j)$}
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 https://formal.hknu.ac.kr/Publi/kruskalJKMS.pdf records the general miniaturization and soundness theorem.
Back to article page
