论文标题
无限直觉集合理论的真实性
Realisability for Infinitary Intuitionistic Set Theory
论文作者
论文摘要
我们介绍了基于序数图灵机（OTM）的无限直觉集合理论的真实性语义。我们表明，我们的OTM真实性概念相对于某些无限直觉逻辑系统而言是合理的，并且实现了无限kripke-platek set理论的所有公理。最后，我们利用我们的真实性概念的一种变体，表明（限制）直觉的kripke-platek集理论的命题可接受的规则正是直觉命题逻辑的可接受规则。
We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). We show that our notion of OTM-realisability is sound with respect to certain systems of infinitary intuitionistic logic, and that all axioms of infinitary Kripke-Platek set theory are realised. Finally, we use a variant of our notion of realisability to show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.
