The axiom of multiple choice and models for constructive set theory
The axiom of multiple choice and models for constructive set theory
复制标题
多项选择公理和构造性集合论模型
DOI：
10.1142/s0219061314500056
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
I. Moerdijk
中科院分区：
文献类型：
--
作者：
B. V. D. Berg;I. Moerdijk
我们提出了一个扩展的Aczel的建设性集合论CZF的公理归纳类型和选择原则，并表明这种扩展具有以下性质：它是可解释的马丁-洛夫的类型理论（因此可以接受的建设性和广义谓词的观点）。此外，它也足够强，可以证明集紧性定理和利用该定理的形式拓扑学结果。此外，它在代数集合论的标准构造下是稳定的，即精确完备化，可实现模型，强迫以及更一般的层扩张。其结果是，从我们早期的工作方法可以应用到表明，这种扩展满足各种派生规则，如导出的康托空间的紧性规则和导出的连续性规则Baire空间。最后，我们表明，这种扩展是强大的意义上说，它也反映了刚才提到的代数集理论的模型构造。
We propose an extension of Aczel's constructive set theory CZF by an axiom for inductive types and a choice principle, and show that this extension has the following properties: it is interpretable in Martin-Lof's type theory (hence acceptable from a constructive and generalized-predicative standpoint). In addition, it is strong enough to prove the Set Compactness theorem and the results in formal topology which make use of this theorem. Moreover, it is stable under the standard constructions from algebraic set theory, namely exact completion, realizability models, forcing as well as more general sheaf extensions. As a result, methods from our earlier work can be applied to show that this extension satisfies various derived rules, such as a derived compactness rule for Cantor space and a derived continuity rule for Baire space. Finally, we show that this extension is robust in the sense that it is also reflected by the model constructions from algebraic set theory just mentioned.