The independence of premise rule in intuitionistic set theories

TL;DR

This paper demonstrates that many intuitionistic set theories are closed under the independence of premise rule for finite types and establishes the existence property for certain formulas, using realizability methods.

Contribution

It shows the closure of intuitionistic set theories under the independence of premise rule and proves the existence property for specific formulas, including CZF and IZF.

Findings

Many intuitionistic set theories are closed under the independence of premise rule.

The existence property holds for formulas of the form ¬A → ∃x F(x) in these theories.

CZF and IZF satisfy the existence property for certain statements despite lacking it generally.

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.