论文标题
直觉集理论的扩展可实现性
Extensional realizability for intuitionistic set theory
论文作者
论文摘要
在设定理论的一般可实现性中，实现者一般处理无界量词。为了使这种可实现性形式，我们通过要求实现者应该在实现者上进行广泛采取行动，从而添加另一层扩展，从而导致一个可靠性$ \ mathrm {v_ {ex}}（a）$，其中在所有有限型$ {\ sf ac} $ a $ a $ a $ a $ a $ a $ a $ a $ a $ a $ a i is a $ as a $ a in a $中均可{\ sf ft。组合代数。该构造提供了许多设定理论的“内部模型”，这些理论还可以验证$ {\ sf ac} _ {\ sf ft} $，尤其是为$ \ sf czf $（构造性zermelo-fraenkel set）和$ \ \ \ \ \ sf izf izf $（Intuituitientiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantiantialwordion set）提供了一种自然化的语义。一个人还可以添加大型公理和许多其他原则。
In generic realizability for set theories, realizers treat unbounded quantifiers generically. To this form of realizability, we add another layer of extensionality by requiring that realizers ought to act extensionally on realizers, giving rise to a realizability universe $\mathrm{V_{ex}}(A)$ in which the axiom of choice in all finite types ${\sf AC}_{\sf FT}$ is realized, where $A$ stands for an arbitrary partial combinatory algebra. This construction furnishes 'inner models' of many set theories that additionally validate ${\sf AC}_{\sf FT}$, in particular it provides a self-validating semantics for $\sf CZF$ (Constructive Zermelo-Fraenkel set theory) and $\sf IZF$ (Intuitionistic Zermelo-Fraenkel set theory). One can also add large set axioms and many other principles.
