Weak and Strong Versions of Effective Transfinite Recursion

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 ${\hat{I}}_2^0$-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.