Reverse mathematics of prime factorization of ordinals (Q1127837)

One of the earliest applications of Cantor's Normal Form Theorem is Jacobstahl's proof of the existence of prime factorizations of ordinals. An ordinal \(\alpha\) is prime if whenever \(\alpha = \lambda \rho\), either \(\rho = 1\) or \(\rho = \alpha\). Applying the techniques of reverse mathematics, we show that the full strength of the Normal Form Theorem is used in proving the existence of prime factorizations of well orderings. In particular, working in the system \(ACA_0\), the prime factorization theorem is provably equivalent to \(ATR_0\), which is known to be equivalent to the Normal Form Theorem.