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)