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

Annals of Pure and Applied Logic 92 (2):113-159 (1998)
  Copy   BIBTEX


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 show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version à la Tarski and à la Russell are shown to be the same



    Upload a copy of this work     Papers currently archived: 94,420

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

38 (#415,628)

6 months
10 (#396,519)

Historical graph of downloads
How can I increase my downloads?

References found in this work

The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
A well-ordering proof for Feferman's theoryT 0.Gerhard Jäger - 1983 - Archive for Mathematical Logic 23 (1):65-77.
A new system of proof-theoretic ordinal functions.W. Buchholz - 1986 - Annals of Pure and Applied Logic 32:195-207.
Extending Martin-Löf Type Theory by one Mahlo-universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.

View all 10 references / Add more references