Characterizing the interpretation of set theory in Martin-Löf type theory

AbstractConstructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization (by a few axiom schemata say) of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized by suitable forms of the axiom of choice.The paper builds on a self-interpretation of CZF (developed in [M. Rathjen, The formulae-as-classes interpretation of constructive set theory, in: Proof Technology and Computation (Proceedings of the International Summer School Marktoberdorf 2003) IOS Press, Amsterdam, 2004 (in press)]) that provides an “inner” model of CZF which also validates the so-called ΠΣ-axiom of choice, ΠΣ–AC. The crucial technical step taken in the present paper is to investigate the absoluteness properties of this model under the hypothesis ΠΣ–AC.It is also shown that CZF plus the ΠΣ-axiom of choice possesses the disjunction property, the numerical existence property and the existence property for an important group of formulae