Note on the fan theorem
Note on the fan theorem
复制标题
关于扇形定理的注释
DOI：
--
复制
发表时间：
1974
期刊：
影响因子：
--
通讯作者：
A. Troelstra
中科院分区：
文献类型：
--
作者：
A. Troelstra
本文的主要目的是建立一个定理，粗略地说明扇形定理和 的相加。基本分析的直觉系统的连续性模式导致了算术陈述的保守扩展。结果意味着，除了标准初等方法之外，一阶算术的一致性不能通过使用扇形定理来证明——尽管正是相反的假设导致 Gentzen 撤回了他的算术一致性证明的第一个版本（参见 [B]）。我们必须预先假定熟悉 [K, T] 的符号和主要结果，以及 [T1] 的第 II 章第 1.6 节和第 III 章第 4-6 节。一方面，我们将偏离 [K, T] 中的表示法：我们将使用 (n)x（而不是 g(n, x)）来指示由 n 编码的序列的第 x 个分量，如果 x < lth(n)，否则为 0。我们还介绍了下面经常使用的缩写 n ≤* m, a ≤ b：
The principal aim of this paper is to establish a theorem stating, roughly, that the addition of the fan theorem and the. continuity schema to an intuitionistic system of elementary analysis results in a conservative extension with respect to arithmetical statements. The result implies that the consistency of first order arithmetic cannot be proved by use of the fan theorem, in addition to standard elementary methods—although it was the opposite assumption which led Gentzen to withdraw the first version of his consistency proof for arithmetic (see [B]). We must presuppose acquaintance with notation and principal results of [K, T], and with §1.6, Chapter II, and Chapter III, §4-6 of [T1]. In one respect we shall deviate from the notation in [K, T]: We shall use (n)x (instead of g(n, x)) to indicate the xth component of the sequence coded by n, if x < lth(n), 0 otherwise. We also introduce abbreviations n ≤* m, a ≤ b which will be used frequently below: