An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe

A. Setzer ()
Additional contact information
A. Setzer: Swansea University Bay Campus, Department of Computer Science

Chapter Chapter 16 in The Legacy of Kurt Schütte, 2020, pp 299-343 from Springer

Abstract: Abstract We present an upper bound for the proof theoretic strength of Martin-Lof’s type theory with W-type and one universe. This proof, together with the well ordering proof carried out in [12] shows that the proof theoretic strength of this theory is precisely ψΩ1ΩI+ω, which is slightly more than the strength of Feferman’s theory T0, the classical set theory KPI, and the subsystem of analysis (Δ12−CA)+(BI). The strength of the intensional and extensional version, and of the version a la Tarski and a la Russell are shown to be the same. The proof is carried out by interpreting the type theories in question in an extension of Kripke-Platek set theory KPI+. We show that validity of Π11-sentences is preserved in this interpretation.

Date: 2020
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-3-030-49424-7_16

Ordering information: This item can be ordered from
http://www.springer.com/9783030494247

DOI: 10.1007/978-3-030-49424-7_16

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().