Fixed point theories and dependent choice (Q1590660)

ATR is Friedman's famous system of second-order arithmetic for arithmetical transfinite recursion; \(\text{ATR}_0\) is ATR with induction on the natural numbers restricted to sets of natural numbers; \((\Sigma^1_1\text{-DC})\) is the usual schema of dependent choice for \(\Sigma^1_1\) formulas. With \(\widehat{\text{ID}}_\alpha\) we denote the first-order system for \(\alpha\) times iterated fixed points generated by positive arithmetic operator forms; \(\widehat{\text{ID}}_{<\beta}\) denotes the union of the theories \(\widehat{\text{ID}}_\alpha\) for \(\alpha<\beta\). In this paper we establish the proof-theoretic equivalence of (i) ATR and \(\widehat{\text{ID}}_\omega\), (ii) \(\text{ATR}_0 + (\Sigma^1_1\text{-DC})\) and \(\widehat{\text{ID}}_{<\omega^\omega}\), and (iii) \(\text{ATR} +(\Sigma^1_1\text{-DC})\) and \(\widehat{\text{ID}}_{<\varepsilon_0}\).