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
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
