学生，海丁

在某种意义上，布劳威尔的学生海丁是他们两人中更有影响的一位——通过一个布劳威尔不认可甚至海丁自己也有所疑虑的成就。他发展了一套严格的直觉主义逻辑的形式化系统。这个系统有时被称作海丁谓词演算（参见，例如，Heyting 1956：第7章，或者一些当代的符号逻辑教材，如Forbes 1994：第10章）。海丁（1930）认为，从经典逻辑背后的形而上学假设——真值的实在论——来看，经典数学的语言最好被理解为（客观的）真的条件。因此，一个经典数学的语义学会描述每句句子为真或为假的条件。考虑到对二值性的拒斥（参见之前的§1），像这样的语义学对直觉主义是不合适的。取而代之的是，直觉主义的语言应该被理解为证明的条件。一个这样的语义学会描述对每一个句子什么能算作一个典范的证明。粗略地说，这里有一些句子：

一个形如“Φ且ψ”的句子的证明由Φ的一个证明和ψ的一个证明构成。

一个形如“Φ或ψ”的句子的证明由Φ的一个证明或者ψ的一个证明构成。

一个形如“如果Φ那么ψ”的句子的证明由一个能把Φ的任意证明转化为ψ的一个证明的方法构成。

一个形如“并非Φ”的句子的证明由一个把任意Φ的证明转化为一个谬论的证明的程序构成。换句话说，并非Φ的一个证明是一个不存在Φ的证明的证明。

一个形如“对所有x，Φ（x）”的句子的证明是由给定任意n造出相应的句子Φ（n）的证明的程序构成。

一个形如“存在一个x满足Φ（x）”的句子的证明由对一个项n的构造以及对相应的Φ（n）的一个证明构成。

这个系统现在被称为海丁语义学（亦参见Dummett 1977：第1章）。请注意，一个人不可能有析取式“Φ或ψ”的一个典范证明，除非他已有其中一句子句的证明。所以，一个人不可能有排中律实例“Φ或非ψ”的一个证明，除非他有Φ的一个证明或者不可能存在Φ的证明的一个证明。所以，很多排中律的实例似乎没有在这套语义学中得到合法性证明。也请注意，一个人只有给出构造那样一个x的方法，才能证明以“存在一个x”开头的句子。这是主流直觉主义主题的形式化，为所有直觉主义学派所共享。

具有讽刺意义的是，海丁这里的工作是对布劳威尔关于语言和逻辑的态度的诅咒。海丁的真正的计划可能是试图帮助他的经典数学的同事们，至少为他们提供一种直觉主义数学的语言附属物的概况。海丁同意布劳威尔关于宣扬精神构造而贬低语言和逻辑的观点。在《数学的直觉主义基础》（The Intuitionist Foundation of Mathematiss，1931：53）中，他写道，“语言的伴随物不是数学的代表物，更不用说是数学本身了”。在《直觉主义》（Intuitionism，1956：5）一书中，他采纳布劳威尔的声明，认为语言是交流真实的数学构造的不完美的媒介。形式系统自身是一个合法的数学构造，但“人们永远不能保证形式系统完整地表达了任何数学思想的领域；在任何时刻，对推理新方法的发现都可能迫使我们去扩展形式系统”。海丁声称，是“逻辑依赖于数学”，而不是什么其他的方式。所以他并不指望用他在逻辑中的工作来系统整理直觉主义推理。没有办法能做到这点。

就算是这样，海丁的形式化工作使得直觉主义（以及构造主义）数学可以在普通证明论的视野下被研究，而现在关于直觉主义的算术、分析和集合论等的形式化版本都已经有了大量的文献。许多（但并不是所有）关于直觉主义逻辑的元理论研究都引用了经典的元理论。也就是说，典型证明论学者运用经典逻辑来研究的系统，其本身就是运用直觉主义逻辑的形式系统。至少从经典数学家的观点来看，一个不朽的贡献是对排中律在数学实践中的作用的详细研究。我们现在知道了直觉主义数学与经典数学之间有多么不同——假设（与布劳威尔和海丁的观点不同）直觉主义形式系统确实刻画了直觉主义数学。这一点对毕晓普的构造主义同样适用（参见注释[6]）。这一元数学的工作还引起了关于直觉主义数学在多大程度上适合于科学的需要的激烈辩论^[7]。

海丁的哲学著作重复了布劳威尔的主题，即数学是依赖心灵的以及对数学构造的关注：

直觉主义数学家提出把数学当作他的智能的天然功能，当作自由的、充满活力的思维活动来做。对他来说，数学是人类心灵的产物……我们不把一个独立于我们思维的存在性，即一个超越的存在性归于……数学对象……数学对象根据它们的本质就是依赖于人类思维的。它们的存在只是在它们能被思维认定的范围内得到保证。它们具有的性质只是在这些性质能被思维认识到对它们成立的范围内而言……对超越的存在的信仰作为一种数学证明的方法必须被拒斥……这就是质疑排中律的理由。（Heyting 1931：52—3）

与他的老师一样，海丁认为，经典数学依赖于下述“形而上学”原则：数学的对象独立于数学家而存在并且数学真是客观的和永恒的。他承认，一个数学家在他的闲暇时间里可以自由地赞同或反对这类形而上学原则。然而，唯一避免“形而上学难题困局”的方法是“把它们从数学中排除”（Heyting 1956：3）。海丁谴责经典数学家通过排中律把形而上学的论证牵扯进来。

如果“存在”的意思不是“被构造”，它就必须有其他的形而上学意义。调查这个意思或判定这是否合理不可能是数学的任务。我们并不反对数学家私下里接纳任何他喜欢的形而上学意义，但布劳威尔的方案需要我们把数学作为比形而上学更简单、更直接的东西来学习。在对精神的数学构造的学习中，“存在”必须与“被构造”同义。（Heyting 1956：2）

简单地说，海丁坚持，数学实践不应该依赖于形而上学^[8]。

在一些地方，他似乎超出了心灵依赖说，甚至声称数学是经验的：

一个数学命题表达一个特定的期望。例如，命题“欧拉（Euler）常数C是有理数”表达了下述期望，我们可以找到两个整数a和b，使得C＝a/b……对一个命题的肯定意味着一个意图得到满足。例如，断言“C是有理数”就意味着一个人确实找到了需要的整数……对一个命题的肯定自身不是一个命题；它是对一个经验事实（即该命题所表达的意图被满足）的断定。（Heyting 1931：59）

直觉主义数学建立在精神构造之上；一条数学定理表达了一个纯粹经验的事实，即某个特定构造的成功。“2＋2＝3＋1”必须被读作下述陈述的简写：“我已经实现了由‘2＋2’和‘3＋1’所指示的精神构造，并且我发现它们导致一个相同的结果”……关于这些构造所做的陈述……表达纯粹经验的结论。（Heyting 1956：8）

然而，我的建议是，像这样的陈述不应该太按照字面来理解。海丁不是在主张一种像密尔那样的经验主义（参见前面的第4章，第3节）。假设某人做了一个关于人类求和的研究。如果“2＋2”和“3＋1”被替换为一些七位自然数，该经验结论肯定会与数学结论不同。毕竟人类确实是会犯错的。当然，海丁会认为经验材料与数学是不相干的。类似地，直觉主义者会接受这样的定理“或者21 001＋1是质数或者21 001＋1是可分解的”，尽管这个事实（如果有的话）的大小会使真正的经验实现十分困难。

在这里的研究之前，我们已经数次遇到过类似的理想化。我以为，理想化使各派都很难声称他们的观点是形而上学中立的。在数学哲学中，形而上学恰恰是无法回避的——尽管一个人可以质疑形而上学与数学实践的相关性（参见第1章，第2节）。布劳威尔自己的康德式立场就不是形而上学中立的。他表达了关于数学本质及其实体的明确观点。人们可能会想，最好的达到中立性的方法是排除布劳威尔的自由选择序列而维持在类似毕晓普的构造主义那样的东西下。海丁（1931：57）承认，如果自由选择序列被丢弃，那么直觉主义数学将是无力的。而如果没有排中律，经典数学也将是无力的。

海丁早期的论文（1931）反映了布劳威尔的主张，经典数学是有缺陷的而应该被直觉主义所取代：“直觉主义是构造数学的唯一可能的道路”。然而，他的专著（1956）更为折中，认为直觉主义数学理应有一个与经典数学“并列的”位置。海丁写道，直觉主义不要求对数学的“垄断”，只要经典数学家“承认”直觉主义观念的“正当性”就满足了。这是很好的妥协。然而，海丁仍然怀疑那个想象中的在经典数学之下的“形而上学”假设。