Systems of explicit mathematics with non-constructive \(\mu\)-operator. II (Q1919537): Difference between revisions

[For Part I see ibid. 65, No. 3, 243-263 (1993; Zbl 0794.03074).] The paper is concerned with proof-theoretic analysis of second-order (sub)systems of explicit mathematics introduced mainly by the first author. They contain three forms of induction: S-I\(_N\) (for sets), T-I\(_N\) (for types), F-I\(_N\) (for all formulas), as well as the non-constructive minimum operator \(\mu\). EET means elementary explicit type theory. Main results are: \[ \begin{aligned}\text{EET}(\mu)+ (\text{S-I}_N) &\equiv\text{PA}\equiv\text{EET}+ (\text{T-I}_N);\;\text{EET}+ (\text{F-I}_N)\equiv (\Pi^\infty_0- \text{CA});\\ \text{EET}(\mu)+ (\text{T-I}_N) &\equiv (\Pi^0_\infty- \text{CA})_{<\varepsilon_0};\;\text{EET}(\mu)+ (\text{F-I}_N)\equiv (\Pi^0_\infty-\text{CA})_{<\varepsilon_{\varepsilon_0}}.\end{aligned} \] Most of these results are established by a (relatively) simple model-theoretic lemma providing conservative extension results with respect to corresponding extensions of the first-order theory BON treated in Part I. The lower bound for the strongest of the considered theories follows from a translation of the system \((\Pi^0_\infty-\text{CA})_{<\varepsilon_{\varepsilon_0}}\) into \(\text{EET}(\mu)+ (\text{F-I}_N)\), where second-order quantifiers range over \(P(N)\). Upper bound is obtained by translation of a theory \(\widehat{\text{E}\Omega}\) of second-order arithmetic plus ordinals, which was proved to be proof-theoretically equivalent to \((\Pi^0_\infty-\text{CA})_{<\varepsilon_{\varepsilon_0}}\) [the second author and \textit{T. Strahm}, ``Second-order theories with ordinals and elementary comprehension'', Arch. Math. Logic 34, No. 6, 345-375 (1995; Zbl 0846.03028)].