集合论的简单计算解释
A simple computational interpretation of set theory
摘要：
CZF是一个集合论系统，在经典逻辑上，它等价于ZF，而在直觉主义逻辑上，它有一个众所周知的构造型理论解释。本文介绍了一个更简单、直观的构造性解释家族：集合是集合的良基可计算条件枚举。这个家族中的一种解释是：所有的集合都是通过迭代构造{f_n}从空集归纳构建的|n：N ^ g_n = h_n}，其中g和h是可计算的集合序列，f是可计算的序列，使得当g_n和h_n外延相等时f_n是一个集合。扩展的丘奇命题，一个与经典逻辑不相容的假设，需要使这成为CZF的模型。除了它的基本利益，它产生了一个直接的保守性结果，为某些选择原则，亚可数性公理，并为一些所谓的全知原则，包括一阶算术全知。这个家族中的一个更大的解释也模拟了正则扩展公理。
英文摘要：
CZF is a system of set theory which, over classical logic, is equivalent to ZF, while over intuitionistic logic, it has a well-known constructive type-theoretic interpretation. This article introduces a simpler, intuitive family of constructive interpretations: sets are well-founded extensional computable conditional enumerations of sets. One interpretation in this family is just this: all sets are inductively built from the empty set by iterating the construction {f_n | n:N ^ g_n = h_n}, where, in turn, g and h are computable sequences of sets, and f is a computable sequence such that f_n is a set when g_n and h_n are extensionally equal. Extended Church's Thesis, an assumption which is incompatible with classical logic, is required to make this a model of CZF. Besides its foundational interest, it yields a direct conservativity result for certain choice principles, the Subcountability axiom, and for some so-called Omniscience principles, including first-order arithmetic Omniscience. A larger interpretation in this family also models the Regular Extension Axiom.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
