不可达集的规范化直觉集合论
A Normalizing Intuitionistic Set Theory with Inaccessible Sets
摘要：
我们提出了一个集理论强大到足以解释强大的类型论的基础证明助手，如乐高，也可能Coq，这在同一时间，使程序提取其建设性的证明。为了这个目的，我们公理化Zermelo-Fraenkel集理论IZF与替换和$ω$ -许多不可接近的，我们称之为\izfio的一个不可预测的建设性版本。我们的公理化利用集条款，一个归纳的定义不可访问的集合和相互递归性质的平等和成员关系。它允许我们根据Curry-Howard同构原则定义一个弱规范化类型λ演算，对应于\izfio中的证明。我们使用可实现性来证明规范化定理，这为程序抽取能力提供了基础。
英文摘要：
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 its constructive proofs. For this purpose, we axiomatize an impredicative constructive version of Zermelo-Fraenkel set theory IZF with Replacement and $ω$-many inaccessibles, which we call \izfio. Our axiomatization utilizes set terms, an inductive definition of inaccessible sets and the mutually recursive nature of equality and membership relations. It allows us to define a weakly-normalizing typed lambda calculus corresponding to proofs in \izfio according to the Curry-Howard isomorphism principle. We use realizability to prove the normalization theorem, which provides a basis for program extraction capability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
