id: 01501510 dt: j an: 01501510 au: Strahm, Thomas ti: The non-constructive $μ$ operator, fixed point theories with ordinals, and the bar rule. so: Ann. Pure Appl. Logic 104, No.1-3, 305-324 (2000). py: 2000 pu: Elsevier Science B.V. (North-Holland), Amsterdam la: EN cc: ut: first-order applicative theory $\text{AutBON}(μ)$; predicative analysis; proof-theoretical ordinal; bar rule; transfinite induction; second-order arithmetic; fixed-point theory; systems with infinitary rules; ramified analysis ci: li: doi:10.1016/S0168-0072(00)00016-6 ab: The author considers a first-order applicative theory $\text{AutBON}(μ)$, and shows that it is proof-theoretically equivalent to predicative analysis, hence its proof-theoretical ordinal is Schütte-Feferman’s $Γ_0$. Here, BON stands for the basic theory of operations and numbers (Feferman et al.), and $μ$ 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(Π^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_Ω+ (\text{Subst})$ for the upper bound. Here, $\Aut(Π^1_0)$ is second-order arithmetic with autonomously iterated $Π^1_0$ jumps, and $\text{PA}^w_Ω$ is the fixed-point theory (so, with inductive operator axioms) over PA with ordinals $Ω$, and $Δ_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 $φ20$ in the Veblen hierarchy. rv: M.Yasuhara (Princeton)