A well-ordering proof for Feferman's theoryT 0
From MaRDI portal
Publication:4749835
DOI10.1007/BF02023014zbMath0511.03025MaRDI QIDQ4749835
Publication date: 1983
Published in: Archiv für Mathematische Logik und Grundlagenforschung (Search for Journal in Brave)
Full work available at URL: https://eudml.org/doc/138008
Other constructive mathematics (03F65) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15)
Related Items (28)
The strength of admissibility without foundation ⋮ The strength of some Martin-Löf type theories ⋮ On the proof-theoretic strength of monotone induction in explicit mathematics ⋮ Ordinal notations based on a hierarchy of inaccessible cardinals ⋮ RELATIVIZING OPERATIONAL SET THEORY ⋮ Natural well-orderings ⋮ Realization of analysis into Explicit Mathematics ⋮ Recent Advances in Ordinal Analysis: Π12— CA and Related Systems ⋮ Theories with self-application and computational complexity. ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ The Operational Perspective: Three Routes ⋮ From Subsystems of Analysis to Subsystems of Set Theory ⋮ Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms ⋮ 1999 European Summer Meeting of the Association for Symbolic Logic ⋮ A theory of rules for enumerated classes of functions ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator and join ⋮ Reflections on reflections in explicit mathematics ⋮ Replacement versus collection and related topics in constructive Zermelo-Fraenkel set theory ⋮ Well-ordering proofs for Martin-Löf type theory ⋮ Having a Look Again at Some Theories ofProof-Theoretic Strengths around $$ \varGamma_{0} $$ ⋮ Cut-Elimination for SBL ⋮ An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator. I ⋮ Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe ⋮ A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
Cites Work
This page was built for publication: A well-ordering proof for Feferman's theoryT 0
