The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule
From MaRDI portal
Publication:1577487
DOI10.1016/S0168-0072(00)00016-6zbMath0964.03061MaRDI QIDQ1577487
Publication date: 16 July 2001
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
transfinite inductionsecond-order arithmeticfixed-point theoryproof-theoretical ordinalpredicative analysisbar rulefirst-order applicative theory \(\text{AutBON}(\mu)\)ramified analysissystems with infinitary rules
Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35) Relative consistency and interpretations (03F25)
Related Items (5)
Theories with self-application and computational complexity. ⋮ UNFOLDING FINITIST ARITHMETIC ⋮ Unfolding Schematic Systems ⋮ The unfolding of non-finitist arithmetic ⋮ Universes over Frege structures
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Constructivism in mathematics. An introduction. Volume I
- Fixed points in Peano arithmetic with ordinals
- The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
- The unfolding of non-finitist arithmetic
- A theory of rules for enumerated classes of functions
- Totality in applicative theories
- Second order theories with ordinals and elementary comprehension
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
- Systems of explicit mathematics with non-constructive \(\mu\)-operator and join
- Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis
- Systems of predicative analysis
- Some theories with positive induction of ordinal strength φω0
This page was built for publication: The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule
