The independence of premise rule in intuitionistic set theories

Abstract

Independence of premise principles play an important role in characterizing the modified realizability and the Dialectica interpretations. In this paper we show that a great many intuitionistic set theories are closed under the corresponding independence of premise rule for finite types over $\mathbb{N}$. It is also shown that the existence property (or existential definability property) holds for statements of the form $\neg A\to \exists x^{\sigma }F(x^{\sigma })$, where the variable $x^{\sigma }$ ranges over a finite type $\sigma$. This applies in particular to Constructive Zermelo-Fraenkel Set Theory (CZF) and Intuitionistic Zermelo-Fraenkel Set Theory (IZF), two systems known not to have the general existence property. On the technical side, the paper uses the method of realizability with truth from [21] and [8] with the underlying partial combinatory algebra (pca) chosen among the total ones. A particular instance of the latter is provided by the substructure of the graph model formed by the semi computable subsets of $\mathbb{N}$, which has the advantage that it forms a set pca even in proof-theoretically weak set theories such as CZF.