Normalization of IZF with Replacement

TL;DR

This paper axiomatizes IZF with Replacement, develops a typed lambda calculus for it, and proves normalization and key logical properties using realizability and model-theoretic techniques.

Contribution

It introduces a formal framework for IZF with Replacement and proves normalization and logical properties through realizability and models.

Findings

Weak normalization of the lambda calculus $ ext{li}$

Proof of disjunction, numerical existence, and term existence properties

Establishment of set existence property for extensional IZF with Replacement

Abstract

ZF is a well investigated impredicative constructive version of Zermelo-Fraenkel set theory. Using set terms, we axiomatize IZF with Replacement, which we call \izfr, along with its intensional counterpart \iizfr. We define a typed lambda calculus $\li$ corresponding to proofs in \iizfr according to the Curry-Howard isomorphism principle. Using realizability for \iizfr, we show weak normalization of $\li$. We use normalization to prove the disjunction, numerical existence and term existence properties. An inner extensional model is used to show these properties, along with the set existence property, for full, extensional \izfr.