About the proof-theoretic ordinals of weak fixed point theories (Q4032884)

The theory \(\text{FP}\)-\(\text{ACA}_ 0\) in the language of second-order arithmetic contains the arithmetic comprehension axiom, the induction axiom, a new relational symbol \(P_ A\) (fixed-point constant) for every arithmetic formula \(A[X,x]\) positive in \(X\), and the fixed-point axioms \(\forall x(A[P_ A,x]\leftrightarrow P_ A(x))\). There is no uniqueness axiom for \(P_ A\) stating that it is the minimal fixed point. The extension \(\text{FP}\)-\(\text{ACA}\) of \(\text{FP}\)-\(\text{ACA}_ 0\) contains the induction scheme for all formulas of its language. Using embedding into ramified analysis and cut-elimination, the authors establish proof-theoretic ordinals: \(|\text{FP}\)-\(\text{ACA}_ 0|=\varepsilon_ 0\), \(|\text{FP}\)-\(\text{ACA}|=\varphi 1\varepsilon_ 0\). Here \(| T|\) is the supremum of ordinals of primitive recursive well-orderings \(\prec\) such that well-foundedness of \(\prec\) is provable in \(T\). On the other hand, \(\text{FP}\)-\(\text{ACA}_ 0\) is proof-theoretically equivalent to the system \((\Sigma^ 1_ 1\)- \(\text{AC})\), although \(|\Sigma^ 1_ 1\)- \(\text{AC}|=\varphi\varepsilon_ 0 0\). The reason: the reduction of \(\Sigma^ 1_ 1\)-\(\text{AC}\) to \(\text{FP}\)-\(\text{ACA}_ 0\) through an intermediate system \(\widehat{\text{ID}}_ 1\) considered by Feferman) uses a coding of sets by natural numbers satisfying a unary relation \(S\). If \((\Sigma^ 1_ 1\)-\(\text{AC})\lvdash\text{WF}(\prec)\), then transfinite induction on \(\prec\) is provable in \(\text{FP}\)- \(\text{ACA}_ 0\) for all sets \(Z\) coded by \(S\), but not necessarily for all sets.