【SEP】数学与哲学直觉主义（一）

数学哲学中的直觉主义 Intuitionism in the Philosophy of Mathematics

原作者：Iemhoff, Rosalie

URL: https://plato.stanford.edu/archives/fall2020/entries/intuitionism/

Translator: Demian

Proofreader：Demian

直觉主义是一种由荷兰数学家布劳威尔（L.E.J. Brouwer 1881-1966）提出的认为数学是心灵的构造的观点。一个数学陈述的真理只能通过证明它是真的心理构造来确证，而数学家之间的交流只是作为在不同的头脑中创造相同的心理过程的一种手段。

这种对数学的看法对数学的日常实践有着深远的影响，其后果之一就是对排中律的冲击。即“A∨¬A”这一逻辑形式不再有效。事实上，有些命题，比如黎曼假设，目前既没有使其成立的证明，也没有否定它的证明。由于在直觉主义中，知道一个陈述的否定，意味着人们可以证明该陈述不是真的，也就是说，无论是A还是¬A在这个时候的直觉上都不成立。直觉主义对时间的依赖性是至关重要的：语句在时间过程中可以变得可被证明，因此可能变得直观有效，即使以前不是这样。

除了拒斥排中律以外，直觉主义在连续体（continuum）的概念上也强烈地偏离了经典数学，在前者的设定中，连续体的特性是它上面的所有总函数都是连续的。因此，与其他几种构造数学的理论不同，直觉主义不是限制经典推理，而是在根本上与经典数学相矛盾。

布劳威尔把他生命中的大部分时间都用于在这个新基础上发展数学。虽然直觉主义从未取代经典数学成为数学的标准观点，但它一直吸引着人们的注意力，至今仍被广泛研究。

在本条目中，我们集中讨论了直觉主义有别于建构主义（constructivism也译作构造主义）数学其他分支的方面，而它与其他形式的建构主义（如基础理论和模型）共有的部分，只作了简单的讨论。

目录：

1布劳威尔

2直觉主义

2.1 直觉主义的两个规定

2.2 创造主体

3数学

3.1 BHK解释

3.2 直觉主义逻辑‬

3.3 自然数

3.4 连续体

3.5 连续性公理

3.6 条形定理（The bar theorem）

3.7 选择公理‬

3.8 描述性集合论、拓扑学和拓扑理论‬

4建构主义

5元数学‬

5.1 算术

5.2 分析

5.3 无规律的序列

5.4 创造主体的形式化

5.5 基础和模型

5.6 逆向数学‬

6哲学

6.1 现象学‬

6.2 维特根斯坦

6.3 达米特

6.4 有穷主义‬

1布劳威尔

卢特森·埃格伯特斯·扬·布劳威尔出生于荷兰的奥弗斯奇。他在阿姆斯特丹大学学习数学和物理学，并于1907年获得博士学位。1909年，他成为该大学的讲师，1912年被任命为正教授，一直到1951年退休。布劳威尔是一位杰出的数学家，他在拓扑学方面做了开创性的工作，在年轻时就已经成名。在他的一生中，他都是一个独立的人，以热忱的态度追求他所相信的东西，这使他与许多同事发生冲突，最明显的是与大卫·希尔伯特。他也有崇拜者，在他位于布拉里库姆的“小屋”里，他接待了他那个时代的许多知名数学家。在他生命的最后阶段，他变得更加孤僻，但他对自己哲学真理的信念从未动摇过。在妻子利泽·布劳威尔去世七年后，他在布拉里库姆死于一场车祸，享年85岁。

24岁时，布劳威尔写了《生活、艺术和神秘主义》（1905）一书，其唯我论（solipsistic）的内容预示了他的数学哲学的风格。在他的论文中首次提出了直觉主义的基础，尽管还没有用这个名字，也没有形成最终的形式。在他的论文之后的最初几年，布劳威尔的大部分科学生活都致力于拓扑学，在这个领域，他仍然以他的维度（dimension）理论和他的定点定理（fixed-point theorem）闻名。这项工作是经典数学的一部分，根据布劳威尔后来的观点，他的定点定理并不成立。尽管根据他的原则，可以通过拟合（analogue cast）达到近似值（approximations）。

从1913年开始，布劳威尔越来越多地致力于将其论文中提出的观点发展为完整的数学哲学。他不仅完善了直觉主义的哲学，而且还根据这些原则重修了数学，特别是连续体理论和集合理论。那时，布劳威尔已经是一位著名的数学家，他在当时的科学圣地如剑桥、维也纳和哥廷根等地就直觉主义进行了有影响力的演讲。尽管他的哲学被许多人认为是蹩脚的，但却被当时一些最有名的数学家当作经典数学的严肃替代方案，即使他们对这个问题有不同的看法。库尔特·哥德尔就是其中之一，虽然他一生都是柏拉图主义者。赫尔曼·魏尔（Hermann Weyl）有一次写道：“因此，现在我放弃了自己的主张，加入了布劳威尔的行列”（Weyl 1921, 56）。虽然魏尔后来很少实践直觉主义数学，但他从未停止过对布劳威尔及其直觉主义数学哲学的欣赏。

布劳威尔的一生充满了冲突，最著名的一次是与大卫·希尔伯特的冲突，这最终导致布劳威尔被逐出《数学年鉴》的董事会。这场冲突是20世纪初震撼数学界的基础性争论的一部分，它是由于数学中出现悖论和高度非结构性证明而出现的。哲学家和数学家被迫承认，数学缺乏认识论和本体论的基础。而布劳威尔的直觉主义就是一种旨在提供一个这样的基础的数学哲学。

2直觉主义

2.1 直觉主义的两个规定

根据布劳威尔的说法，数学是一种无语言的心灵创造。在康德主义的意义上，时间是唯一的先验概念。布劳威尔区分了直觉主义的两个规定：

直觉主义的第一个规定是：

“将数学与数学语言完全分开，进而与理论性逻辑所描述的语言现象完全分开，从而认识到直觉主义数学是一种本质上无语言的心灵活动，其起源于对时间运动的感知。这种对时间运动的感知可以被描述为将一个生命瞬间分解为两个不同的东西，其中一个让位于另一个，但被记忆所保留。如果这样诞生的二元性被剥离了所有的质量，它就会进入所有二元性的共同基质的空的形式。而正是这种共同的基质，这种空的形式，是数学的基本直觉。”（布劳威尔 1981, 4-5）

正如将在关于数学的章节中讨论的那样，直觉主义的第一个规定产生了自然数，但这意味着对所允许的推理原则的严重限制，最明显的是对排中律的拒斥。由于对这一原则的拒斥和连续体的逻辑基础的消失，用布劳威尔的话说，人们可能会“担心直觉主义的数学必然是贫乏与贫瘠的，特别是没有分析的地方”（布劳威尔 1952, 142）。然而，第二个规定确立了连续体的存在，这种连续体具有它的经典对应物所没有的属性。连续体的恢复依赖于第二个规定中的选择序列的概念，即依赖于自由选择产生的无穷序列的存在，因此这些序列不是事先固定的。

直觉主义的第二个规定是：

“承认创造新的数学实体的两种方式：首先是以先前获得的数学实体或多或少自由进行的无穷序列的形式……；其次是数学种类的形式，即对以前获得的数学实体可假设的属性，满足这样的条件：如果它们对某一数学实体成立，它们也对所有被定义为与之‘相等’的数学实体成立……”（布劳威尔1981, 8）

直觉主义的两个规定构成了布劳威尔哲学的基础，仅从这两个规定中，布劳威尔就创造了直觉主义数学的领域，这一点将在下文解释。从这一基本原则中已经可以得出结论：直觉主义与柏拉图主义和形式主义不同，因为它既未假设存在于我们之外的数学实在，也不认为数学是在按照某些固定规则玩弄符号。在布劳威尔看来，语言是用来交流数学思想的，但后者的存在是独立于前者的。直觉主义与其他数学建构主义观点之间的区别在于，根据这些观点，数学对象与其论证应该是可计算的，第二个规定在构建无穷序列时允许自由。事实上，正如下文所解释的，直觉主义的第二规定的数学含义与经典数学相矛盾，因此在大多数建构主义理论中都不成立，因为这些一般都是经典数学的一部分。

因此，布劳威尔的直觉主义与其他数学哲学不同，它是基于对时间的认识和数学是自由的思想而创造的信念，因此它既不是柏拉图主义，也不是形式主义。它是建构主义的一种形式，但只是在更广泛的意义上，因为许多建构主义者并不接受布劳威尔认为是真的的全部原则。

2.2 创造性主体

直觉主义的两个规定本身并不排除对数学的心理学解释。虽然布劳威尔只是偶尔谈到这一点，但从他的著作中可以看出，他确实认为直觉主义是独立于心理学的。布劳威尔将“创造性主体（Creating Subject）”（布劳威尔1948）作为一个理想化的心智（idealized mind），在其中发生数学，已经抽象出人类推理的非必要方面，如空间和时间的限制以及错误论证的可能性。因此，要求解释人类能够交流这一事实的主体间性问题就不存在了，因为只存在一个创造性主体。在文献中，创造性（Creating）主体的名称也被用于创造（Creative）主体，但这里使用的是布劳威尔的术语。在(Niekus 2010)中，有人认为布劳威尔的创造性主体并不涉及一个理想化的数学家。关于创造性主体作为胡塞尔意义上的超越性主体的现象学分析，见（van Atten 2007）。

布劳威尔用包含“创造性主体”的论证来构造某些在直觉上不可接受的陈述的反例。下面要讨论的弱反例（weak counterexamples）只表明某些陈述目前在直觉上不能被接受，而理想化心灵的概念则证明了某些经典的原则是错误的。在第5.4节关于创造性主体概念的形式化中给出了一个例子。那里还解释了以下原则，即克里普克的模式，可以用创造性主体来论证：

（KS） ∃α（A↔∃nα（n）=1）

在KS中，A的范围是公式，α的范围是选择序列，选择序列是由创造性主体产生的自然数序列，创造性主体逐一选择其元素。选择序列和克里普克模式将在第3.4节进一步讨论。

在大多数数学哲学中，例如柏拉图主义，数学陈述是无时态的。但直觉主义中的真假有一个时间面向：即既定事实将保持不变，但在某个时刻才得到证实的陈述在该时刻之前不具有真值。在“创造性主体”概念的形式化中，直觉主义的时间面向明显存在，而这一概念并非由布劳威尔提出，而是后来才由其他人提出。

尽管使用创造性主体概念的论证对于进一步理解作为数学哲学的直觉主义可能很重要，但它在该领域的发展中的作用不如直觉主义的两个规定的影响大，后者直接导向了布劳威尔和他以后的人愿意接受的数学真理。

3. 数学

尽管布劳威尔对直觉主义的发展在20世纪初数学家们的基础性争论中发挥了重要作用，但他的哲学对数学的深远影响在多年研究后才显现出来。直觉主义最典型的两个特性是它在证明中允许的逻辑推理原则和对直觉连续体的全面构想。只有在后者中，直觉主义才变得与经典数学不可比拟。在本条目中，重点是那些使直觉主义有别于其他数学学科的原则，因此，它的其他构造性方面将得到较少地处理。

3.1 BHK解释

在直觉主义中，知道一个陈述A是真的意味着有对它的证明。1934年，曾是布劳威尔学生的海廷（Arend Heyting）提出了一种后来被称为Brouwer-Heyting-Kolmogorov解释的说明形式，它抓住了直觉主义以及一般建构主义中逻辑符号的意义，通过指出连接词和量词应该如何解释，以一种非正式的方式定义了直觉主义的证明应该包括哪些内容：

• ⊥是不可证明的；

• A∧B 的证明由 A 的证明和 B 的证明组成；

• A∨B 的证明由一个 A 的证明或一个 B 的证明组成；

• A→B 的证明是一个将任何对 A 的证明转换为对 B 的证明的结构；

• ∃xA(x)的证明是通过提出该域的一个元素 d 以及 A(d)的证明来实现的；

• ∀xA(x)的证明是一种结构，它将每个证明d属于该域的证明转化为A(d)的证明。

一旦证明不可能存在A的证明，即提供一个结构，从A的任何可能的证明中导出错误，那么公式A的否定¬A就被证明了。因此，¬A与A→⊥等价。BHK解释并不是一个正式的定义，其构造的概念没有被定义，因此可以有不同的解释。不过，在这个非正式的层面上，人们已经被迫拒绝了经典逻辑中一直存在的一个逻辑原则：排中律(A∨¬A)。根据BHK解释，如果创造性主体知道A的证明或者A不能被证明的证明，那么这个陈述在直觉上就成立。如果既不知道 A 的证明，也不知道 A 的否定的证明，则(A∨¬A)不成立。开放性问题的存在，如哥德巴赫猜想或黎曼假设，都说明了这个事实。但是一旦找到了 A 的证明或者其否定的证明，情况就改变了，对这个特定的 A 来说，原则(A∨¬A)从那一刻起就是真的。

3.2 直觉主义逻辑

布劳威尔在他的哲学基础上拒斥了排中律，但阿伦德·海廷是第一个从直觉主义的角度提出一个可以接受的全面的逻辑原则的人。直觉主义逻辑，也是大多数其他形式的建构主义的逻辑，通常被称为“没有排中律的古典逻辑”。它用IQC来表示，IQC代表直觉主义量词逻辑，但文献中也有其他名称。一个可能的希尔伯特式的公理化由以下原则组成：

A∧B→A A∧B→B A→A∨B B→A∨B

A→(B→A) ∀xA(x)→A(t) A(t)→∃xA(x) ⊥→A

(A→(B→C)) →((A→B)→(A→C))

A→(B→A∧B)

(A→C)→((B→C)→(A∨B→C))

∀x(B→A(x)) →(B→∀xA(x))

∀x(A(x)→B) →(∃xA(x)→B)

伴随着最后两个公理的通常侧面条件，以及“模因”规则，

从A和（A→B）推出 B

作为推理的唯一规则，自从海廷提出直觉主义逻辑以来，它一直是研究的对象。在命题层面上，它已经有了许多不同于经典逻辑的特性，比如说析取属性：

(DP) IQC ⊢ A∨B implies IQC ⊢ A or IQC ⊢ B.

这个原则显然是与经典逻辑相冲突的，因为经典逻辑对独立于其的公式也证明了(A∨¬A)，即对A和¬A都不是同义词。把“Ex Falso Sequitur Quodlibet (⊥→A)”这一原则纳入到直觉主义逻辑中，是研究布劳威尔关于这个问题的言论的讨论点。在van Atten 2008中，有人认为这一原则在直觉主义中是无效的，根据布劳威尔的观点，有效的逻辑原则是相关性逻辑的原则。关于布劳威尔和Ex Falso Sequitur Quodlibet的更多信息，见van Dalen 2004。

尽管到今天为止，直觉主义推理中使用的所有逻辑都包含在IQC中，但在原则上可以想象，在某些时候会发现一个从直觉主义观点来看可以接受的原则，而这个逻辑却没有涵盖到。对于大多数形式的建构主义来说，被普遍接受的观点是，这种情况永远不会出现，因此，IQC被认为是建构主义的逻辑。对于直觉主义来说，情况就不太清楚了，因为不能排除在某个时候，我们的直觉主义理解可能会引导我们找到我们之前没有掌握的新的逻辑原则。

直觉主义逻辑被广泛使用的原因之一是它在证明理论和模型理论的角度都表现良好。它有许多证明系统，如根岑（Gentzen）计算法和自然演绎系统，以及各种形式的语义学，如克里普克模型、贝斯模型、海廷矩阵、拓扑语义学和分类模型。然而，这些语义中的几个只是研究直觉主义逻辑的经典手段，因为可以证明，关于它们的直觉主义完全性证明是不存在的(Kreisel 1962)。然而，已经证明有一些替代性的但不那么自然的模型，对于这些模型，完全性确实是建构性的(Veldman 1976)。直观逻辑的建构性特征在库里-霍华德同构中变得特别明显，该同构在逻辑中的派生与简单类型的λ-微积分中的术语之间建立了对应关系，也就是说，在证明与计算之间。这种对应关系保留了结构，因为术语的减少对应于证明的规范化。

3.3 自然数

自然数的存在是由直觉主义的第一个规定给出的，即通过对时间运动的感知，以及将生命的瞬间分解成两个不同的东西：过去的东西1，和现在的东西2，以及从那里到3，4……与古典数学相反，在直觉主义中，所有的无穷被认为是潜无穷。特别是自然数的无穷大就是这种情况。因此，对这个集合进行量化的声明必须谨慎对待。另一方面，从直觉的角度来看，归纳法的原则是完全可以接受的。

由于自然数的有限性与实数等相比，许多在经典数学中是真实的有限性质的算术陈述在直觉主义中也是如此。例如，在直觉主义中，每个自然数都有一个质因数；存在着不可计算的可列举的集合，(A∨¬A)对所有无量词的语句A都成立。对于更复杂的语句，如范德瓦登定理或克鲁斯卡尔定理，直观性的有效性并不那么直接。事实上，这两个语句的直觉主义证明是复杂的，并且偏离了经典证明（Coquand 1995, Veldman 2004）。

因此，在自然数的背景下，直觉主义和经典数学有很多共同之处。只有涉及到其他无穷集，如实数时，直觉主义才开始与经典数学，以及与大多数其他形式的建构主义有更大的区别。

3.4 连续体（The continuum）

在直觉主义中，连续体既是其古典对应物的延伸，也是其限制。在它的完整形式中，这两个概念是不可比拟的，因为直觉实数拥有经典实数所不具备的属性。下面要讨论的一个著名的例子是，在直觉主义中，连续体上的每个完整的函数都是连续的。直观连续体不满足某些经典属性，这一点可以通过弱反例很容易看出。它还包含经典实数不具备的属性，这源于直觉主义中选择序列的存在。

弱反例（Weak counterexamples）

布劳威尔在1908年提出的弱反例，是布劳威尔用来证明从经典数学概念到直觉主义数学概念的转变对根据这些哲学可以建立的数学真理并非没有影响的第一个例子。他们表明，从直觉的角度来看，某些经典的陈述目前是不可接受的。作为一个例子，考虑由以下定义给出的实数序列：

rn= {2⁻ⁿ if ∀m≤nA(m)

{2⁻ₘ if ¬A(m)∧m≤n∧∀k＜mA(k).

这里A(n)是一个可解的属性，对于它来说，∀nA(n)不知道是真还是假。可判定性意味着目前对于任何给定的n，存在（或可以构造）一个A(n)或¬A(n)的证明。在写这篇文章的时候，我们可以让A(n)表示n如果大于2，是三个素数之和，然后∀nA(n)表示（原初）哥德巴赫猜想，每个大于2的数都是三个素数之和。序列⟨rn⟩定义了一个实数r，对于这个实数，语句r=0等同于语句∀nA(n)。由此可见，语句(r=0∨r≠0)不成立，因此，三段论的规律∀x(x＜y∨x=y∨x＞y)在直觉连续体上不成立。

请注意“A在直觉上不是真的”和“A在直觉上是可反驳的”之间的微妙区别：在第一种情况下，我们知道A不可能有直觉上的证明，第二种说法表示我们有一个¬A的证明，一个从任何可能的A的证明中推导出错误的构造。下面我们将证明，即使是第二种更强的形式，即该法则是可反驳的，也在直觉上成立。然而，对于所有存在弱反例的陈述来说，这并不是真的。例如，哥德巴赫猜想是排中律的一个弱反例，因为上述的∀nA(n)目前还不知道是真的还是假的，因此我们不能凭直觉断言∀nA(n)∨¬∀nA(n)，至少在此刻不能。但是对这个陈述的反驳，¬(∀nA(n)∨¬∀nA(n))，在直觉中不是真的，因为我们可以证明，对于任何陈述B，都可以从¬B和¬¬B成立的假设中得出矛盾（因此也可以从B和¬B中得出矛盾）。换句话说，¬¬(B∨¬B)在直觉上是真的，因此，虽然存在排中律的弱反例，但它的否定在直觉主义中是假的，也就是说，它在直觉上是可驳斥的。

实数r的存在，直觉主义者无法决定它们是否为正数，这表明某些经典的总体函数在直觉主义的环境中将不再如前，如片状常数函数：

f(r)= {0 if r ≥0

{1 if r ＜0.

许多经典的有效语句都存在弱反例。这些弱反例的构造往往与上述例子的模式相同。例如，表明中值定理在直觉主义上无效的论证如下：设r是[-1，1]中的一个实数，对于这个实数，就像上面的例子一样(r≤0∨0＜r)还没有决定，定义[0，3]上的均匀连续函数f为：

f(x)=min(x−1,0) +max (0, x−2) +r.

显然，f(0)=−1+r，f(3)=1+r，因此f在[0，3]中的某个点x取值为0。如果可以确定这样的x，要么1≤x，要么x≤2。由于f在[1，2]上等于r，在第一种情况下r≤0，在第二种情况下0≤r，与语句的不可判定性相矛盾(r≤0∨0≤r)。

这些例子似乎表明，在从经典数学到直觉主义数学的转变中，人们失去了几个基本的分析定理。但事实并非如此，因为在许多情况下，直觉主义又以类似的形式重新获得了这些定理，其中存在性声明被对任意精度内的近似存在的声明所取代，就像中值定理的这种经典等价形式，在构造上是有效的：

该定理是：对于区间[a，b]上的每一个连续实值函数f，都有a＜b，并且对于f(a)和f(b)之间的每一个c，以下情况成立：∀n∃x∈[a，b]|f(x)-c|＜2⁻ⁿ。

弱反例是表明某些数学语句在直觉上不成立的一种手段，但它们还不能揭示直觉主义连续体的丰富性。只有在布劳威尔引入选择序列之后，直觉主义才获得其特殊的意味，并与经典数学不可同日而语。

选择序列（Choice sequences）

选择序列是由布劳威尔引入以捕捉连续体的直觉的。由于对直觉主义者来说，所有的无穷都是潜在的，所以无穷的对象只能通过一个逐步产生它们的过程来把握。因此，什么会被允许为合法的构造，决定了哪些无穷的对象会被接受。例如，在大多数其他形式的建构主义中，只允许生成这类对象的可计算规则，而在柏拉图主义中，无穷性被认为是完成的总体，其存在即使在不知道生成规则的情况下也被接受。

布劳威尔的直觉主义的第二行为产生了选择序列，它提供了某些无穷集合的属性，从经典的角度来看是不可接受的。选择序列是一个由自由意志创造的数字（或有限对象）的无穷序列。这个序列可以由法律或算法决定，比如只由“0”组成的序列，或由素数按递增顺序组成的序列，在这种情况下，我们说的是有法则的序列，或者它可以不受任何规则的约束，在这种情况下，它被称为无法则的。例如，无规律的序列可以通过重复投掷硬币来创造，或者通过要求创造主体逐一选择序列中的连续数字，允许它选择任何它喜欢的数字。因此，一个无规则的序列永远是未完成的，在任何时间阶段，关于它的唯一可用信息是迄今为止创建的序列的初始段。显然，根据无规则的本质，我们永远无法决定它的价值是否会与一个合法的序列相吻合。另外，自由意志能够创造出一开始是有法则的序列，但在某一点上，法则可能会被解除，自由选择的过程就会接管，产生后续的数字，或者反之亦然。

根据布劳威尔的观点，每个实数都由一个选择序列来表示，选择序列使他能够通过有争议的连续性公理来捕捉直观的连续体。布劳威尔在他的就职演说中第一次谈到了选择序列（Brouwer 1912），但当时他还没有把它们作为他的数学的一个基本部分。渐渐地，它们变得越来越重要，从1918年开始，布劳威尔开始以下一节解释的方式使用它们。

3.5 连续性公理（Continuity axioms）

接受选择序列的概念具有深远的意义。对于直觉主义者来说，它证明了连续性公理的使用，从这些公理中可以得出经典的无效语句。这些公理中最弱的是弱连续性公理：

(WC-N) ∀α∃nA(α,n)→∀α∃m∃n∀β∈α(¯¯¯¯¯m)A(β,n).

这里n和m的范围是自然数，α和β的范围是选择序列，β∈α(m)意味着α和β的前m个元素是相等的。尽管到目前为止，对于任意选择序列的大多数连续性公理从未给出过完全令人满意的理由，甚至连布劳威尔也没有，但当限制在无规律序列类时，支持弱连续性公理有效性的论据如下。当一个形式为∀α∃nA(a,n) 是由直觉主义建立的吗？根据无规律序列概念的本质，数字的选择n对其A (α , n)的有穷初始段后，必须使其成立。α的一个有穷的初始段后，才能做出判断。因为我们不知道如何α将如何进行，因此，我们必须基于以下选择 n 的初始段上。α的初始段，在我们希望固定的那个时间点上是已知的n，这意味着，对于每一个无规律的序列β的初始段都与α , A(β,n)也是成立的。

弱连续性公理已被证明是一致的，并经常以一种可以被证明的形式应用，即在谓词A只指的是α的值，而不是它可能拥有的高阶属性。这里将省略论证的细节，但它包含了与无规律序列原则的论证相同的成分，可以在van Atten和van Dalen 2002中找到。

弱连续性并没有穷尽直觉主义关于连续体的直觉，因为鉴于弱连续性公理，似乎可以合理地假设，选择使 ∀β∈α(¯¯¯¯¯m)A(β,n)的数m，可以被明确化。因此，∀α∃nA(α,n)意味着存在一个连续的函数Φ，对于每一个α产生固定α的长度的m，在此基础上选择n。更正式地说，让CF是连续函数Φ的类别，它将自然数分配给无穷序列，也就是说，它满足：

∀α∃m∀β∈α(¯¯¯¯¯m)Φ(α)=Φ(β).

连续性的完整公理，即弱连续性公理的延伸，可以表示为：

(C-N)∀α∃n一个(α,n)→∃Φ∈CF∀α一个(α,Φ(α)).

通过连续性公理，某些弱的反例可以转化为对经典公认原则的真正驳斥。例如，它意味着排中律的量化版本是错误的：

¬∀α(∀nα(n)=0).

这里α(n)表示α的第n个元素。为了说明这个否定成立，假设，通过矛盾论证，¬∀α(∀nα(n)=0∨¬∀nα(n)=0) 成立。这就意味着：

∀α∃k((∀nα(n)=0∧k=0)∨(¬∀nα(n)=0∧k=1)).

根据弱连续性公理，对于 α 只由零组成，存在一个数 m 的选择是固定的 k 的选择，这意味着对于所有 β ∈ α ( ¯¯¯¯¯ m ) , k = 0 . 但存在一些序列，其前 m 元素是0并且包含一个1的序列的存在表明，这不可能。

这个例子表明，排中律在直觉主义中不仅不成立，而且实际上是错误的，它导致了对连续体的许多基本属性的反驳。例如，考虑到实数 r α 是由数字组成的序列的极限 r n 在弱反例一节中给出，其中的 A ( m ) 定义中的A ( m ) 被认为是指 α ( m ) = 0 . 那么上面的反驳就意味着 ¬ ∀ α ( r α = 0 ∨ r α ≠ 0 ) ，因此它驳斥了三分法：

∀x(x＜y∨x=y∨y＜x).

下面的定理是连续性公理反驳某些经典原则的另一个例子：

定理 ( C - N ) 每个全实函数都是连续的。

事实上，这个定理的一个经典反例是无处连续的函数：

f(x)={0 if x is a rational number

1 if x is an irrational number

从直觉主义的角度来看，这不是一个合法的函数，因为有理的属性在实数上是不可解的。上面的定理意味着连续体是不可分解的，在van Dalen 1997年，它表明这甚至对无理数集也是成立的。

上述两个例子是连续性公理在直觉主义数学中应用方式的特点。它们是直觉主义中唯一与经典推理相矛盾的公理，因此代表了布劳威尔哲学中最丰富多彩以及最具争议性的部分。

邻域函数

有一种方便的连续函数表示法，在文献中被广泛使用，尽管不是布劳威尔本人所为。将数字分配给无限序列的连续函数可以用邻接函数表示，其中邻接函数 f 是自然数上的一个函数，满足以下两个属性( ⋅ 表示连接和 f ( α ( ¯¯¯ n ) ) 表示f的值 f 在有限序列的代码上 α ( ¯¯¯ n ) ).

α∃nf(α(¯¯¯n))＞0 ∀n∀m(f(n)＞0→f(n⋅m)=f(n)).

直观地说，如果 f 代表 Φ 则 f ( α ( ¯¯¯ n ) ) 0 意味着 α ( ¯¯¯ n ) 不够长，无法计算出 Φ ( α ) ，而 f ( α ( ¯¯¯ n ) ) m + 1 意味着 α ( ¯¯¯ n ) 是足够长的时间来计算 Φ ( α ) 的值，并认为 Φ ( α ) 是 m . 如果 K 表示邻接函数的类别，那么连续性公理 C - N 可以被改写为：

∀α∃nA(α,n)→∃f∈K∀m(f(m)＞0→∀β∈mA(β,f(m−1))),

其中 β ∈ m 表示初始段的代码为 β 是 m .

3.6 条形定理（The bar theorem）

布劳威尔引入了选择序列和连续性公理来捕捉直觉上的连续，但仅凭这些原则并不足以恢复布劳威尔认为直觉上合理的那部分传统分析，如闭区间上的每个连续实函数都是均匀连续的定理。出于这个原因，布劳威尔证明了所谓的巴氏定理。这是一个经典的有效陈述，但布劳威尔给出的证明被许多人认为根本不是证明，因为它使用了一个关于证明形式的假设，而这个假设没有提供严格的论证。这就是条形定理也被称为条形原则的原因。

条形定理最有名的结果是扇形定理，它足以证明上述关于均匀连续性的定理，我们将首先处理它。扇形定理和条形定理都允许直觉主义者沿着某些有根基的对象集合使用归纳法，这些对象被称为传播。散布是集合的直观类似物，它抓住了无限对象不断增长且永不结束的想法。散布本质上是一棵可数分支的树，用自然数或其他有限对象标记，只包含无限的路径。

扇形是一个有限分支的散布，扇形原理表达了一种紧凑性的形式，在经典上等同于柯尼希定理，其经典证明从直觉的角度看是不可接受的。该原则指出，对于每个扇形 T 中，每一个分支在某一点上都满足一个属性 A ，在满足该属性的深度上有一个统一的约束。这样的属性被称为T的条形 T。

（FAN）∀α∈T∃nA(α(¯¯¯n))→∃m∀α∈T∃n≤mA(α(¯¯¯n)).

这里 α ∈ T 表示 α 是T的一个分支 T . FAN原则足以证明上述定理：

定理（FAN） 闭区间上的每个连续实函数都是均匀连续的。

Brouwer对扇形定理的论证是他的普遍传播的条形原则：

(BI)[∀α∀n(A(α(¯¯¯n))∨¬A(α(¯¯¯n)))∧∀α∃nA(α(¯¯¯n)) ∧∀α∀n(A(α(¯¯¯n))→B(α(¯¯¯n))) ∧∀α∀n(∀mB(α(¯¯¯n)⋅m)→B(α(¯¯¯n)))]→B(ε).

这里 ε 代表空序列、·代表串联，BI代表Bar Induction，而下标D指的是谓词的可解性。A条形原则为直觉主义提供了一个树的归纳原则；它表达了一个关于可解码属性的铺展的基础性原则。这个原则的扩展，其中可解码性的要求被弱化了，可以从布劳威尔的工作中提取出来，但这里将省略。连续性和条形原则有时在一个公理中得到体现，称为条形连续性公理。

条形原则和连续性公理一节中提到的邻接函数之间有密切联系。设IK是归纳定义的邻接函数类，由所有常数非零序列λm.n+1组成，并且如果f(0)=0，并且λm.f(x⋅m)∈IK，对于所有x，那么f∈IK。语句K=IK，也就是邻接函数可以归纳生成的语句，等同于BID。

布劳威尔对条形定理的证明很了不起，因为它使用了假设证明的井然有序的特性。它是基于这样的假设：任何关于序列上的属性A是条形的证明都可以分解成一个井然有序的典范证明。尽管它在经典上是有效的，但布劳威尔对该原则的证明表明，在直觉主义中接受它为有效原则的理由与支持它在经典数学中的可接受性的论据有根本的不同。

3.7 选择公理（Choice axioms）

从建构的角度来看，选择公理的完整形式是不可接受的，至少在集合论的某些其他核心公理，比如扩展性（Diaconescu 1975）面前是如此。对于让 A 是一个不知道是真还是假的陈述。那么以下两个集合的成员资格是不可判定的。

X={x∈{0,1}∣x=0∨(x=1∧A)}

Y={y∈{0,1}∣y=1∨(y=0∧A)}

存在一个选择函数f：{X,Y}→{0,1}从X和Y中选择一个元素。X 和 Y 中选择一个元素，意味着 (A∨¬A)。因为如果f(X)≠f(Y)，就说明X≠Y，并且ence ¬ A 而 f ( X ) = f ( Y ) 意味着 A . 因此，一个选择函数为 { X , Y } 不可能存在。

然而，有一些公理的限制是直觉主义可以接受的，例如可数选择公理，也被下面要讨论的半直觉主义接受为合法原则：

（AC-N）∀R⊆N×N(∀m∃nmRn→∃α∈NN∀mmRα(m))

这个方案可以有如下的理由。对前提的证明应该提供一种方法，即给定 m 提供一个数字 n 这样 m R n . 因此，该函数 α 在自然数上的函数 N 的函数可以逐步构建：首先是一个元素 m 0 被选中，以便 0 R m 0 的值，这将是 α ( 0 ) . 那么一个元素 m 1 被选中，使得 1 R m 1 的值，这将是 α ( 1 ) ，以此类推。

其他几个选择公理也可以用类似的方式进行论证。这里只提一个，即从属选择的公理：

(DC-N) ∀R⊆N×N(∀m∃nmRn→∀k∃α∈NN(α(0)=k ∧∀i≥0α(i)Rα(i+1))).

同样在经典数学中，选择公理也被谨慎对待，而且经常明确提到在一个证明中需要多少选择。由于从属选择公理与经典集合理论中的一个重要公理（确定性公理）是一致的，而完整的选择公理则不是，所以人们特别关注这个公理，而且一般来说，如果有选择的话，人们会试图将证明中的选择量减少到从属选择。

3.8 描述性集合论、拓扑学和拓扑理论

布劳威尔并不是唯一对某些经典推理形式表示怀疑的人。这在描述性集合论中尤其明显，描述性集合论的出现是对康托尔集合论中出现的高度非结构性概念的反应。这个领域的奠基人，包括Émile Borel和Henri Lebesgue这两个主要人物，被称为半直觉主义者，他们对连续体的建设性处理导致了博莱尔层次的定义。从他们的观点来看，像所有实数集的集合这样的概念是没有意义的，因此必须用一个确实有明确描述的子集的层次结构来代替。

在Veldman 1999中，提出了Borel集概念的直觉等价物，并表明Borel集的经典等价定义会产生各种直觉上不同的类，这种情况在直觉主义中经常发生。对于直觉主义的Borel集，Borel等级定理的类似物在直觉上是有效的。对这一事实的证明基本利用了上面讨论的连续性公理，从而显示了经典数学如何指导寻找直观主义的类似物，然而，这些类似物必须以完全不同的方式来证明，有时使用从经典观点来看不可接受的原则。

另一种研究连续体或一般拓扑空间的子集的方法是通过形式或抽象拓扑学的发展出现的（Fourman 1982, Martin-Löf 1970, Sambin 1987）。在这种构造性拓扑学中，开放集和点的作用是相反的；在经典拓扑学中，开放集被定义为某个点的集合，在构造性案例中，开放集是基本概念，而点则是以它们为基础定义的。因此，这种方法有时被称为无点拓扑学。

在Brouwer之后，直觉性的函数分析被许多人发展得很远，但由于大多数方法不是严格意义上的直觉性的，也是广义上的构造性的，所以这里将不再讨论这一研究。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。