Well-ordering proofs for Martin-Löf type theory
type: Item
instance of: scholarly article
title: Well-ordering proofs for Martin-Löf type theory
zbMATH Open document ID: 0928.03067
DOI: 10.1016/S0168-0072(97)00078-X
author: Anton Setzer
published in: Annals of Pure and Applied Logic
publication date: 1999-08-16T00:00:00Z
review text: In his Ph.D. thesis [Proof theoretical strength of Martin-Löf type theory with \(W\)-type and one universe, Diss., Univ. München (1993; Zbl 0863.03029)], the author proved an upper bound \(\alpha= \psi_{\Omega_1} \Omega_{I+\omega}\) for the proof-theoretic ordinal of Martin-Löf's intuitionistic type theory with \(W\)-type and one universe. In the present paper he proves in this system transfinite induction up to every ordinal less than \(\alpha\). This determines the proof-theoretic strength of the theory and shows that it is slightly stronger than Feferman's theory \(T_0\) and \((\Delta^1_2- \text{CA})+ (\text{BI})\). The author points out that the proof extends to show that the strength of Martin-Löf's type theory with \(n\) universes is \(\psi_{\Omega_1} \Omega_{I_n+ \omega}\) where \(I_n\) is the \(n\)th inaccessible, and this implies that the strength of the theory with arbitrary finitely iterated universes is \(\psi_{\Omega_1} I_\omega\) where \(I_\omega= \sup\{I_n\mid n\in\omega\}\).
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F15
zbMATH DE Number: 1308059
zbMATH Keywords: Martin-Löf's intuitionistic type theory
zbMATH Keywords: transfinite induction
zbMATH Keywords: proof-theoretic strength
zbMATH Keywords: finitely iterated universes
reviewed by: G. E. Mints
MaRDI profile type: Publication
cites work: Q4075450
cites work: Q3803111
cites work: Q3679172
cites work: Q4109654
cites work: A new system of proof-theoretic ordinal functions
cites work: Q3138829
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Die Beziehungen Zwischen den OrdinalzahlsystemenΣ Und $$\bar \Theta \left( \omega \right)$$
cites work: Q4040375
cites work: Q4128540
cites work: Q3773876
cites work: The strength of some Martin-Löf type theories
cites work: A well-ordering proof for Feferman's theoryT 0
cites work: Q3041187
cites work: Q4099613
cites work: Constructive mathematics and computer programming
cites work: Q3688389
cites work: Q3999860
cites work: Type-theoretic interpretation of iterated, strictly positive inductive definitions
cites work: Domain interpretations of Martin-Löf's partial type theory
cites work: Q3773877
cites work: How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinals
cites work: Q4143279
cites work: Q3800031
cites work: Q3138828
cites work: Q4715478
cites work: Q4364521
cites work: Proof theory. 2nd ed
cites work: On the syntax of Martin-Löf's type theories
cites work: Constructivism in mathematics. An introduction. Volume II
Recommended article: Q4247313
Recommended article: Q5438968
Recommended article: Representing inductively defined sets by wellorderings in Martin-Löf's type theory
Recommended article: A coherence theorem for Martin-Löf's type theory
Recommended article: Zermelo’s Well-Ordering Theorem in Type Theory
Recommended article: Polynomial-time Martin-Löf type theory
Recommended article: The constructive Hilbert program and the limits of Martin-Löf type theory
Recommended article: The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory
Recommended article: Well-Ordering Principles in Proof Theory and Reverse Mathematics
Recommended article: Q4715478
description: scientific article; zbMATH DE number 1308059