Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
type: Item
instance of: scholarly article
title: Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
zbMATH Open document ID: 0868.03026
DOI: 10.1016/0168-0072(95)00028-3
author: Solomon Feferman
author: Gerhard Jäger
published in: Annals of Pure and Applied Logic
publication date: 1997-08-19T00:00:00Z
review text: [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)].
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 908466
zbMATH Keywords: proof-theoretic analysis
zbMATH Keywords: explicit mathematics
zbMATH Keywords: conservative extension
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: 0168-0072(95)00028-3
OpenAlex ID: W4213356241
cites work: Q3679172
cites work: Q5622162
cites work: Q4128540
cites work: Q3882452
cites work: Q4723729
cites work: Hilbert's program relativized; Proof-theoretical and foundational reductions
cites work: Q4010354
cites work: Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
cites work: Q5619071
cites work: Q3035279
cites work: Totality in applicative theories
cites work: Second order theories with ordinals and elementary comprehension
cites work: Q4143279
cites work: Constructivism in mathematics. An introduction. Volume II
Recommended article: Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
Recommended article: Second order theories with ordinals and elementary comprehension
Recommended article: Q3081650
Recommended article: Universes in metapredicative analysis
Recommended article: Q4040375
Recommended article: Ein Wohlordnungsbeweis mit $$ \Delta^{1}_{2} $$-Komprehension und Bar-Induktion
Recommended article: Bounded arithmetic and truth definition
Recommended article: The strength of some Martin-Löf type theories
Recommended article: Universes in explicit mathematics
Recommended article: Classical predicative logic-enriched type theories
description: scientific article; zbMATH DE number 908466