带替换公理的 IZF 的正规化

ZF 是策梅洛 - 弗兰克尔集合论的一个经过深入研究的非直谓构造性版本。利用集合项，我们将带替换公理的 IZF（称为 \izfr）及其内涵对应物 \iizfr 公理化。根据柯里 - 霍华德同构原理，我们定义了与 \iizfr 中证明相对应的类型化 $\lambda$-演算 $\li$。利用针对 \iizfr 的可实现性，我们证明了 $\li$ 的弱正规化。我们利用正规化证明了析取性质、数值存在性质和项存在性质。通过引入一个内涵扩展模型，我们证明了全扩展 \izfr 的这些性质以及集合存在性质。