直觉主义逻辑的直观语义与形式语义

1. 直觉主义思想概述

20世纪初，对数学基础的研究催生了以荷兰数学家布劳威尔(L.E.J. Brouwer)为代表的直觉主义学派(intuitionist school)，其思想被称为直觉主义。(1)参见冯棉： 《经典逻辑与直觉主义逻辑》，上海： 上海人民出版社，1989年，第47页。直觉主义思想可以追溯到德国哲学家康德(I. Kant)的数学哲学立场，布劳威尔称：“在康德那里，我们发现了一种古老的直觉主义形式，也就是： 在人类推理中，时间和空间是作为固有的概念形式，这种观点在如今却几乎完全被抛弃了。对于康德来说，算术公理和几何公理是先验综合判断，也就是独立于经验的判断并且不能被分析地证明；这就解释了它们在经验世界中和抽象中都具有的绝对精确性。因此对康德来说，算术律和几何律在经验上不能被证明的这种可能性不仅仅被坚定的信念所排除，而且也是完全无法想象的。”(2)引自L.E.J. Brouwer, Intuitionism and Formalism, (1912A), in Collected Works， I, A. Heyting(ed.), Amsterdam： North-Holland, 1975, p.125。

直觉主义学派把数学理解为人类心智的创造性活动，以“存在必须被构造”作为它的座右铭，拒斥“实无穷”而采纳“潜无穷”观，并试图在其哲学立场基础上去改造经典数学。(3)参见冯棉： 《经典逻辑与直觉主义逻辑》，第47—48页。直觉主义学派对“构造”的理解体现在只接受心智可构造的数学对象和数学证明。(4)其一，可构造的数学对象指的是，对于所考虑的数学对象来说，我们的心智能够通过一定的方法能行地(有穷步)得到它们；其二，可构造的数学证明指的是，对于一个数学命题来说，我们能够能行地判定它的真。在对待逻辑和数学的关系上，直觉主义认为： 直觉是数学的基础，逻辑不是数学的基础，逻辑只是数学的一部分，逻辑有效性依赖于数学的可构造性，这也导致了经典逻辑中某些逻辑规律在直觉主义那里不是普遍有效的。(5)参见冯棉： 《经典逻辑与直觉主义逻辑》，第48页。最典型的例子便是经典逻辑中的“排中律(law of excluded middle)”在直觉主义那里不是普遍有效的(6)这里，普遍有效指的是无论在有穷论域还是无穷论域上都是有效的，直觉主义不接受无穷论域上的“排中律”，但有穷论域上的“排中律”在直觉主义那里依然是有效的。，进而经典数学中常用的间接证明方法也不能接受。(7)间接证明方法指的是用反证法证明一个肯定命题，即为了证明一个肯定命题A为真，可以通过假设“非A”为真推出矛盾，进而证明A为真。布劳威尔在论证排中律在数学中不是普遍有效的时候，提供了一种被称作“弱反例(weak counterexamples)”的方法： 如果承认了排中律普遍有效，那么就能够得到，某一尚未被证明或否证的数学陈述或者能够证明，或者能够被否证，换句话说，承认排中律普遍有效就要承认我们能够确证某一尚未被确证的数学陈述。(8)参见L.E.J. Brouwer, The Unreliablity of The Logical Principles, 1908C. in Collected Works I, A. Heyting (ed.), Amsterdam： North—Holland, 1975, pp.109-110。上述那种未被确证的数学陈述通常被称为“弱反例”，我们能够通过利用寻找“弱反例”的办法来论证经典逻辑中的某些逻辑规律不是直觉主义所普遍接受的。

2. 直觉主义逻辑的直观语义——证明解释

以下我们仅以直觉主义命题逻辑为例来阐述直觉主义逻辑的直观语义(9)参见冯棉： 《经典逻辑与直觉主义逻辑》，第48—49页。：

(1) 对于一个原子命题(不含逻辑联结词的命题)A来说，判定A为真当且仅当给出A的构造性证明。

(3) 对于合取命题A∧B来说，判定A∧B为真，当且仅当，同时给出对A的构造性证明和对B的构造性证明。

(4) 对于析取命题A∨B来说，判定A∨B为真，当且仅当，给出对A的构造性证明或对B的构造性证明；另一种更强的对析取命题的构造性解释是： 判定A∨B为真，当且仅当，可指明A,B中哪一个析取支是正确的，并且给出该析取支的构造性证明。(10)参见L. Goble(ed.), The Blackwell Guide to Philosophical Logic, Malden, Mass.: Blackwell Publishers Ltd, 2001, p.224。

(5) 对于蕴涵命题A→B来说，判定A→B为真，当且仅当，给出一个构造，这个构造使得： 从任何假设A为真的构造都能够得到对B的构造性证明。

3. 直觉主义逻辑的形式系统

在直觉主义逻辑直观语义的基础上，直觉主义逻辑形式系统从语型的视角刻画了关于逻辑联结词和量词的逻辑规律。已有的直觉主义命题逻辑的形式系统主要有三种类型： 希尔伯特式(Hilbert-style)系统(也称公理系统)、自然推理(natural deduction)系统和矢列演算(sequent calculus)。容易证明，这三种逻辑形式系统是等价的，也就是说，在同一形式语言下，三种类型的形式系统的内定理集是相同的。(11)参见冯棉： 《经典逻辑与直觉主义逻辑》，第62页；冯棉： 《结构推理》，桂林： 广西师范大学出版社，2015年，第44页。

自然推理系统能够较好地反映直觉主义构造性推理的特性。(12)参见D.M. Gabbay and F. Guenthner(eds.), Handbook of Philosophical Logic(Second Edition), Vol.5, Berlin： Springer Netherlands, 2014. p.10。基于此，我们以直觉主义命题逻辑的自然推理系统IPN为例(13)见冯棉： 《经典逻辑与直觉主义逻辑》，第51—52页。，分析直觉主义逻辑形式系统的特点。

IPN由两个部分组成： 一、形式语言；二、推理规则。

我们先给出形式语言L：

推理规则有11条：

以下，A,B,C表示任意公式；Γ, Δ, Ω是任意的由公式组成的集合(可为空集∅)；├是推演符号，Γ├A表示以Γ为前提，经过有限次使用系统的规则，得到公式A；如果∅├A(可简记为├A)，那么称A是IPN的内定理。

规则1： 如果A∈Γ，那么Γ├A。

规则2： 如果Γ├A， Δ├B，那么Γ∪Δ├(A∧B)。

规则3： 如果Γ├(A∧B)，那么Γ├A。

规则4： 如果Γ├(A∧B)，那么Γ├B。

规则5： 如果Γ├A，那么Γ├(A∨B)。

规则6： 如果Γ├A，那么Γ├(A∨B)。

规则7： 如果Γ├(A∨B)，Δ∪{A}├C，Ω∪{B}├C，那么Γ∪Δ∪Ω├C。

规则8： 如果Γ∪{A}├B，那么Γ├(A→B)。

规则9： 如果Γ├A， Δ├(A→B)，那么Γ∪Δ├B。

IPN的11条推理规则都是遵循直观语义的，我们以规则5为例做验证(其他规则的验证类似)，由于Γ├A，这意味着： 由Γ中的那些公式为前提，可以用构造性的方法推出A，根据析取命题的直观语义，由A的构造性证明可获得(A∨B)构造性证明，进而，由Γ中的那些公式出发，可以用构造性的方法推出(A∨B)，即Γ├(A∨B)成立。进而，我们可以把IPN的内定理理解为直观语义下的逻辑规律，即形如定理A的命题都被判定为真，也就是说，总能给出对它的构造性证明。

4. 直觉主义逻辑的博弈式语义

虽然直觉主义逻辑形式系统的构建是为了从语型角度来刻画证明解释下的逻辑规律，但就形式系统本身来说，它仅仅是符号的推演系统，这使得我们可以从不同的语义视角去理解它，进而对逻辑常项(logical constants)的理解也存在多种可能性。博弈式语义(game-theoretical semantics从博弈的视角去理解直觉主义逻辑的形式系统，它以对话语义(dialogue semantics)为代表，对话语义利用两个主体的博弈来给出逻辑常项(logical constants)的语义解释。

以下，我们以直觉主义命题逻辑为例来分析对话语义的特点。

我们先给出相关语型定义(16)参见W. Felscher, “Dialogues, Strategies and Intuitionistic Provability,” Annals of Pure and Applied Logic, Vol.28 (1985): 217-254, at pp.218-219。：

在语言L的基础上我们增加四个初始符号： ∧1, ∧2,P,O，并增加一个概念： 特殊符号(special symbols)，特殊符号仅可以是： ∧1, ∧2, ∨。公式和特殊符号都被称为表达式(expression)，别无其他；对于任意一个表达式e，我们可以形成两个被标记的表达式Pe(可以直观理解为： 支持e)和Oe(可以直观理解为： 反对e)。如果一个被标记的表达式是公式，那么它被称为断言(assertion)；如果一个被标记的表达式是特殊符号，那么它被称为符号攻击(symbolic attack)。X,Y作为变量X≠Y，可取P或Q。

令A,B，A1,A2为任意公式，对逻辑联结词的解释是由论证形式(argumentation form)决定的(17)参见Ibid., p.219，表述有所修改。：

(1)合取联结词∧的论证形式为： (2) 析取联结词∨的论证形式为：

断言：X(A1∧A2) 断言：X(A1∨A2)

攻击：Y∧i,i∈{1, 2} 攻击：Y∨

防守：XAi防守：XAi,i∈{1, 2}

攻击：YA攻击：YA

防守：XB防守： 无

可进一步定义“对话(dialogue)”、“D对话(D-dialogue)”和“策略(strategy)”等概念。(18)参见Ibid., pp.219-220。(对于公式A来说，如果存在对它的策略，那么我们称公式A是对话可证的。)

基于对话语义可以证明IPN的可靠性定理(soundness theorem)和完全性定理(completeness theorem)，也就是说，IPN的内定理都是对话可证的公式并且对话可证的公式都是IPN的内定理。(19)参见T. Piecha, Some Notes on Intuitionistic Logic and Dialogue Semantics, Lecture Notes, 2018, p.36。

对于任意公式A来说，由于对A的策略是有限长的并且能够有限步寻找到对A的策略，因此对话语义的构建是符合直觉主义思想的。对话语义在博弈的视角，利用“对话可证”解读了直观语义中“构造性证明”这个概念的内涵；同时，对话可证的公式从逻辑形式系统的内定理得到了刻画。在这个意义上，对话语义可以理解为一种符合直觉主义逻辑直观语义的形式语义。

5. 直觉主义逻辑的模型论式语义

模型论式语义(model-theoretical semantics)可以理解成集合-关系语义，这种语义以Kripke语义为代表。以下，我们以直觉主义命题逻辑的Kripke语义为例来分析：

定义5.1(20)参见冯棉： 《经典逻辑与直觉主义逻辑》，第70—71页。： 系统IPN(21)IPN与直觉主义命题逻辑公理系统IP是等价的(内定理集相同)，进而系统IP的Kripke模型与系统IPN的Kripke模型等价，参见冯棉： 《经典逻辑与直觉主义逻辑》，第62页。的一个Kripke模型是一有序三元组〈K,R,V〉，其中K是一非空集合，被称为结点集或时间集，R是K上的满足自反性(reflexivity)和传递性(transitivity)(22)自反性： 对于任意的x∈K， 〈x， x〉∈R(我们把〈x,x〉∈R记为xRx)；传递性： 对于任意的x,y,z∈K，如果xRy且yRz，那么xRz。的二元关系(R⊆K×K)，V是赋值函数，其定义域为F×K(F是所有公式组成的集合)，值域是{1, 0}，V满足以下五个条件(以下，A,B是任意公式，变元k∈K)：

(1)V(pi,k)=1,V(pi,k)=0，两者有且仅有一个成立，其中，i是任意正整数；此外，如果V(pi,k)=1，那么对于任意的h∈{x|kRx,x∈K}，都有V(pi,h)=1(这个条件也可以简称为命题变元的单调性条件)。

(2)V((A∧B),k)=1，当且仅当，V(A,k)=1且V(B,k)=1。

(3)V((A∨B),k)=1，当且仅当，V(A,k)=1或V(B,k)=1。

(4)V((A→B),k)=1，当且仅当，对于任意的h∈{x|kRx,x∈K}，都有V(A,h)=0或V(B,h)=1。

(5)V(A,k)=1，当且仅当，对于任意的h∈{x|kRx,x∈K}，都有V(A,h)=0。

可以证明，IPN的Kripke模型是存在的。(23)参见冯棉： 《经典逻辑与直觉主义逻辑》，第70—71页。对于任意的IPN的Kripke模型，命题变元的单调性条件可以直接扩充到公式的单调性条件，即： 令A为任意公式，变元k∈K，如果V(A,k)=1，那么对于任意的h∈{x|kRx,x∈K}，都有V(A,h)=1。(24)参见冯棉： 《经典逻辑与直觉主义逻辑》，第72—73页。

定义5.2(25)参见冯棉： 《经典逻辑与直觉主义逻辑》，第73页。： 对于任意的INP的Kripke模型〈K,R,V〉，如果对于任意k∈K，都有V(A,k)=1，那么称A是IPN有效的(也可称为Kripke有效的)，其中A是任意公式。

从代数视角来看，Kripke语义和基于伪布尔代数(26)也被称作海廷代数(Heyting algebras)。(pseudo-Boolean algebras)的代数语义是等价的： 一个公式是Kripke有效的(Kripke valid)，当且仅当，它是代数有效的(algebraically valid)。(27)参见M. Fitting, Intuitionistic Logic, Model Theory and Forcing, Amsterdam： North—Holland, 1969, p.27.

基于Kripke语义，可以证明： IPN有可靠性定理和完全性定理，也就是说： 对于任意公式A来说，A是IPN的内定理，当且仅当，A是IPN有效的。(28)参见冯棉： 《经典逻辑与直觉主义逻辑》，上海： 上海人民出版社，1989年，第83—84页。除此之外，在Kripke树模型(tree models)基础上可以证明IPN的有限模型性(finite model property)和析取性质(disjunction property)。(29)参见D. Jacquette(ed.), A Companion to Philosophical Logic, Oxford： Blackwell Publishing, 2006, p.525.

根据定义5.1, Kripke模型的构建是基于集合论框架的，是依赖于实无穷的；但直觉主义逻辑的直观语义是遵循直觉主义的哲学立场的，是拒斥实无穷的。在这个意义上，作为直觉主义逻辑形式系统的形式语义来说，Kripke语义与直觉主义逻辑的直观语义有偏离的，这是第一种偏离。

根据定义5.2，公式的IPN有效是根据赋值函数V来定义的，也就是说，公式的IPN有效是一种外延定义；而根据直觉主义逻辑的直观语义，IPN有效的公式(即IPN的内定理)被判定为真是根据构造性证明这个内涵意义来定义的。在这个意义下，Kripke语义与直观语义也是有偏离的，这是第二种偏离。

6. 进一步讨论

直觉主义逻辑的直观语义对构造性证明的内涵意义的理解可以通过对蕴含式(A→B)的解释呈现出来，比如(30)例子参见L. Goble(ed.), The Blackwell Guide to Philosophical Logic, Blackwell Publishers Ltd, 2001. p.225。：

令A为命题：π的十进制展开中出现连续20个7；

令B为命题：π的十进制展开中出现连续19个7，

就Kripke语义而言，虽然它是一种抽象的集合-关系语义，但我们可以通过对它作认识论的解释(作为人的认知过程的一种模拟)来直观理解它(31)参见冯棉： 《经典逻辑与直觉主义逻辑》，第69—70页。：

时间集K的元素被解释为“时刻(或时期)”；对于任意的k1,k2∈K，R(k1,k2)被解释为“时刻k2不先于时刻k1(R自然满足自反性和传递性)”；对于任意公式A和k∈K，V(A,k)=1被解释成“命题A在k时刻被确认为真”，相应地，V(A,k)=0被解释成“命题A在k时刻未被确认为真”，公式的单调性条件告诉我们： 一个命题在某一时刻被确认为真了，那么在以后的时刻它依然是被确认为真的，这是一种对真理积累式的认知过程。

在这种认识论解释下，我们能够更为直观地阐释直觉主义逻辑的Kripke语义与直观语义的偏离：

根据定义5.1的(4)，“命题(A→B)在时刻k被确认为真”等价于“对于时刻k及未来任意时刻h，要么命题A未被确认为真，要么命题B被确认为真”，进而，命题(A→B)在时刻k是否被确认为真就依赖于命题A,B在时刻k及未来任意时刻h上是否被确认为真的分布情况。就上面的例子来说，当我们把命题A,B放到我们的认识论解释下来看，如果B在任意时刻k被确认为真，那么根据公式的单调性条件可知： 对于时刻k及未来任意时刻h，命题B都被确认为真，进而命题(A→B)都被确认为真，也就是说，仅仅通过B在时刻k是否被确认为真就能够判断命题(A→B)在时刻k是否被确认为真，而不必诉诸于A,B的内涵意义，这就与直观语义对蕴涵的理解有偏离。

虽然存在这种偏离，但是Kripke语义的认识论解释从认识论的视角对直觉主义逻辑形式系统作了解读，丰富了对它的理解，与对话语义一起为直觉主义逻辑在其他领域中的应用开辟了道路，这也使得直觉主义逻辑可以作为桥梁让多种不同领域联系起来，促进多学科的交叉研究。

除此之外，Kripke语义为直觉主义逻辑形式系统的元逻辑研究带来了便利，比如，利用它可以证明IPN的完全性定理、有限模型性和析取性质；由于直觉主义逻辑的直观语义缺乏对相关语义概念的严格定义，因此关于直觉主义逻辑形式系统的一些好的元性质很难从中挖掘出来。

在Kripke语义基础上，利用一定的变换，可以得到直觉主义命题逻辑公理系统IP(它等价于IPN)与模态命题逻辑系统S4的联系，即： 对于任意公式A，A是IP的内定理，当且仅当，A的S4变换式是S4的内定理(32)参见冯棉： 《经典逻辑与直觉主义逻辑》，第97—101页。。与强调内涵意义的直觉主义逻辑直观语义相比，Kripke语义体现了在外延层面建立直觉主义逻辑和其他非经典逻辑之间的联系的优势。