Weak and Strong Versions of Effective Transfinite Recursion

TL;DR

This paper characterizes the strength of two definitions of Effective Transfinite Recursion in reverse mathematics and establishes an equivalence between $ ext{Pi}^0_2$-induction along a well-order and the well-foundedness of exponentiated well-orders.

Contribution

It provides a detailed comparison of two definitions of Effective Transfinite Recursion and links $ ext{Pi}^0_2$-induction to well-foundedness of exponentiated well-orders.

Findings

Characterization of the strength of two Effective Transfinite Recursion definitions.

Equivalence between $ ext{Pi}^0_2$-induction along a well-order and well-foundedness of exponentiated well-orders.

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 $\Pi^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.