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

4. 建构主义（Constructivism）

直觉主义与大多数其他形式的建构主义有一个核心部分。一般来说，建构主义关注的是建构的数学对象和推理。至少在原则上，人们可以从建构性证明中提取计算元素的算法，并模拟在证明中确定存在的建构。大多数形式的建构主义都与经典数学兼容，因为它们一般都是基于对量词和连接词以及允许的结构的更严格的解释，而不做额外的假设。几乎所有建构主义团体所接受的逻辑都是一样的，即直觉主义逻辑。

经典数学中的许多存在性定理都有一个建设性的类似物，其中存在性声明被一个关于近似的声明所取代。我们在上面关于弱反例的章节中看到了一个例子，即中值定理。数学的大部分内容都可以用类似的方式建设性地恢复。之所以在此不作进一步处理，是因为本条目的重点在于直觉主义的那些方面，这些方面使它与数学的其他建构主义分支不同。对于建构主义的彻底处理，读者可以参考本百科全书中的相应条目。

5. 元数学

尽管布劳威尔以精确和基本的方式发展了他的数学，但我们今天所知的形式化只是后来由其他人进行的。事实上，根据布劳威尔的观点，数学是在内部展开的，形式化虽然不是不可接受的，但也是不必要的。在他之后的其他人则不这么认为，直觉主义数学的形式化和对其元数学特性的研究，特别是对算术和分析的研究，吸引了许多研究者。所有形式化的基础是直觉主义逻辑的形式化，这一点上面已经讲过了。

5.1 算术

由Arend Heyting制定的Heyting算术HA是自然数直觉论的形式化（Heyting 1956）。它具有与Peano算术PA相同的非逻辑公理，但它是基于直觉主义逻辑的。因此，它是对经典算术的限制，而且它是几乎所有建构数学领域中公认的自然数理论。海廷算术有许多反映其建构性的属性，例如，对直觉逻辑也适用的分离属性。HA的另一个属性是数字存在属性，这是PA所不具备的：( ¯¯¯ n 是对应于自然数的数字 n )

(NEP) HA⊢∃xA(x)⇒∃n∈NHA⊢A(¯¯¯n).

这个属性在PA中不成立，这是因为PA证明了∃x(A(x)∨∀y¬A(y))的事实。例如，考虑A(x)是公式T（e,e,x）的情况，其中T是可解的Kleene谓词，表示x是编码为e的程序在输入e上的终止计算的代码。如果每一个e都存在一个数n，使得PA⊢T(e,e,n)∨∀y¬T(e,e,y)，那么通过检查T(e,e,n)是否成立，就可以决定一个程序e在输入e上是否终止。

马尔科夫规则是一个在经典上和直觉上都成立的原则，但只有对HA来说，这个事实的证明是不难的：

(MR)HA⊢∀x(A(x)∨¬A(x))∧¬¬∃xA(x)⇒HA⊢∃xA(x)

由于HA证明了每个原始递归谓词的排除中间律，因此，对于这样的A，HA中¬¬∃xA(x)的可推导性也意味着∃xA(x)的可推导性。由此可见，PA对HA是Π02保守的。也就是说，对于原始递归的A：

PA⊢∀x∃yA(x,y)⇒HA⊢∀x∃yA(x,y).

因此，HA的可证递归函数类与PA的可证递归函数类相吻合，根据建构主义和直觉主义的基础思想，这一属性可能并不令人惊讶。

5.2 分析

直觉主义数学的形式化不仅仅包括算术。分析的很大一部分已经从构造的角度被公理化了（Kleene 1965, Troelstra 1973）。这些系统的建构性可以用函数、类型理论或可实现性解释来建立，其中大多数是基于哥德尔的辩证法解释(Gödel 1958, Kreisel 1959)、Kleene可实现性(Kleene 1965)或类型理论(Martin-Löf 1984)或其延伸。在这些解释中，构造性语句所依据的函数，例如将y分配给∀x∃yA(x,y)中的每个x的函数，以各种方式被明确化。

在(Scott 1968 and 1970)中，提出了一个二阶直觉分析理论的拓扑学模型，其中的实数被解释为从Baire空间到经典实数的连续函数。在这个模型中，克里普克的模式以及某些连续性公理是成立的。在(Moschovakis 1973)中，这种方法被改编为以选择序列的方式构造直觉分析理论的模型。在这个模型中，克里普克的模式和某些连续性公理也是成立的。在(Van Dalen 1978)中，Beth模型被用来提供一个满足选择模式、弱连续性实例和Kripke模式的算术和选择序列的模型。在这个模型中，每个节点的域都是自然数，因此人们不必像克里普克模型那样使用非标准模型。此外，创建主体的公理CS1-3可以在其中得到解释，从而表明这个理论是一致的。

5.3 无规律序列（Lawless sequences）

存在着无规律序列的公理化，它们都包含连续性公理的扩展（Kreisel 1968, Troelstra 1977）。特别是以开放数据公理的形式，说明对于 A (α) 不包含除此之外的其他非法学参数α：

A(α)→∃n∀β∈α(¯¯¯n)A(β)

在(Troelstra 1977)中，无规律序列的理论在直觉分析的背景下被发展(并被证明)。除了基本分析的公理之外，对于无规律序列，它还包含了开放数据、连续性、可决断性和密度(密度表示每个有限序列都是无规律序列的初始段)等公理的强化形式。特别有趣的是，在这些理论中，无规律序列上的量词可以被消除，这一结果也可以看作是为这类理论提供了一个有规律序列的模型。无规律序列理论的其他经典模型已经在范畴理论中以模型束的形式被构造出来（van der Hoeven and Moerdijk 1984）。在(Moschovakis 1986)中，引入了一个相对于一定的类定律元素集合的选择序列的理论，以及一个经典模型，在这个模型中，无规律序列正好是通用的。

5.4 创造主体的形式化（Formalization of the Creating Subject）

第2.2节介绍的创造主体可以产生选择序列，这是布劳威尔直觉主义中最重要和最复杂的数学实体。一些哲学家和数学家试图从数学和哲学的角度进一步发展创造主体的理论。

在创建主体概念的形式化中，它的时间方面是用符号形式化的 □ n A 表示创造主体在时间n有一个A的证明（在其他一些表述中：经历了A的真理性 A 在时间 n ). Georg Kreisel (1967)为“创造主体”引入了以下三个公理，它们一起用CS表示：

CS1：□nA∨¬□nA(在时间n，可以决定创建主体是否有A的证明。)

CS2：□mA→□m+nA(创造主体永远不会忘记它所证明的东西)

CS3：(∃n□nA→A)∧(A→¬¬∃n□nA)(创造主体只证明真实的东西，对创造主体来说，没有真实的陈述是无法证明的。)

在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 是一个函数，这就确定了在直觉主义中，并非所有函数都是可计算的。

5.5 基础（Foundations）

旨在作为建构数学基础的形式化，要么是集合论的（Aczel 1978, Myhill 1975），要么是类型论的（Martin-Löf 1984）。前者是Zermelo-Fraenkel集合理论在建构性环境中的改编，而在类型（type）论中，建构性陈述中隐含的构造在系统中被明确化了。集合理论可以被看作是数学的延伸性基础，而类型论一般是延伸性的。

近年来，出现了许多这种直观数学基础理论的部分模型，其中一些已在上文提到。特别是在拓扑理论（van Oosten 2008）中，有许多模型抓住了直觉主义的某些特征。例如，有一些拓扑，其中所有的全实函数都是连续的。诸如可实现性这样的函数解释以及类型理论中的解释也可以被看作是直觉主义数学和大多数其他构造理论的模型。

5.6 逆向数学（Reverse mathematics）

在逆向数学中，人们试图为数学定理建立证明这些定理所需的公理。在直觉逆向数学中，人们有一个类似的目的，但这是针对直觉定理而言的：在一个弱的直觉理论上工作，公理和定理是相互比较的。人们希望定理与之比较的典型公理是扇形原理和条形原理、克里普克的模式和连续性公理。

在(Veldman 2011)中，研究了扇形原理在一个叫做基本直觉数学的基本理论上的等价物。研究表明，扇形原理等同于单位区间[0,1]具有Heine-Borel属性的声明，并由此推导出许多其他等价物。在(Veldman 2009)中，扇形原理被证明也等同于Brouwer的近似定点定理。在(Lubarsky等人，2012)中，反向数学被应用于克里普克模式的一种形式，它被证明等同于某些拓扑学声明。

这样的例子还有很多，来自直觉主义的反向数学。特别是在更大的建构主义逆向数学领域，有许多这种性质的结果也与直觉主义的观点有关。

6. 哲学

布劳威尔从头开始建立他的直觉主义，并没有对直觉主义和其他现有哲学之间的关系做太多评论，但他之后的其他人做了评论。本节将讨论其中的一些联系，特别是直觉主义原则可以用其他哲学来证明的方式。

6.1 现象学

直觉主义与埃德蒙·胡塞尔（Edmund Husserl）发展的哲学之间的联系，在布劳威尔生前和几十年后都被一些作者研究过。赫尔曼·魏尔（Hermann Weyl）是最早讨论布劳威尔的思想与数学现象学观点之间关系的人之一。与布劳威尔一样，魏尔在他的《Das Kontinuum》（第二章）一书中也谈到了直观的连续体，但魏尔的概念是基于时间的（意识）现象学。Weyl后来觉得布劳威尔对实分析的发展比他自己的更忠实于直观连续体的想法（Weyl 1921），因此他把自己放在布劳威尔的一边，至少在这方面是这样的（van Atten 2002）。

Van Atten（2003, 2007）用现象学来证明选择序列作为数学对象的合理性。他(2002)对布劳威尔的选择序列的论证持批评态度，这也是在其他地方寻找哲学论证的动机。选择序列出现在贝克尔（1927）和魏尔的作品中，但它们与布劳威尔的概念不同，胡塞尔从未公开讨论过选择序列。Van Atten解释了连续体的同质性是如何解释它的不可穷尽性和非原子性的，这是布劳威尔所说的直觉连续体的两个关键属性。利用这两个基本属性存在于选择序列的定义中的事实，人们得出了对它们的现象学论证。

6.2 维特根斯坦

1928年3月10日，布劳威尔在维也纳就他的直觉主义数学基础进行了演讲。路德维希·维特根斯坦在赫伯特·费格尔的劝说下参加了那次讲座，费格尔事后写下了他在讲座后与维特根斯坦等人相处的时间：发生了一件大事。突然间，维特根斯坦开始滔滔不绝地谈论哲学——说得很详细。也许这是一个转折点，因为从那时起，1929年，当他搬到剑桥大学时，维特根斯坦又成了一个哲学家，并开始发挥巨大的影响。

还有人对布劳威尔的演讲影响了维特根斯坦的思想提出异议（Hacker 1986, Hintikka 1992, Marion 2003）。维特根斯坦在多大程度上（如果有的话）受到了布劳威尔思想的影响并不完全清楚，但他们的观点之间肯定存在着有趣的一致和分歧。Marion（2003）认为，维特根斯坦在《数学基础研究》中所描述的数学概念与布劳威尔的概念非常接近，维特根斯坦同意拒绝排中律（1929年手稿，第155-156页，载于Wittgenstein 1994），但不同意布劳威尔反对它的论点。Marion(2003)称，维特根斯坦的立场比布劳威尔的更激进，因为在前者看来，数学中排除中间律的无效性是所有数学命题（相对于经验命题而言）的一个显著特征，而不是像布劳威尔那样只是无限数学的一个特殊性。

Veldman讨论了布劳威尔和维特根斯坦之间的几个（不）一致之处，例如逻辑的危险，根据两人的观点，逻辑可能导致没有数学内容的构造。本文提出的分歧之一涉及维特根斯坦关于数学是一项共同事业的观点，这与布劳威尔的《创造主体》及其关于数学是一项无语言活动的观点形成了鲜明的对比。

6.3 达米特

英国哲学家迈克尔·达米特（1975）为直觉主义，特别是直觉主义逻辑发展了一个哲学基础。达米特明确指出，他的理论不是对布劳威尔工作的注释，而是一种可能用于（用他的话说）摒弃数学中的经典推理，而支持直觉主义推理的哲学理论。

达米特的方法始于这样一个想法，即选择一种逻辑而不是另一种逻辑，必然在于人们赋予逻辑语句的意义。在达米特使用的意义理论中，它是基于维特根斯坦关于语言的思想，特别是基于他的意义即使用的思想，一个句子的意义是由该句子的使用方式决定的。一个数学语句的意义体现在对它的使用上，而对它的理解就是对使用该语句的能力的认识。这一观点得到了我们获得数学知识的方式的支持。当我们学习一个数学概念时，我们会学习如何使用它：如何计算它、证明它或从它推断。而确定我们已经掌握了一个数学陈述的意义的唯一方法是我们对该陈述的正确使用的熟练程度。

鉴于这种对意义的看法，数学意义理论的核心概念不是柏拉图主义中的真理，而是证明；对一个数学陈述的理解在于当人们得到一个证明时，能够识别它。正如达米特所说，这导致了采用直觉主义逻辑作为数学推理的逻辑。

有趣的是，正如达米特(1975)自己所说，他的意义理论与布劳威尔关于数学是一种本质上无语言的活动的观点相去甚远。因此，至少有两条截然不同的思路导致采用直觉主义逻辑而不是经典逻辑，一条是布劳威尔发展的思路，另一条是达米特论证的思路。达米特关于直觉主义的工作已经被不同的哲学家评论过，比如Dag Prawitz (1977), Parsons (1986) 和 Richard Tieszen (1994, 2000)。

6.4 有穷主义

各种形式的有穷主义都是基于与达米特所表达的类似的观点，但其中允许用来证明数学语句的结构不仅要在原则上存在，而且要在实践中存在。根据后一个概念的精确实施，我们可以得到不同形式的有穷主义，例如亚历山大·叶赛宁·沃尔平（1970）提出的超直觉主义和克里斯平·赖特（1982）提出的严格有穷主义。

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