多重选择公理与构造性集合论的模型
逻辑
2013-09-27 v2
摘要
我们提出对Aczel构造性集合论CZF的一个扩展，通过增加一个归纳类型公理和一个选择原理，并证明该扩展具有以下性质：它可在Martin-Löf类型论中解释（因此从构造性和广义谓词性立场是可接受的）。此外，它足够强以证明集合紧致性定理以及形式拓扑中用到该定理的结果。而且，它在代数集合论的标准构造下是稳定的，即精确完备化、可实现性模型、力迫以及更一般的层扩张。因此，我们早期工作中的方法可用于证明该扩展满足各种导出规则，例如康托尔空间的导出紧致性规则和贝尔空间的导出连续性规则。最后，我们证明该扩展是稳健的，即它也能被前述代数集合论的模型构造所反映。
引用
@article{arxiv.1204.4045,
title = {The Axiom of Multiple Choice and Models for Constructive Set Theory},
author = {Benno van den Berg and Ieke Moerdijk},
journal= {arXiv preprint arXiv:1204.4045},
year = {2013}
}