The strength of some Martin-Löf type theories
From MaRDI portal
(Redirected from Publication:1344548)
Recommendations
Cites work
- scientific article; zbMATH DE number 3833954 (Why is no real title available?)
- scientific article; zbMATH DE number 3839951 (Why is no real title available?)
- scientific article; zbMATH DE number 3900744 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 4012604 (Why is no real title available?)
- scientific article; zbMATH DE number 3687373 (Why is no real title available?)
- scientific article; zbMATH DE number 3754682 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 3494394 (Why is no real title available?)
- scientific article; zbMATH DE number 3556031 (Why is no real title available?)
- scientific article; zbMATH DE number 946307 (Why is no real title available?)
- A well-ordering proof for Feferman's theoryT 0
- Constructive set theory
- Constructivism in mathematics. An introduction. Volume II
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Proof-theoretic analysis of KPM
- Recursive models for constructive set theories
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen
Cited in
(43)- A New Foundational Crisis in Mathematics, Is It Really Happening?
- 1999 European Summer Meeting of the Association for Symbolic Logic
- Functional interpretation of Aczel's constructive set theory
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
- On the syntax of Martin-Löf's type theories
- Well-ordering proofs for Martin-Löf type theory
- The disjunction and related properties for constructive Zermelo-Fraenkel set theory
- Realization of analysis into Explicit Mathematics
- 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05
- Non-deterministic inductive definitions
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
- Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
- Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
- CZF and second order arithmetic
- On Relating Theories: Proof-Theoretical Reduction
- Interpreting classical theories in constructive ones
- In memoriam: Kenneth Jon Barwise, 1942--2000
- Monotone inductive definitions in explicit mathematics
- Realizability and intuitionistic logic
- Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
- Characterizing the interpretation of set theory in Martin-Löf type theory
- Independence results around constructive ZF
- An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe
- Inaccessible set axioms may have little consistency strength
- A cumulative hierarchy of sets for constructive set theory
- scientific article; zbMATH DE number 1420782 (Why is no real title available?)
- Does mathematics need new axioms?
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
- On the proof-theoretic strength of monotone induction in explicit mathematics
- Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
- A characterization of ML in many-sorted arithmetic with conditional application
- Proof theory of constructive systems: inductive types and univalence
- scientific article; zbMATH DE number 7379292 (Why is no real title available?)
- Inaccessibility in constructive set theory and type theory
- On power set in explicit mathematics
- Quotient topologies in constructive set theory and type theory
- 2004 Summer Meeting of the Association for Symbolic Logic
- Recent Advances in Ordinal Analysis: Π12— CA and Related Systems
- The generalised type-theoretic interpretation of constructive set theory
- On Tarski’s fixed point theorem
- On the existence of Stone-Čech compactification
- Heyting-valued interpretations for constructive set theory
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)
