直觉主义逻辑

非古典逻辑的一个分支，数学哲学中直觉主义流派构造数学时所用的逻辑，属于构造性逻辑，但不是直觉主义哲学的组成部分。直觉主义逻辑反映了建立直觉主义数学时所用的证明方法，也规范了直觉主义所可接受的论证方法。直觉主义流派的创始人是荷兰数学家L．E．J布劳维尔(1881～1966)，这一流派强调构造性，认为一命题为真必须证明它为真，一命题为假必须证明它为假，主张数学领域中的一切对象必须可构造才能算是存在的，数学存在等于可构造。在如此严格的要求下，排中律AvA和公式xA(x)xA(x)等在直觉主义逻辑中一般都不成立，因而也不承认数学中存在性定理的间接证明。直觉主义逻辑与古典逻辑的区别除了表现在是否拒绝排中律和双重否定律等定理外，还表现在有没有选言性和存在性。直觉主义命题逻辑具有选言性，也就是说，如果析取式BvC是它的定理，那末析取支B和C中必有一个也是它的定理。含有常项但不含有函项的直觉主义谓词逻辑则不仅具有选言性，而且还具有存在性，也就是说，如果存在式xA(x)是它的定理，那末对于某个闭项t而言A(t)亦是它的定理。两种逻辑在可判定性方面也有差异，命题部分都是可判定的，但直觉主义逻辑的一元谓词部分是不可判定的，这是跟古典逻辑中的情况不同的。此外，古典逻辑的前束范式、司寇伦范式和Herbrand定理等性质也都是直觉主义逻辑没有的。当然，两种逻辑在元逻辑性质方面也有相同的，例如完全性、紧致性和演绎定理等。

在直觉主义数学发展过程中出现了多个逻辑系统，第一个完整的直觉主义逻辑系统是布劳维尔的学生A．海廷(1898～1980)于1930年建立的。海廷的系统被公认为正确地形式化了布劳维尔的想法，也为布劳维尔本人所接受。海廷系统由下列公理模式和推理规则组成：

A→(B→A)，

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

A→(B→A∧B)，

A∧B→A，A∧B→B，

A→A∨B，B→A∨B，

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

(A→B)→((A→B)→A)，A→(A→B)，

代入；

从A和A→B可推出B，

从B→A(x)可推出B→xA(x)，

从A(x)→B可推出xA(x)→B，

后面两个推理规则中的x都不得在B中自由出现。从这系统中去掉有关量词的公理模式和推理规则，就得到海廷的命题逻辑系统。附加排中律A∨A或双重否定律A→A到海廷的系统中，就可得到古典逻辑系统。

海廷系统中的联结词、∧、∨和→都是初始概念，是相互独立的；两个量词同样是互相独立的。关于联结词和量词的意义，海廷于1931年提出了一种解释——证明解释(proof interpretation)。他的根本想法是：仅当一个命题A有证明时才承认它为真。这里的证明是指确立A的一个数学结构，而不是指形式系统中的推导。初始概念“a证明A”的具体定义如下：

a证明B∧C指：a是一个序对(b，c)使得b证明B且c证明C；

a证明B∨C指：a是一个序对(b，c)使得b是自然数，并且b=0时c证明B而b≠0时c证明C；

a证明B→C指：a是一个结构，它把B的任一个证明p转换成C的一个证明a(p)；

a证明B指：a是一个结构，它从B的任一个证明都能产生矛盾，即，a是B→(0=1)的证明。

关于量词，须假定已给定某个个体域D：

a证明xB(x)指：a是一个结构使得对各个d∈D有a(d)证明B(d)；

a证明xB(x)指：a是一个序对(b，c)使得b∈D并且c证明B(b)；d和b分别表示个体d和b的名字。利用证明解释，可以从直观上明白在直觉主义逻辑中什么是不正确的、什么是正确的。例如，排中律是不正确的；否则，从证明解释可知A∨A有一个证明a，a是一个序对(b，c)使得b是自然数，并且b=0时c证明A而b≠0时c证明A，因此，无论b是零还是非零，c不是证明A就是证明A，对于任意一个具体的命题A，要想必然产生A或A的一个证明，这当然是不可能的。

在海廷提出证明解释以后，直觉主义逻辑取得了很大进展，出现了其它一些解释。1934年，G．K．E根岑(1909～1945)建立了直觉主义逻辑的自然推理系统。这系统可以由下列规则组成：

x不在推出A(x)时所作的任 t项对A(x)中的x可代入；

一假定中出现；

y不在B中出现，也不在推出

B时所作的假定中出现。

规则中被方括号括起来的公式是由该规则消除的公式。根岑的自然推理系统远比海廷的公理化系统更精确地体现了直觉主义逻辑联结词的意旨，完成了直觉主义逻辑研究的一大突破。

有关直觉主义逻辑与其它逻辑的关系的第一批元逻辑结果出现在20世纪30年代初。K．德尔和根岑各自独立地表述了古典谓词逻辑到直觉主义谓词逻辑内的转换，哥德尔还建立了模态逻辑S4系统跟直觉主义命题逻辑之间的联系。1938年A．塔尔斯基(1902～1983)提出拓扑解释，第二次大战后S．C．克利尼(1909～ )建立了可实现性解释，1956年E．W．贝思引进了比早期拓扑解释更为直观的解释，1958年哥德尔提出了一种算法类型的解释－辩证解释(dialectica interpretation)，1963年S．克里普克(1942～ )提出可能世界解释。50年代以后，直觉主义逻辑的研究发展较快，获得了很多重要成果。70～80年代，由于发现拓扑层(sheaves)和拓扑斯(topoi)，一些逻辑学家提出了更为普遍的拓扑解释。

直觉主义逻辑在构造性数学中取得了成功的应用，这已为大部分数学家所肯定。更为重要的是，它与计算机的设计和改进有着较为密切的关系。