Extensional realizability for intuitionistic set theory
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
