Well-ordering proofs for Martin-Löf type theory Original Research Article

We present well-ordering proofs for Martin-Löfʹs type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer (1993) show that the proof theoretical strength of the type theory is precisely View the MathML source, which is slightly more than the strength of Fefermanʹs theory T0, classical set theory KPI and the subsystem of analysis (Δ12 − CA) + (BI). The strength of intensional and extensional version, of the version à la Tarski and à la Russell are shown to be the same.