Weak and Strong Versions of Effective Transfinite Recursion
Patrick Uftring
TL;DR
This paper analyzes the exact strength of Weak and Strong Effective Transfinite Recursion principles within reverse mathematics. It proves that for a fixed well-order $X$, Strong Effective Transfinite Recursion along $X$ is equivalent to transfinite $Π^0_2$-induction along $X$ and to the preservation of well-orders by the exponentiation map $α o α^X$, and that Strong SETR is equivalent to $ACA_0$; for a general SETR, $SETR_X$ is equivalent to $Π^0_2$-induction along $X$ as well. For Weak Effective Transfinite Recursion, the paper shows $WETR_X$ is equivalent to the disjunction of $WKL$ and $SETR_X$, with a rule version of $WETR$ admissible over $RCA_0$, and analyzes the ω-case where $WETR_ω$ corresponds to $WKL \, ext{or}\, Π^0_2$-induction along $ℕ$ (not provable in $RCA_0$). The results sharpen the ATR-related landscape by linking order-theoretic constructions to standard subsystems and clarifying the role of exponentiation of well-orders in reverse mathematics.
Abstract
Working in the context of reverse mathematics, we give a fine-grained characterization result on the strength of two possible definitions for Effective Transfinite Recursion used in literature. Moreover, we show that $Π^0_2$-induction along a well-order $X$ is equivalent to the statement that the exponentiation of any well-order to the power of $X$ is well-founded.