Well-ordering proofs for Martin-Löf type theory

DOI10.1016/S0168-0072(97)00078-XzbMATH Open0928.03067MaRDI QIDQ1295372FDOQ1295372

Authors: Anton Setzer 

Publication date: 16 August 1999

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Recommendations

• scientific article; zbMATH DE number 1302068
• Proof theory of Martin-Löf type theory. An overview
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• A coherence theorem for Martin-Löf's type theory
• Zermelo’s Well-Ordering Theorem in Type Theory
• Polynomial-time Martin-Löf type theory
• The constructive Hilbert program and the limits of Martin-Löf type theory
• The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory
• Well-Ordering Principles in Proof Theory and Reverse Mathematics
• Publication:4715478

zbMATH Keywords

proof-theoretic strengthtransfinite inductionfinitely iterated universesMartin-Löf's intuitionistic type theory

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35) Recursive ordinals and ordinal notations (03F15)

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?)
• Title not available (Why is that?)
• Proof theory. 2nd ed
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructivism in mathematics. An introduction. Volume II
• Title not available (Why is that?)
• The strength of some Martin-Löf type theories
• Title not available (Why is that?)
• Title not available (Why is that?)
• How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinals
• 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
• Title not available (Why is that?)
• A new system of proof-theoretic ordinal functions
• On the syntax of Martin-Löf's type theories
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• Domain interpretations of Martin-Löf's partial type theory
• Constructive mathematics and computer programming
• Title not available (Why is that?)
• Die Beziehungen Zwischen den OrdinalzahlsystemenΣ Und $$\bar \Theta \left( \omega \right)$$
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (28)

• Title not available (Why is that?)
• A flexible type system for the small Veblen ordinal
• Transfinite type theory and provability of second order formulas
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• Inaccessibility in constructive set theory and type theory
• Transfinite constructions in classical type theory
• Title not available (Why is that?)
• The strength of some Martin-Löf type theories
• Title not available (Why is that?)
• Polynomial-time Martin-Löf type theory
• The constructive Hilbert program and the limits of Martin-Löf type theory
• Proof theory of constructive systems: inductive types and univalence
• Proof theory of Martin-Löf type theory. An overview
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• From realizability to induction via dependent intersection
• Ordinal analysis by transformations
• Realization of analysis into Explicit Mathematics
• An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe
• On the strength of dependent products in the type theory of Martin-Löf
• Helly's selection theorem and the principle of local reflexivity of ordered type
• Wellfoundedness proofs by means of non-monotonic inductive definitions. II: First order operators
• Universes in explicit mathematics
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
• The strength of Martin-Löf type theory with a superuniverse. II
• On Relating Theories: Proof-Theoretical Reduction
• Zermelo’s Well-Ordering Theorem in Type Theory
• Universes in type theory. I. Inaccessibles and Mahlo
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe

This page was built for publication: Well-ordering proofs for Martin-Löf type theory

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