Reading “Un upper bound for the proof-theoretic strength of Martin-Löf type theory with W-type and one universe” by Anton Setzer

The paper preciselly formalizes Martin-Löf constructive type theory with the W-type (inductive definitions) and one universe, in its intensional and extensional variants, and in its variants “à la Tarski” and “à la Russell”, as well as a version/extension of classical Kripke-Platek set theory. It is then shown how to interpret the extensional type theory into Kripke-Platek set theory, from which an upper bound on the proof-theoretic strength is obtained. Together with previous results on a lower bound for intensional type theory (and an embedding into the extensional one), one obtains as a precise characterisation for the proof-theoretic strength of all variants of type theory the ordinal ψΩ1ΩI+ω.

Actually this is the most precise and succinct formulation of type theory that I have seen and should be helpful for relative interpretations of/inside type theory as well as implementing proof tools.

Comments @danko@mamot.fr