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

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

Abstract

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

Links

PhilArchive



    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

Analytics

Added to PP
2014-01-16

Downloads
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