Brouwer’s Fan Theorem as an axiom and as a contrast to Kleene’s alternative
Brouwer’s Fan Theorem as an axiom and as a contrast to Kleene’s alternative
复制标题
布劳威尔扇形定理作为公理并与克莱恩替代定理对比
DOI：
10.1007/s00153-014-0384-9
复制
发表时间：
2011
影响因子：
0.3
通讯作者：
W. Veldman
中科院分区：
文献类型：
--
作者：
W. Veldman
本文是对直觉逆数学的一个贡献。我们引入一个正式的系统，称为基本直觉主义数学BIM，然后搜索语句，在BIM，相当于布劳威尔的风扇定理或其积极的否定，克莱因的替代风扇定理。Fan定理在预期的直觉解释下是正确的，Kleene的替代在由图灵可计算函数组成的BIM模型中是正确的。从直觉上讲，寻找克莱因替代方案的等价物的任务是寻找范定理的等价物的任务的一个非平凡的扩展，尽管在我们将试图使之透明的论证中存在某种对称性。我们引入Baire空间$${\mathcal{N}}$$N和真实的数的集合$${\mathcal{R}}$$R的闭可分子集。这样的集合可以是紧的，也可以是正非紧的。范定理是康托空间C或单位区间[0，1]是紧的，而克莱因替代定理是C或单位区间[0，1]是非紧的。紧闭可分集的类和正非紧闭可分集的类以许多不同的方式被刻画，并且发现了范定理和克莱因替代定理的许多等价物。
The paper is a contribution to intuitionistic reverse mathematics. We introduce a formal system called Basic Intuitionistic MathematicsBIM, and then search for statements that are, over BIM, equivalent to Brouwer’s Fan Theorem or to its positive denial, Kleene’s Alternative to the Fan Theorem. The Fan Theorem is true under the intended intuitionistic interpretation and Kleene’s Alternative is true in the model of BIM consisting of the Turing-computable functions. The task of finding equivalents of Kleene’s Alternative is, intuitionistically, a nontrivial extension of the task of finding equivalents of the Fan Theorem, although there is a certain symmetry in the arguments that we shall try to make transparent. We introduce closed-and-separable subsets of Baire space $${\mathcal{N}}$$N and of the set $${\mathcal{R}}$$R of the real numbers. Such sets may be compact and also positively noncompact. The Fan Theorem is the statement that Cantor space $${\mathcal{C}}$$C, or, equivalently, the unit interval [0, 1], is compact and Kleene’s Alternative is the statement that $${\mathcal{C}}$$C, or, equivalently, [0, 1], is positively noncompact. The class of the compact closed-and-separable sets and also the class of the closed-and-separable sets that are positively noncompact are characterized in many different ways and a host of equivalents of both the Fan Theorem and Kleene’s Alternative is found.
构造性逆向数学中的弱弱柯尼格引理
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
T. Nemoto;M.O. MedSalem;K. Tanaka;Takako Nemoto
通讯作者：
Takako Nemoto
DOI：
--
发表时间：
2005
期刊：
Oxford Logic Guides 48
影响因子：
--
作者：
Hajime Ishihara
通讯作者：
Hajime Ishihara