直观主义

数学哲学、逻辑学科术语

在数学哲学和逻辑中，直觉主义（英语：Intuitionism），或者新直觉主义（Neointuitionism ）（对应于前直觉主义（Preintuitionism）），是用人类的构造性思维活动进行数学研究的方法。也可翻译成直观主义。

描述

任何数学对象被视为思维构造的产物，所以一个对象的存在性等价于它的构造的可能性。这和古典的方法不同，因为根据古典方法，一个实体的存在可以通过否定它的不存在来证明。对直觉主义者来说，这是不正确的：不存在的否定不表示可能找到存在的构造证明。正因为如此，直觉主义是数学结构主义的一种；但它不是唯一的一类。

直觉主义把数学命题的正确性和它可以被证明等同起来；如果数学对象纯粹是精神上的构造，还有什么其它法则可以用作真实性的检验呢（如同直觉主义者所说的一样）？这意味着直觉主义者对一个数学命题的含义，可能与古典的数学家有不同理解。例如，说A或B，对于一个直觉主义者，是宣称A或是B可以被“证明”，而非两者之一“为真”。值得一提的是，只允许A或非A的排中律，在直觉主义逻辑中是不被允许的；因为不能假设人们总是能够证明命题A或它的否定命题。

直觉主义也拒绝承认实无穷的抽象概念；也就是说，它不把像所有自然数的集合或任意有理数的序列这样的无穷当作实体来考虑。这要求将集合论和微积分的基础分别重新构造为构造主义集合论和构造主义分析。

历史

在元理论中，一种认识论认为通过一种直观的推理可以马上知道关于道德的叙述是否正确。在17和18世纪，卡德沃斯和莫尔（1614~1687），克拉克（1675~1729）和普莱斯（1723~1729）是直观主义的维护者；在20世纪，其支持者包括普理查德（1871~1947）、穆尔和罗斯。那些可以直接理解的道德真理有各种类别，对应的直观主义也就不同。例如，穆尔认为某些事情具有道德价值这一点就是毋庸置疑的正确的，而罗斯则认为我们立即能知道的就是我们有责任去做这类事情。

由于悖论的出现，产生了数学基础论的危机，其后30年间，围绕着各种问题进行热烈的争论，出现相互对立的逻辑主义、直觉主义、形式主义三大学派。从1900年到1930年左右，数学的危机使许多数学家都卷入到一场大辩论当中。他们看到这次危机涉及数学的根本，必须对数学的哲学基础加以严密的考察。在这场大辩论中，原来的不明显的意见分歧扩展成为学派的争论，以罗素为代表的逻辑主义，以布劳威尔为代表的直觉主义，以希尔伯特为代表的形式主义三大学派应运而生。

1930年，哥德尔不完全性定理的证明暴露了各派的弱点，哲学的争论冷淡了下去。此后各派力量沿着自己的道路发展演化。特别是罗素等人企图从逻辑中推出全部数学。推导过程极为繁琐，以至花上几百页才能把数1定义出来，无怪乎法国大数学家彭加勒挖苦他们说：“这是一个可钦佩的定义，它献给从来没有听说过1的人。”从哲学上来讲，也很难在这个体系中补充直观和经验的概念，从而使数学成为“不结果实的”、纯粹形式的演绎科学。不过，罗素等人以符号形式实现逻辑数学化，从而极大地推动数理逻辑的发展，这种功绩是不可抹杀的。

直觉主义者走向另一个极端，他们否定实在的无限。克罗内克甚至否定无理数的存在，连圆周率π都认为不存在，因为从整数出发，无法造出π来。代表人物是布劳威尔。他在1907年发表《论数学基础》，正式建立起直觉主义数学。他们否定排中律，也就是认为存在着既不能证明也不能否证的命题。他们坚持所有定义和命题都必须通过构造来实现，从而根本不承认无穷集合论。虽然他们因此消除了悖论，但是也因此否定了大部分经典数学。他们把数学建立在构造的基础上，尽管他们取得相当的成就，但也无法与整个数学的大洋相提并论。反对直觉主义最有力的是希尔伯特。

希尔伯特他第一篇证明论的工作是1922年发表的，在《数学的新基础：第一篇》中，他论述如何把数论用有限方法讨论，而数学本身却一般须用超穷方法。他指出用符号逻辑方法可以把命题和证明加以形式化，而把这些形式化的公式及证明直接当做研究对象。在1922年在德国自然科学家协会莱比锡会议上，他做了《数学的逻辑基础》的演讲，更进一步提出了证明方法。要求有限主义，即经过有限步不推出矛盾来即为证明可靠，这称为希尔伯特计划。其实早先弗雷格已经坚持认为需要有明显的符号系统，明显的公理及推演规则，明显的证明。

希尔伯特定走的更远，他提出这样一种明显理论本身也做为一种数学研究的对象，且应用适当的方法来判定它是否无矛盾，这种做法一般称为元数学。希尔伯特建议两条最基本的原则：一、形式主义原则：所有符号完全看做没有意义的内容，即使将符号、公式或证明的任何有意的意义或可能的解释也不管，而只是把它们看作纯粹的形式对象，研究它们的结构性质；二、有限主义原则，即总能在有限机械步骤之内验证形式理论之内一串公式是否一个证明。应用数学方法于这样一个形式理论，避免涉及无穷的推断，这就排除了康托尔**论的方法。这个思想是只应用靠得住的方法，因为要证明数学或其一部分无矛盾的方法是大家公认可靠的，整个数学才有牢固的基础。希尔伯特认为数学的真理所在就是没有矛盾，而不在于能否构造出来。他提出的形式主义的主要论点是：数学本身是形式系统的集合，每个形式系统都包含自己的逻辑、概念、公理及推理规则；数学的任务就是发展出每一个这样的演绎系统，在每一个系统中，定理的证明通过一系列程序得到，只要这种推演过程不产生矛盾出来。为此，希尔伯特以数学的证明为研究对象，提出所谓希尔伯特纲领，成为后来证明论（元数学）的来源。在希尔伯特纲领中，希尔伯特要求无矛盾性的证明通过有限的构造步骤达到，而且力图首先在初等算术的系统中实现。但是1931年奥地利数学家哥德尔证明这个要求是达不到的。

数学分支

直觉逻辑

直觉主义逻辑或构造性逻辑是最初由阿兰德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的证实性而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有存在性质，这使它还适合其他形式的数学构造主义。

直觉类型理论

直觉类型论、或构造类型论、或Martin-Löf 类型论、或就叫类型论是基于数学构造主义的函数式编程语言、逻辑和集合论。直觉类型论由瑞典数学家和哲学家Per Martin-Löf在1972年介入。 Martin-Löf 已经多次修改了它的提议；先是非直谓性的而后是直谓性的，先是外延的而后是内涵的类型论变体。

直觉类型论基于的是命题和类型的同一: 一个命题同一于它的证明的类型。这种同一通常叫做Curry-Howard同构，它最初公式化了命题逻辑和简单类型 lambda 演算。类型论通过介入包含着值的依赖类型把这种同一扩展到谓词逻辑。类型论内在化了Brouwer、Heyting和Kolmogorov提议的叫做BHK释义的直觉逻辑释义。类型论的类型扮演了类似于集合在集合论的角色，但是在类型论中的函数总是可计算的。

其他