The strength of some Martin-Löf type theories

DOI10.1007/BF01278464zbMATH Open0819.03047MaRDI QIDQ1344548FDOQ1344548

Authors: Edward R. Griffor, Michael Rathjen 

Publication date: 27 August 1995

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

Recommendations

• Publication:4944846
• scientific article; zbMATH DE number 1302068
• Well-ordering proofs for Martin-Löf type theory
• The strength of Martin-Löf type theory with a superuniverse. I
• Characterizing the interpretation of set theory in Martin-Löf type theory

zbMATH Keywords

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructive set theory
• Title not available (Why is that?)
• Constructivism in mathematics. An introduction. Volume II
• Title not available (Why is that?)
• Title not available (Why is that?)
• Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen
• Title not available (Why is that?)
• Proof-theoretic analysis of KPM
• Title not available (Why is that?)
• A well-ordering proof for Feferman's theoryT 0
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Recursive models for constructive set theories
• Title not available (Why is that?)
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• Title not available (Why is that?)

Cited In (43)

• Quotient topologies in constructive set theory and type theory
• Inaccessibility in constructive set theory and type theory
• On power set in explicit mathematics
• Inaccessible set axioms may have little consistency strength
• A characterization of ML in many-sorted arithmetic with conditional application
• Characterizing the interpretation of set theory in Martin-Löf type theory
• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• Title not available (Why is that?)
• Proof theory of constructive systems: inductive types and univalence
• On the proof-theoretic strength of monotone induction in explicit mathematics
• Realization of analysis into Explicit Mathematics
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
• A New Foundational Crisis in Mathematics, Is It Really Happening?
• An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe
• A cumulative hierarchy of sets for constructive set theory
• CZF and second order arithmetic
• 2004 Summer Meeting of the Association for Symbolic Logic
• The generalised type-theoretic interpretation of constructive set theory
• Functional interpretation of Aczel's constructive set theory
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• Independence results around constructive ZF
• Title not available (Why is that?)
• On Relating Theories: Proof-Theoretical Reduction
• Interpreting classical theories in constructive ones
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• 1999 European Summer Meeting of the Association for Symbolic Logic
• Non-deterministic inductive definitions
• Realizability and intuitionistic logic
• On the syntax of Martin-Löf's type theories
• Well-ordering proofs for Martin-Löf type theory
• Recent Advances in Ordinal Analysis: Π¹₂— CA and Related Systems
• Heyting-valued interpretations for constructive set theory
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• In memoriam: Kenneth Jon Barwise, 1942--2000
• Monotone inductive definitions in explicit mathematics
• Does mathematics need new axioms?
• Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
• On Tarski’s fixed point theorem
• 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• On the existence of Stone-Čech compactification

This page was built for publication: The strength of some Martin-Löf type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1344548)