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 (20)

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

This page was built for publication: Systems of explicit mathematics with non-constructive \(\mu\)-operator. I