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

DOI10.1016/0168-0072(93)90013-4zbMath0794.03074OpenAlexW2137355506MaRDI QIDQ1314542

Solomon Feferman, Gerhard Jäger

Publication date: 28 August 1994

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(93)90013-4

zbMATH Keywords

inductionPeano arithmeticbasic theory of operators and numbersordinal stagesproof-theoretic analysis of systems of explicit mathematics

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

Formalizing non-termination of recursive programs, Totality in applicative theories, Systems of explicit mathematics with non-constructive \(\mu\)-operator. II, The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories, Some theories with positive induction of ordinal strength φω0, Theories with self-application and computational complexity., Polynomial time operations in explicit mathematics, On Feferman's operational set theory \textsf{OST}, The Operational Perspective: Three Routes, Explicit mathematics: power types and overloading, TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES, The Operational Penumbra: Some Ontological Aspects, Predicativity and Feferman, THE UNIVERSAL SET AND DIAGONALIZATION IN FREGE STRUCTURES, Full operational set theory with unbounded existential quantification and power set, The unfolding of non-finitist arithmetic, The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule, Systems of explicit mathematics with non-constructive \(\mu\)-operator and join, A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\), Universes over Frege structures

Cites Work

• Proof theory. 2nd ed
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Constructivism in mathematics. An introduction. Volume I
• Fixed points in Peano arithmetic with ordinals
• Hilbert's program relativized; Proof-theoretical and foundational reductions
• A well-ordering proof for Feferman's theoryT 0
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item