The strength of some Martin-Löf type theories (Q1344548)

The main result of this paper shows that the classical second-order arithmetic of \(\Delta^ 1_ 2- \text{CA}+ \text{BI}\) (bar induction) is reducible to \(\text{ML}_ 1 \text{W}\), Martin-Löf's type theory with one universe and the type of well-founded trees. The method used is, in the authors' parlance, a ``soft'' proof theory, like the interpretation of one theory into another, and no (hard) ordinal analysis is employed. The paper has the character of a survey, and many constructive theories are discussed, compared, and interpreted, on the way to achieving the above result. They include KP (Kripke-Platek set theory), CZF (constructive ZF of Aczel), \(\text{T}_ 0\) (of Feferman), and IARI (intuitionistic second order arithmetic). KP, CZF, \(\text{ML}_ 1 \text{V}\) (here, V is Aczel's set of iterative sets) and ten or so other theories are shown to be mutually interpretable. A second group contains \(\text{T}_ 0\), \(\Delta^ 1_ 2- \text{CA}+ \text{BI}\), KPi (i for inaccessible ordinal) and \(\text{ML}_{1 \text{W}} \text{V}\) (the subscript W indicates W-formation for small types). In the `Conclusions', the authors announce that they will consider intuitionistic transfinite types in the future.