Choice and independence of premise principles play an important role in characterizing Kreisel's modified realizability and G\"odel's Dialectica interpretation. In this paper we show that a great many intuitionistic set theories are closed under the corresponding rules for finite types over $\mathbb{ N}$. It is also shown that the existence property (or existential definability property) holds for statements of the form $\exists y^{ \sigma}\, \varphi(y)$, where the variable $y$ ranges over objects of finite type $\sigma$. This applies in particular to ${ \sf CZF}$ (Constructive Zermelo-Fraenkel set theory) and ${ \sf IZF}$ (Intuitionistic Zermelo-Fraenkel set theory), two systems known not to have the general existence property. On the technical side, the paper uses a method that amalgamates generic realizability for set theory with truth, whereby the underlying partial combinatory algebra is required to contain all objects of finite type.
Categories: math.LO