Systems of explicit mathematics with non-constructive \(\mu\)-operator. I (Q1314542)

Complete proof-theoretic analysis of two systems of explicit mathematics introduced by the first author is given. System \(\text{BON}(\mu)\) [basic theory of operators and numbers with a non-constructive minimum operator] with set induction on natural numbers is proof-theoretically equivalent to Peano arithmetic PA. Adding the induction schema for arbitrary formulas leads to a system equivalent to the fixed point theory \(\widehat{\text{ID}}_ 1\) of the first author [Patras Logic Symp., Proc., Patras 1980, Stud. Logic Found. Math. 109, 171-196 (1982; Zbl 0522.03045)]. The latter was proved by P. Aczel to be proof-theoretically equivalent to \((\Pi^ 0_ \infty-\text{CA})_{<\varepsilon_ 0}\). PA is translated here into \(\text{BON}(\mu)+\) set-induction by applying the unbounded minimum operator \(\mu\) in order to eliminate the number quantifiers. To translate \((\Pi^ 0_ \infty- \text{CA})_{<\varepsilon_ 0}\) the autors use the known derivation of transfinite induction up to every ordinal \(\alpha<\varepsilon_ 0\) from induction on natural numbers, and hence \(\text{BON}(\mu)+\) formula induction. Translations in the opposite direction use the theories of ordinals introduced by the second author [Ann. Pure Appl. Logic 60, No. 2, 119-132 (1993; Zbl 0776.03027)] and containing the standard apparatus for defining sets inductively by ordinal stages. The system \(\text{PA}^ r_ \Omega\) contains induction on natural numbers for the formulas, where all ordinals are bounded. This allows to translate partial recursive computations over \(\mu\), and hence \(\text{BON}(\mu)+\) set- induction. The system \(\text{PA}^ w_ \Omega\) contains induction over formula of the language, and hence translates formula-induction. The proof is concluded by the reference to the equivalences: \(\text{PA}^ r_ \Omega\equiv\text{PA}\); \(\text{PA}^ w_ \Omega\equiv\widehat{\text{ID}}_ 1\).