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

Constructive 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. per 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 . 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.