Choice and independence of premise rules in intuitionistic set theory

TL;DR

This paper investigates how choice and independence of premise rules influence intuitionistic set theories, demonstrating closure properties and the existence property for certain statements, especially in systems like CZF and IZF.

Contribution

It shows that many intuitionistic set theories are closed under rules for finite types and establishes the existence property for specific formulas, using a novel amalgamation of realizability and truth methods.

Findings

Many intuitionistic set theories are closed under rules for finite types.

The existence property holds for statements with objects of finite type.

CZF and IZF satisfy the existence property for certain formulas.

Abstract

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.