The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule (Q1577487)

The author considers a first-order applicative theory \(\text{AutBON}(\mu)\), and shows that it is proof-theoretically equivalent to predicative analysis, hence its proof-theoretical ordinal is Schütte-Feferman's \(\Gamma_0\). Here, BON stands for the basic theory of operations and numbers (Feferman et al.), and \(\mu\) is the unbounded (hence non-constructive) minimum operator. Further, this theory has the inductiion scheme, and the bar rule: infer \(\text{TI}(\prec,A)\) from \(\text{TI}(\prec, U)\), where \(U\) is a unary predicate variable, \(A\) is any formula, \(\prec\) is a recursive binary relation, and TI expresses transfinite induction. The method of proof is standard: \(\Aut(\Pi^1_0)\) is interpreted in the theory in question to give the lower bound, and the theory is, in turn, interpreted in \(\text{PA}^w_\Omega+ (\text{Subst})\) for the upper bound. Here, \(\Aut(\Pi^1_0)\) is second-order arithmetic with autonomously iterated \(\Pi^1_0\) jumps, and \(\text{PA}^w_\Omega\) is the fixed-point theory (so, with inductive operator axioms) over PA with ordinals \(\Omega\), and \(\Delta_0\)-inductions \(w\). To determine the strength of the last theory, the author uses systems with infinitary rules, cut-elimination, asymmetric interpretation, and so forth. In the form of an appendix, the author gives similar consideration to the theory whose underlying applicative system is recursive, and shows that it is equivalent to ramified analysis in all finite levels and hence its ordinal is \(\varphi 20\) in the Veblen hierarchy.