【SEP】数学与哲学直觉主义（二） (6-3)

在Anne Troelstra（1969）的版本中，最后一个公理被强化为：

(CS3+) ∃n□nA↔A（创造主体只证明真实的东西，而真实的东西将在某个时候被创造主体证明。）

第一个公理CS1是没有争议的：在任何时间点，都可以确定创造主体是否有对某一给定语句的证明。第二条公理CS2明确使用了创建主体是一个理想化的事实，因为它表达了证明将永远被记住。最后一个公理CS3是“创造主体”形式化中最有争议的部分，或者说，它的第二个结点（A→¬¬∃n□nA）是，它被Kreisel命名为“基督教慈善公理”。例如，Göran Sundholm（2014）认为，从建构的角度来看，"基督教慈善公理 "是不可接受的。而哥德尔不完备性定理甚至暗示，当□nA将被解释为在足够强的证明系统中可被证明时，该原则是错误的，然而，这肯定不是布劳威尔所想的解释。

给出一个声明 A 不包含对时间的任何提及，即没有出现 □ n ，我们可以根据以下规则来定义一个选择序列（Brouwer 1953）：

α(n)= {0 if ¬□nA

1 if □nA.

由此产生了第2.2节中介绍的被称为克里普克模式KS的原则，这个原则与创造主体理论的公理不同，不包含对时间的明确提及：∃α(A↔∃nα(n)=1).

使用克里普克的模式，弱的反例论证可以在不参考创造主体的情况下被正式表达。下面的例子取自（van Atten 2018）。设A是一个陈述，目前¬A∨¬A不知道是否成立。使用KS，可以得到选择序列α1和α2，这样：

¬A↔∃nα1(n)=1 ¬¬A↔∃nα2(n)=1

将这两个序列与实数联系起来 r 0 和 r 1 ，其中对于 i = 0 , 1 ：

ri(n)=0 if αi(n)≠1(−1)i2−mif for some m≤n，

αi(m)=1 and for no k＜m，αi(k)=1

那么对于 r = r 0 + r 1 ，声明 ¬ A ∨ ¬ ¬ A 隐含的是 ( r＞0 ∨ r＜0 ) ，这表明 ( r＞0 ∨ r＜0 ) 不能被证明。

在(van Dalen 1978)中，在算术和选择序列的背景下构建了一个创建主体公理的模型，从而证明它们与直觉算术和分析的某些部分相一致。在(van Dalen 1982)中，CS被证明对Heyting算术是保守的。克里普克方案的数学后果可以在(van Dalen 1997)中找到，其中表明KS和连续性公理拒绝马尔科夫原则，而KS与马尔科夫原则一起意味着排除中间原则。

克里普克已经证明KS意味着非递归函数的存在，这个结果不是他发表的，而是Kreisel(1970)发表的。显然，这意味着理论CS也意味着非递归函数的存在。关于CS的一个可能的论证如下。假设 X 是一个不可计算但可计算的可列举集，并定义函数 f 如下：

f(m，n)={0 if not □m(n∉X)

1 if □m(n∉X).

那么就可以看出， n ∉ X 当且仅当 f ( m , n ) = 1 对于一些自然数 m ，这意味着 f 不可能是可计算的。因为如果是这样，X的补数 X 的补数将是可计算的，这意味着 X . 由于 f 是一个函数，这就确定了在直觉主义中，并非所有函数都是可计算的。

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。