Constructive Set Theory and Brouwerian Principles
Constructive Set Theory and Brouwerian Principles
复制标题
构造性集合论和布劳威尔原理
DOI：
10.3217/jucs-011-12-2008
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
M. Rathjen
中科院分区：
文献类型：
--
作者：
M. Rathjen
本文提出了建设性Zermelo-Fraenkel集合理论（CZF）的可实现性模型，验证了连续选择公理（CC）、扇定理（FT）、单调条归纳法（BIM）等Brouwerian原理，从而确定了这些原理增强的CZF的证明理论强度。结果是，CZF+CC+FT具有与CZF相同的强度，或者更准确地说，CZF+CC+FT对于02个算术命题在CZF上是保守的，而在CZF上添加一个受限的条形归纳（称为可判定条形归纳，BID），使得证明理论强度更大，因为CZF+BID证明了CZF的一致性。
The paper furnishes realizability models of constructive Zermelo-Fraenkel set theory, CZF, which also validate Brouwerian principles such as the axiom of continuous choice (CC), the fan theorem (FT), and monotone bar induction (BIM), and thereby determines the proof-theoretic strength of CZF augmented by these principles. The upshot is that CZF+CC+FT possesses the same strength as CZF, or more precisely, that CZF+CC+FTis conservative over CZF for 02 statements of arithmetic, whereas the addition of a restricted version of bar induction to CZF (called decidable bar induction, BID) leads to greater proof-theoretic strength in that CZF+BID proves the consistency of CZF.