Constructive Zermelo-Fraenkel set theory, power set, and the calculus of constructions
pp. 313-349
in: P. Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm (eds), Epistemology versus ontology, Berlin, Springer, 2012Abstract
Full intuitionistic Zermelo-Fraenkel set theory, IZF, is obtained from constructive Zermelo-Fraenkel set theory, CZF, by adding the full separation axiom scheme and the power set axiom. The strength of CZFplus full separation is the same as that of second order arithmetic, using a straightforward realizability interpretation in classical second order arithmetic and the fact that second order Heyting arithmetic is already embedded in CZFplus full separation. This paper is concerned with the strength of CZFaugmented by the power set axiom, ({mathbf{CZF}}_{mathcal{P}}). It will be shown that it is of the same strength as Power Kripke–Platek set theory, (mathbf{KP}(mathcal{P})), as well as a certain system of type theory, ({mathbf{MLV}}_{mathbf{P}}), which is a calculus of constructions with one universe. The reduction of ({mathbf{CZF}}_{mathcal{P}})to (mathbf{KP}(mathcal{P}))uses a realizability interpretation wherein a realizer for an existential statement provides a set of witnesses for the existential quantifier rather than a single witness. The reduction of (mathbf{KP}(mathcal{P}))to ({mathbf{CZF}}_{mathcal{P}})employs techniques from ordinal analysis which, when combined with a special double negation interpretation that respects extensionality, also show that (mathbf{KP}(mathcal{P}))can be reduced to CZFwith the negative power set axiom. As CZFaugmented by the latter axiom can be interpreted in ({mathbf{MLV}}_{mathbf{P}})and this type theory has a types-as-classes interpretation in ({mathbf{CZF}}_{mathcal{P}}), the circle will be completed.