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

DOI10.1016/S0168-0072(97)00078-XzbMath0928.03067MaRDI QIDQ1295372

Anton Setzer

Publication date: 16 August 1999

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

zbMATH Keywords

proof-theoretic strengthtransfinite inductionMartin-Löf's intuitionistic type theoryfinitely iterated universes

Mathematics Subject Classification ID

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

Related Items

From realizability to induction via dependent intersection, Realization of analysis into Explicit Mathematics, Wellfoundedness proofs by means of non-monotonic inductive definitions. II: First order operators, On Relating Theories: Proof-Theoretical Reduction, Universes in explicit mathematics, Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms, Ordinal analysis by transformations, Proof Theory of Constructive Systems: Inductive Types and Univalence, Inaccessibility in constructive set theory and type theory, An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe, Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe, The constructive Hilbert program and the limits of Martin-Löf type theory

Cites Work

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