The strength of some Martin-Löf type theories

DOI10.1007/BF01278464zbMath0819.03047MaRDI QIDQ1344548

Edward R. Griffor, Michael Rathjen

Publication date: 27 August 1995

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

zbMATH Keywords

Kripke-Platek set theoryMartin-Löf's type theoryconstructive systemsclassical second-order arithmeticconstructive ZFintuitionistic second order arithmetic

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items

Inaccessible set axioms may have little consistency strength, Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice, On the proof-theoretic strength of monotone induction in explicit mathematics, Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience, On Tarski’s fixed point theorem, Non-deterministic inductive definitions, A New Foundational Crisis in Mathematics, Is It Really Happening?, Realization of analysis into Explicit Mathematics, Unnamed Item, Recent Advances in Ordinal Analysis: Π¹₂— CA and Related Systems, Monotone inductive definitions in explicit mathematics, Interpreting classical theories in constructive ones, On power set in explicit mathematics, On Relating Theories: Proof-Theoretical Reduction, A cumulative hierarchy of sets for constructive set theory, Independence results around constructive ZF, CZF and second order arithmetic, Quotient topologies in constructive set theory and type theory, Characterizing the interpretation of set theory in Martin-Löf type theory, Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms, Does Mathematics Need New Axioms?, Does Mathematics Need New Axioms?, 1999 European Summer Meeting of the Association for Symbolic Logic, On the existence of Stone-Čech compactification, 2004 Summer Meeting of the Association for Symbolic Logic, Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?, Proof Theory of Constructive Systems: Inductive Types and Univalence, The generalised type-theoretic interpretation of constructive set theory, The disjunction and related properties for constructive Zermelo-Fraenkel set theory, Functional interpretation of Aczel's constructive set theory, Well-ordering proofs for Martin-Löf type theory, Inaccessibility in constructive set theory and type theory, Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions, Heyting-valued interpretations for constructive set theory, 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05, 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\), Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe

Cites Work

• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• Proof-theoretic analysis of KPM
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Constructivism in mathematics. An introduction. Volume II
• Recursive models for constructive set theories
• Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen
• Constructive set theory
• 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