On the relationship between ATR0 and
Jeremy D. Avigad · Journal of Symbolic Logic · 1996
Abstract We show that the theory ATR0 is equivalent to a second-order generalization of the theory . As a result, ATR0 is conservative over for arithmetic sentences, though proofs in ATR0 can be much shorter than their counterparts.