A Normalizing Intuitionistic Set Theory with Inaccessible Sets

Abstract

We propose a set theory strong enough to interpret powerful type theories underlying proof assistants such as LEGO and also possibly Coq, which at the same time enables program extraction from constructive proofs. For this purpose, we axiomatize impredicative constructive version of Zermelo-Fraenkel set theory IZF with Replacement and $\omega$-many inaccessibles, which we call IZF_{R\omega}. Our axiomatization of IZF_{R\omega} utilizes set terms, an inductive definition of inaccessible sets and mutually recursive nature of equality and membership relations. It allows us to define a weakly-normalizing typed lambda calculus \lambda Z_\omega corresponding to proofs in IZF_{R\omega} according to the Curry-Howard isomorphism principle. We use realizability to prove the normalization theorem, which provides basis for extracting programs from IZF_{R\omega} proofs.