具有不可达集合的正规化直觉主义集合论

我们提出了一种足够强大的集合论，能够解释 LEGO 以及可能的 Coq 等证明助手所基于的强大类型论，同时能够从其构造性证明中提取程序。为此，我们公理化了一种带有替换公理和 $\omega$-多个不可达集的不可预测构造性版本的 Zermelo-Fraenkel 集合论 IZF，我们称之为 \izfio。我们的公理化利用了集合项、不可达集的归纳定义以及相等关系和隶属关系的相互递归性质。它允许我们根据 Curry-Howard 同构原理，定义一个对应于 \izfio 中证明的弱正规化类型 lambda 演算。我们使用 realizability 来证明正规化定理，这为程序提取能力提供了基础。