Realizability for Constructive Zermelo-Fraenkel Set Theory
Realizability for Constructive Zermelo-Fraenkel Set Theory
复制标题
构造性 Zermelo-Fraenkel 集合论的可实现性
DOI：
10.1017/9781316755785.015
复制
发表时间：
2007
影响因子：
0.6
通讯作者：
M. Rathjen
中科院分区：
文献类型：
--
作者：
M. Rathjen
构造性策梅洛-弗伦克尔集合论（Constructive Zermelo-Fraenkel Set Theory，CZF）是一种标准的参考理论，它与构造性谓词数学有关，就像ZFC与经典的康托利亚数学有关一样。这个理论的一个特点是它拥有一个类型理论模型。Aczel表明，它在Martin-Lof的直觉主义类型理论中有一个公式作为类型的解释[14，15]。然而，本文所关注的是一种相当不同的解释。结果表明，Kleene可实现性为CZF提供了一个自验证语义，即这种可实现性的概念可以在CZF中形式化，并且可以证明在CZF中可以验证CZF的每个定理都是实现的。这种语义，然后，被用来建立几个equiconsiderable结果。具体来说，通过与俄罗斯建构主义和布劳威尔的直觉主义有密切关系的著名原则来扩充CZF，结果产生了具有相同可证明递归函数的同等证明理论强度的理论。MSC：03F50、03F35
Constructive Zermelo-Fraenkel Set Theory, CZF, has emerged as a standard reference theory that relates to constructive predicative mathematics as ZFC relates to classical Cantorian mathematics. A hallmark of this theory is that it possesses a type-theoretic model. Aczel showed that it has a formulae-as-types interpretation in Martin-Lof’s intuitionist theory of types [14, 15]. This paper, though, is concerned with a rather different interpretation. It is shown that Kleene realizability provides a self-validating semantics for CZF, viz. this notion of realizability can be formalized in CZF and demonstrably in CZF it can be verified that every theorem of CZF is realized. This semantics, then, is put to use in establishing several equiconsistency results. Specifically, augmenting CZF by well-known principles germane to Russian constructivism and Brouwer’s intuitionism turns out to engender theories of equal proof-theoretic strength with the same stock of provably recursive functions. MSC:03F50, 03F35