On Relating Type Theories and Set Theories

The original motivation1 for the work described in this paper was to determine the proof theoretic strength of the type theories implemented in the proof development systems Lego and Coq, [12],[4]. These type theories combine the impredicative type of propositions2, from the calculus of constructions, [5], with the inductive types and hierarchy of type universes of Martin-Löf’s constructive type theory, [13]. Intuitively there is an easy way to determine an upper bound on the proof theoretic strength. This is to use the ‘obvious’ types-as-sets interpretation of these type theories in a strong enough classical axiomatic set theory. The elementary forms of type of Martin-Löf’s type theory have their familiar set theoretic interpretation, the impredicative type of propositions can be interpreted as a two element set and the hierarchy of type universes can be interpreted using a corresponding hierarchy of strongly inaccessible cardinal numbers. The assumption of the existence of these cardinal numbers goes beyond the proof theoretic strength of ZFC. But Martin-Löf’s type theory, even with its W types and its hierarchy of universes, is not fully impredicative and has proof theoretic strength way below that of second order arithmetic. So it is not clear that the strongly inaccessible cardinals used in our upper bound are really needed. Of course the impredicative type of propositions does give a fully impredicative type theory, which certainly pushes up the proof theoretic strength to a set theory3, Z−, whose strength is well above that of second order arithmetic. The hierarchy of type universes will clearly lead to some further strengthening. But is it necessary to go beyond ZFC to get an upper bound?