On the proof-theoretic strength of monotone induction in explicit mathematics

We characterize the proof-theoretic strength of systems of explicit mathematics with a general principle (MID) asserting the existence of least fixed points for monotone inductive definitions, in terms of certain systems of analysis and set theory. In the case of analysis, these are systems which co...

Full description

Saved in:
Bibliographic Details
Published in:Annals of pure and applied logic 1997-04, Vol.85 (1), p.1-46
Main Authors: Glaß, Thomas, Rathjen, Michael, Schlüter, Andreas
Format: Article
Language:English
Subjects:
Admissible sets
Asymmetric interpretation
Explicit mathematics
Monotone induction
Proof theory
Stability
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We characterize the proof-theoretic strength of systems of explicit mathematics with a general principle (MID) asserting the existence of least fixed points for monotone inductive definitions, in terms of certain systems of analysis and set theory. In the case of analysis, these are systems which contain the Σ 1 2-axiom of choice and Π 1 2-comprehension for formulas without set parameters. In the case of set theory, these are systems containing the Kripke-Platek axioms for a recursively inaccessible universe together with the existence of a stable ordinal. In all cases, the exact strength depends on what forms of induction are admitted in the respective systems.
ISSN:0168-0072
DOI:10.1016/S0168-0072(96)00040-1