直觉主义认知逻辑与不同程度的真

程华清

1 引言

对邱奇-费奇悖论1邱奇-费奇悖论指的是：在“任意命题的真都可能被知道”和“存在不知道的真命题”的前提下，通过经典的模态和认知逻辑推演会导致结论“任意命题的真都被知道”，这违背了我们的直觉。（Church-Fitch paradox）的解悖促进了直觉主义认知逻辑的研究。直觉主义认知逻辑是基于直觉主义逻辑的认知扩充，直觉主义逻辑的构建遵循Brouwer-Heyting-Kolmogrov 解释2简称BHK 解释。BHK 解释是从构造性语境下对逻辑算子的解释，关于BHK 解释的详细阐释见本文第二节。，这意味着直觉主义逻辑包含认知因素3直觉主义把数学理解为心智的构造性活动，这可被视作一种认知活动，直觉主义逻辑是直觉主义数学的衍生品，更多阐释详见文中第二节内容。，但其形式语言中不含认知算子，而直觉主义认知逻辑的形式语言能够表达含有认知算子K的公式KA，对认知算子的不同理解形成了不同的直觉主义认知逻辑。

直觉主义认知逻辑的研究当前可分为两条进路：

(1) 接纳知识的事实性（factivity of knowledge）原则KA →A，它也被称为反射（reflection）原则。这方面的代表是[9]中所构建的系统IKT*，构建IKT*不依赖于BHK 解释，而是基于以下观点：

真在于证实（verification）的可能性，其中“证实”被理解为实时（real time）呈现给一个真实主体（real subject）的事物，但真仅仅需要这样事物的可能性而不是其实际的出现。（[9]，第63 页）

(2) 接纳真的构造性（constructivity of truth）原则A →KA，它也被称为余反射（coreflection）原则。这方面的代表是[1]中所构建的系统IEL，对IEL 的构建旨在遵循BHK 解释，并持有观点：

直觉主义认知状态（信念或知识）是证实的结果，其中“证实”指的是足以达到实际目的而给出的确凿的（conclusive）证据（evidence）。4这种对“证实”的理解与[9]中所理解的“证实”稍有不同，参见[1]中第288 页的注释30。（[1]，第269 页）

由此可见，[1]试图从直觉主义原初立场出发来建立关于直觉主义知识的逻辑，这是[9]未考虑的。如[1]中所述：

因此威廉姆森（Williamson）的直觉主义认知逻辑没有表达基于BHK的知识（BHK-based knowledge）的含义（而这是我们的目标），与此同时它也把经典的认知假设引入到直觉主义的语境中来。（[1]，第288 页）

S.Artemov 将命题KA解读为“A是直觉主义知识”，并借助“证实”的概念给出认知算子K 的预期理解。（[1]）IEL 接受直觉主义反射（intuitionistic reflection）原则KA →¬¬A，它被视作直觉主义知识的真值条件（truth condition）。

Artemov 的工作具有启发性，它为回到直觉主义本身来发展（模态）认知逻辑提供了基本思路（比如[7]对IEL 做了一般化的研究，证明了IEL 能够嵌入到其S5 类型系统中），进而促进了直觉主义认识论（intuitionistic epistemology）的研究。遗憾的是，IEL 的预期解释并未严格遵循BHK 解释，导致IEL 的构建未达到预期目标，本文第二节会对此作详细的论证。第三节简要回顾IEL 的形式化工作，并在第二节讨论基础上重新理解IEL。第四节提出了KA的新解读，并由此引出直觉主义真和经典真之间不同程度的真，在此基础上重新理解IEL 系统的一些重要内定理。最后在第五节提出IEL 系统对应问题的一个猜测。

2 IEL 的预期解释与BHK 解释的偏离

IEL 的构建试图遵循BHK 解释，但这种尝试有一定局限性，本节从直觉主义视角下逻辑和数学的关系出发来论证：IEL 的预期解释偏离了BHK 解释，进而IEL 并未达到预期构建目标。

BHK 解释是直觉主义对基本逻辑联结词和量词的标准解释，它经由布劳威尔（L.E.J.Brouwer）、海廷（A.Heyting）和柯尔莫哥洛夫（A.Kolmogorov）发展而来。基本逻辑联结词的BHK 解释如下所述（[8]，第9 页）：

(H1)A ∧B的一个证明（proof）通过呈现A的一个证明和B的一个证明而得到。

(H2)A ∨B的一个证明通过呈现A的一个证明或B的一个证明而得到，此外规定：所呈现的证明就作为A ∨B的证明。

(H3)A →B的一个证明是一个构造（construction），这个构造使得我们能够从A的任意证明转换为B的一个证明。

(H4) 荒谬（absurdity）⊥（矛盾）没有证明。¬A的一个证明是一个构造，这个构造将A的任意假设的证明转换为矛盾的一个证明。

不难发现，BHK 解释规定了一个复合命题的证明是以何种方式从它的子命题的证明而获得，不过其核心在于对证明和构造的理解，如[8]中所言：

BHK 解释自身没有解释力（explanatory power）：一个有效的经典逻辑模式被视作构造地不可接受的，这完全取决于对“构造”“函数”“运算”的解释。（[8]，第33 页）

在BHK 解释中，证明和构造指的都是心智的构造5可称其为构造性证明，它可被理解为直观的能行（effective）方法。（mental constructions，[6]，第87 页）。这种对证明和构造的理解基于直觉主义对数学以及数学和逻辑关系的独特理解：

（一）直觉主义把数学理解为心智的构造性活动，这意味着直觉主义只接受心智可构造的数学对象和心智可构造的数学证明，即：数学对象能够通过直观能行的方法得到，数学命题所表达的内容能够通过直观能行的方法直接验证。数学定理表达的是纯粹经验的事实，数学不能建立在公理化基础之上，直觉（intuition）就是数学可靠性的基础。直觉主义数学的代表是选择序列（choice sequences）理论，利用选择序列能够遵循直觉主义思想构造连续统（continuum），形象地说，可以利用选择序列把连续统“算术化”，进而发展直觉主义分析学。

（二）数学不依赖于语言，语言仅仅是记录数学构造的工具，逻辑是利用语言记录数学构造所产生的形式规律，它的有效性自然依赖于数学的构造性。逻辑可以看作是数学的应用，如[6]所述：

逻辑可被视作语言学的一部分或者关于世界的哲学理论，在这两种理解下它都属于应用数学。仅仅第三种解释处于纯数学讨论范围内。逻辑定理是数学定理。逻辑不是数学的基础，恰恰相反，在概念上它是数学的复杂而精细的部分。（[6]，第86-87 页）

综上所述，对构造性证明的要求是BHK 解释的核心，这是由直觉主义逻辑依赖于直觉主义数学所决定的。

由于对数学的理解不同，导致直觉主义意义上的“真”有别于经典意义上的“真”。经典意义下，一个命题的真独立于对它的证明；但是在直觉主义看来，一个数学命题被判定为直觉主义真就意味着这个命题获得构造性证明。

例1.简单命题“1+12”被判定为直觉主义真，其构造性证明为：我们的心智先构造出一个自然数1，接着再构造出一个自然数1，之后把这整个过程与对自然数2 的构造作比较，能够得出两者是一样的。

例2.蕴涵命题“如果π的十进制展开中出现连续20 个7，那么π的十进制展开中会出现连续19 个7”被判定为直觉主义真，其构造性证明为：假设a是“π的十进制展开中出现连续20 个7”的任意构造性证明，显然能够给出一个构造使得从a得到“π的十进制展开中出现连续19 个7”的构造性证明。（[5]，第225 页）

基于“直觉主义知识是证实的结果”和基本逻辑联结词的BHK 解释，[1]在构建IEL 时通过“证实”概念定义了“命题KA的证明”：KA的一个证明指的是证实“A有证明”的确凿证据，其中对“A有证明”的证实无需包含A的证明。6比如基于零知识协议的证实便是这类证实：零知识协议是一类密码协议，通常是概率性的，证明者利用这种协议能够使得验证者确信一个给定命题为真，而无需提供任何额外有用的信息。在此基础上，反射原则KA →A不被IEL 接受。（[1]，第273-274 页）（[1]，第270 页）这个定义是有缺陷的：根据前面的阐释，对构造性证明的要求是BHK 解释的核心，而命题KA的证明并没有对构造性证明的要求，这偏离了BHK解释的初衷。从另一角度来说，直觉主义数学的数学对象都是从自然数出发而构造性得到的（[10]，第47-48 页），直觉主义数学命题是关于直觉主义数学对象的命题，直觉主义逻辑依赖于直觉主义数学，上述对“命题KA的证明”的定义超出了直觉主义数学的考虑范围，无法严格遵循BHK 解释。尽管[1]中对此作了一定辩护：

反对的要点在于BHK 解释不能容纳非数学命题。然而这很清楚是错误的，因为在BHK 解释的表述中没有特别数学化的东西，它并未提到数、函数、集合、范畴、类型等等。（[1]，第290 页）

但这段辩护并不成立，因为它把BHK 解释独立于直觉主义数学来看待，并未抓住“直觉主义逻辑依赖于直觉主义数学”这点。

Artemov 在构建IEL 时主张“直觉主义真蕴涵直觉主义知识”：从BHK 解释出发，命题A是直觉主义真意味着A获得证明，证明是一种证实，由于直觉主义知识是证实的结果，因此直觉主义真蕴涵直觉主义知识，进而余反射原则A →KA被IEL 接受。（[1]，第266-267 页）但是IEL 所接受的余反射原则A →KA仅仅适用于A是数学命题的情况：当A是数学命题时，A中不含认知算子K，对于任意假设的A的证明p，由于证明是最严格意义上的证实，因此p可以作为确凿的证据证实“A有证明”，进而KA获得证明；（[1]，第271 页）当A中包含认知算子K时（不妨令A为KB），A的真仅仅意味着对A的证实，并未体现对构造性证明的要求（构造性证明一定是证实，而证实不一定是构造性证明），这时“命题A为真”要弱于“A是直觉主义真”。同样的道理，对于IEL 所接受的直觉主义反射原则KA →¬¬A来说，它也仅仅适用于A是数学命题的情况。

当A是不含认知算子K的公式时，余反射原则和直觉主义反射原则可以分别解读为“直觉主义真蕴涵直觉主义知识”以及“直觉主义知识蕴涵经典真”，可合并简记为“直觉主义真直觉主义知识经典真”。（[1]，第268 页）此时可以对A作BHK 解释，但是BHK 解释无法扩展到含有认知算子K的公式上，因为一旦把BHK 解释扩展到认知算子K上，那么就没办法保证对构造性证明的要求。

综上所述，IEL 的预期解释偏离了BHK 解释，进而构建IEL 的预期目标并未达到。

3 IEL 的形式化工作

本节简要回顾IEL 的形式化工作，并在第二节的讨论基础上重新理解IEL。

令LK为IEL 的形式语言，LK的初始符号由以下部分构成：

• 命题变元：p1,p2,p3,...；

• 逻辑联结词：否定词¬、合取词∧、析取词∨和蕴含词→；

• 认知算子K；

• 左、右括号：(和)。

初始符号中的四个逻辑联结词是相互独立的，公式的递归定义遵循认知逻辑的一般定义方式，在公式省略括号时，逻辑联结词以及认知算子的联结强度遵循认知逻辑通常的约定。

对IEL 的构建可采用[2]中使用的直觉主义命题逻辑公理系统（记为IPC）为基础（[2]，第219-220 页），在LK语言下对IPC 做认知扩充。在LK语言下，IEL通过在IPC 基础上添加如下三条认知公理模式而得到（[1]，第276 页）：

• 分配（distribution）公理模式：K(A →B)→(KA →KB)

• 余反射公理模式：A →KA

• 直觉主义反射公理模式：KA →¬¬A

值得一提的是，[2]对正规（normal）直觉主义模态逻辑的模型论研究为直觉主义认知逻辑的模型论研究奠定了技术性基础。[2]对含有模态算子□的正规直觉主义模态命题逻辑系统HK□做了研究，给出了相应的克里普克语义，并保持了直觉主义命题逻辑的基本模型论性质。

在HK□的克里普克语义中（[2]，第222 页），H□框架（frame）是三元有序组〈W,RI,RM〉，其中W是非空集合，RI是W上满足自反性和传递性的二元关系，RM是W上的另一个二元关系，RM和RI要满足条件：RIRM ⊆RMRI（RIRM表示集合{〈x,y〉 |存在z，使得xRIz并且zRMy，x,y,z ∈W}，集合RMRI的定义类同）。

单调性（monotonicity）作为直觉主义逻辑的重要模型论性质，不仅在H□框架下的模型依旧保持着，而且[2]中证明了：RM和RI满足条件RIRM ⊆RMRI是H□框架下的模型满足单调性的充分必要条件（[2]，第223 页），这个结论为构造不同的直觉主义认知逻辑形式系统的克里普克语义提供了帮助。

Artemov 中构造了IEL 的克里普克语义并给出了IEL 模型的认识论解释（[1]，第279-280 页）：

（一）首先，IEL 模型指的是四元有序组〈W,R,E,V〉，其中〈W,R,V〉是IPC的克里普克模型，即：〈W,R〉是非空偏序（partial order），W被称为结点集，其中的元素被称为结点，W上的二元关系R被称为W 上的“认知”关系，⊩是命题变元在W上的满足单调性的赋值（evaluation）7对于任意结点w 和任意命题变元p 来说，w ⊩p 也被称为“w 力迫（forces）p”。。其次，W上的二元关系E被称为W上的“知识”关系，E满足：(1)对于任意的结点u，E(u)⊆R(u)成立8E(x)表示{x | wEx,x ∈W}，R(x)表示{x | wRx,x ∈W}。；(2) 如果结点u和v满足关系uRv，那么E(v)⊆E(u) 成立；(3) 对任意的结点u，E(u)。最后，将赋值⊩从命题变元（以递归定义的方式）扩展到合取式A ∧B、析取式A ∨B、蕴涵式A →B、否定式¬A和认知公式KA上，其中对KA的扩展定义为：令u是任意的结点，u⊩A当且仅当对于任意的v ∈E(u)都有v⊩A成立。

在直觉主义命题逻辑克里普克模型的认识论解释9直觉主义命题逻辑克里普克模型的认识论解释参见[10]中第69-70 页。基础上，IEL 模型的认识论解释为：W和R分别被理解为时间点组成的集合以及时间点的先后关系，对任意时间点w和v，wRv意为v不先于w。对任意时间点u，E(u)被理解为u 的“检查”（audit）集（其中的元素可被称为“检查点”）：在“检查”集的每个检查点对命题A的证实都可能发生。E满足的条件(1)被理解为：每个时间点u的检查点v都不先于u，这意味着每个时间点的检查点都只能是该时间点或该时间点之后的时间点。E满足的条件(2)被理解为：对每个不先于时间点u的时间点v来说，v的检查点都是u的检查点，这意味着随着时间的流逝，每个时间点的检查点数是不会增加的。E满足的条件(3)被理解为：每个时间点u都有检查点。最后，KA的赋值扩展定义被理解为：在时间点u确认KA为真（确认A是直觉主义知识）当且仅当在u的“检查”集中的每个检查点都确认命题A为真。

（二）“IEL 有效”的概念被定义为：令A是任意的LK公式，对任意的IEL模型M来说，如果对于任意的结点w，都有w⊩A，那么称A是模型M有效的；如果对任意的IEL 模型M都有：A是模型M有效的，那么称A是IEL 有效的。

由于R是偏序关系，因此它自然满足自反性和传递性，以下证明：E和R满足条件RE ⊆ER，进而可知：若将IEL 模型中的K替换为□，并将R、E分别替换为RI、RM，就成了一个H□模型。

E和R满足条件RE ⊆ER的证明：对任意的结点w和v，假设wREv成立，那么存在结点t使得wRt并且tEv。根据E满足的条件(2)可知：由wRt成立和tEv成立可得wEv成立。再根据R的自反性可知vRv成立，进而wERv成立。

在IEL 的克里普克语义基础上，直觉主义命题逻辑的基本模型论性质单调性、可靠性、完全性和析取性质（disjunction property）在IEL 中依然保持着。（[1]，第280-281、283 页）

IEL 有如下一些重要内定理，其中A是任意的LK公式，比如（[1]，第276-277、第282 页）：

• 定理一“知识的真值条件”¬K(A ∧¬A)

• 定理二“知识的真值条件”¬(KA ∧¬A)

• 定理三“知识的真值条件”¬A →¬KA

• 定理四K¬A →¬A

另外，利用IEL 模型能够证明：K(A ∨B)→(KA ∨KB)和KA →A都不是IEL 的内定理。（[1]，第281-282 页）

根据第二节的讨论，在BHK 解释基础上，IEL 预期解释中的“命题KA的证明”定义需要修改为：当A是数学命题时，KA的一个“证明”指的是证实“A有构造性证明”的确凿证据，其中对“A有构造性证明”的证实无需包含A的构造性证明，进而KA被判定为真意味着“A是直觉主义真”获得证实。尽管IEL预期解释借助了BHK 解释的框架，由于KA的“证明”没有对构造性证明的要求，因此只有不含认知算子K的IEL 公式才能在直观上遵循BHK 解释；此外有些IEL 公式也无法遵循IEL 的预期解释，比如KKp1→KKKp1。把IEL 系统三个公理模式以及定理一到定理四中的公式A和B都限定在不含认知算子K的情况时，它们在IEL 的预期解释下普遍成立。IEL 系统形式语义的建立能够帮助证明一些公式不是IEL 系统的内定理，比如K(A ∨B)→(KA ∨KB)和KA →A；当其中的A和B不含认知算子K时，它们在IEL 的预期解释下不是普遍成立的。

4 KA 的新解读及不同程度的真

在IEL 的预期解释中，当A是不含认知算子K的数学命题时，除了可以把KA解读为“A是直觉主义知识”或“直觉主义知识A获得证实”以外，还可以将其理解为“知道‘A是直觉主义真（A获得构造性证明）或A是经典真’”，其中联结“A是直觉主义真”和“A是经典真”的析取词“或”是经典意义下的析取10这个析取是元语言，而非IEL 的形式语言。。值得注意的是，这种新解读已经不再坚持直觉主义立场了。

在这样的解读下，“KA为真”（即“‘知道A’为真”）也是一种介于直觉主义真和经典真之间的真，并且联系了直觉主义真和经典真，即满足如下关系：

A是直觉主义真知道“A是直觉主义真或A是经典真”（后面对KA的这种解读中，引号将省略）。A是经典真。

详细来说，如果A是直觉主义真，那么意味着A获得了构造性证明，由A的构造性证明可以知道A是直觉主义真，进而知道A是直觉主义真或A是经典真；如果知道A是直觉主义真或A是经典真，那么一定知道A是经典真（A是直觉主义真A是经典真），因此A是经典真（如果A为假，那么就不可能知道A为真）。上述关系进一步可以扩展为：

A是直觉主义真知道A是直觉主义真知道A是直觉主义真或A是经典真知道A是经典真A是经典真。

再反过来考虑上述关系，不难发现，如果A是经典真，那么不一定知道A是经典真；如果知道A是经典真，那么一定知道A是直觉主义真或A是经典真；如果知道A是直觉主义真或A是经典真，那么不一定知道A是直觉主义真；如果知道A是直觉主义真，那么A是直觉主义真。最后产生如下关系：

A是直觉主义真⇐⇒知道A是直觉主义真知道A是直觉主义真或A是经典真⇐⇒知道A是经典真A是经典真。从上述关系可知，在经典视角下，直觉主义真和经典真之间产生了三种不同程度的真：

强“A是直觉主义真”“知道A是直觉主义真”

中“知道A是直觉主义真或A是经典真”“知道A是经典真”

弱“A是经典真”

当KA被解读为“知道A是直觉主义真”时，根据上述关系，直觉主义知识坍塌为直觉主义真。以下我们仅考虑在KA被解读为“知道A是直觉主义真或A是经典真”和“知道A是经典真”时，如何重新理解IEL 系统的一些重要内定理。需要注意的是，以下公式A和B都不含认知算子，它们被理解为任意的数学命题，并遵循BHK 解释。

4.1 KA 被解读为“知道A 是直觉主义真或A 是经典真”的情况

“余反射公理模式”A →KA被解读为：如果A是直觉主义真，那么知道A是直觉主义真或A是经典真。其中联结A和KA的蕴涵词是经典蕴涵。根据不同程度真的关系，A →KA在这种解读下是普遍成立的。

“直觉主义反射公理模式”KA →¬¬A被解读为：如果知道A是直觉主义真或A是经典真，那么A不可能没有构造性证明。其中联结KA和¬¬A的蕴涵词是经典蕴涵。KA →¬¬A在这种解读下是普遍成立的：假设知道A是直觉主义真或A是经典真，那么A是经典真，进而A可能有构造性证明，A没有构造性证明就是不可能的。

“分配公理模式”K(A →B)→(KA →KB)被解读为：如果知道A →B是直觉主义真或A →B是经典真，那么若知道A是直觉主义真或A是经典真，则知道B是直觉主义真或B是经典真。其中联结K(A →B)和(KA →KB)的蕴涵词以及联结KA和KB的蕴含词都是经典蕴涵。K(A →B)→(KA →KB)在这种解读下是普遍成立的：假设知道A →B是直觉主义真或A →B是经典真，那么知道A →B是经典真；再假设知道A是直觉主义真或A是经典真，同理得到知道A是经典真，进而知道B是经典真，因此知道B是直觉主义真或B是经典真。

“知识的真值条件”¬K(A ∧¬A)被解读为：不知道矛盾是直觉主义真或矛盾是经典真。其中联结K(A∧¬A)的否定词是经典否定。在这种解读下¬K(A∧¬A)是普遍成立的：假设知道矛盾是直觉主义或矛盾是经典真，那么矛盾就是经典真，而矛盾恒假，所以假设不成立。

“知识的真值条件”¬(KA ∧¬A)被解读为：并非不仅知道A是直觉主义真或A是经典真，而且¬A是直觉主义真。其中联结(KA ∧¬A)的否定词是经典否定，联结KA和¬A的合取词是经典合取。在这种解读下¬(KA ∧¬A)是普遍成立的：假设知道A是直觉主义真或A是经典真，而且¬A是直觉主义真，那么A是经典真，进而A可能有构造性证明，同时A没有构造性证明，所以假设不成立。

“知识的真值条件”¬A →¬KA被解读为：如果A没有构造性证明，那么不知道A是直觉主义真或A是经典真。其中联结¬A和¬KA的蕴涵词是经典蕴涵，联结KA的否定词是经典否定。在这种解读下¬A →¬KA是普遍成立的：假设A没有构造性证明，如果知道A是直觉主义真或A是经典真，那么A就是经典真，进而A可能有构造性证明，因此不知道A是直觉主义真或A是经典真。

定理四K¬A →¬A被解读为：如果知道¬A是直觉主义真或¬A是经典真，那么A没有构造性证明。其中联结K¬A和¬A的蕴涵词是经典蕴涵。在这种解读下K¬A →¬A是普遍成立的：假设知道¬A是直觉主义真或¬A是经典真，那么A没有构造性证明或A为假，进而A没有构造性证明。

最后考察对K(A ∨B)→(KA ∨KB)和KA →A的理解。

K(A ∨B)→(KA ∨KB)被解读为：如果知道A ∨B是直觉主义真或A ∨B是经典真，那么要么知道A是直觉主义真或A是经典真，要么知道B是直觉主义真或B是经典真。其中联结K(A ∨B)和(KA ∨KB)的蕴涵词是经典蕴涵，联结KA和KB的析取词是经典析取。在这种解读下K(A ∨B)→(KA ∨KB)不是普遍成立的：令A是黎曼猜想（Riemann hypothesis），B为¬A，即可得到反例。

KA →A被解读为：如果知道A是直觉主义真或A是经典真，那么A就是直觉主义真。其中联结KA和A的蕴涵词是经典蕴涵。在这种解读下KA →A不是普遍成立的：令A是关于正整数的命题“如果m和n是任意正整数，那么存在正整数k使得k×m ≥n”11这个命题也被称为正整数的阿基米德性质（Archimedean property）。，使用正整数的最小自然数原理，通过反证法可以证明A成立（A是经典真），进而知道A是经典真，因此也知道A是直觉主义真或A是经典真，但是并未给出A的构造性证明。

4.2 KA 被解读为“知道A 是经典真”的情况

“余反射公理模式”A →KA被解读为：如果A是直觉主义真，那么知道A是经典真。其中联结A和KA的蕴涵词是经典蕴涵。根据不同程度真的关系，A →KA在这种解读下是普遍成立的。

“直觉主义反射公理模式”KA →¬¬A被解读为：如果知道A是经典真，那么A不可能没有构造性证明。其中联结KA和¬¬A的蕴涵词是经典蕴涵。KA →¬¬A在这种解读下是普遍成立的：假设知道A是经典真，那么A是经典真，进而A可能有构造性证明，A没有构造性证明就是不可能的。

“分配公理模式”K(A →B)→(KA →KB)被解读为：如果知道A →B是经典真，那么若知道A是经典真，则知道B是经典真。其中联结K(A →B)和(KA →KB)的蕴涵词以及联结KA和KB的蕴含词都是经典蕴涵。容易证明K(A →B)→(KA →KB)在这种解读下是普遍成立的。

“知识的真值条件”¬K(A ∧¬A)被解读为：不知道矛盾是经典真。其中联结K(A ∧¬A)的否定词是经典否定。容易证明在这种解读下¬K(A ∧¬A)是普遍成立的。

“知识的真值条件”¬(KA ∧¬A)被解读为：并非不仅知道A是经典真，而且¬A是直觉主义真。其中联结(KA ∧¬A)的否定词是经典否定，联结KA和¬A的合取词是经典合取。在这种解读下¬(KA ∧¬A)是普遍成立的：假设知道A是经典真，而且¬A是直觉主义真，那么A可能有构造性证明，同时A没有构造性证明，所以假设不成立。

“知识的真值条件”¬A →¬KA被解读为：如果A没有构造性证明，那么不知道A是经典真。其中联结¬A和¬KA的蕴涵词是经典蕴涵，联结KA的否定词是经典否定。在这种解读下¬A →¬KA是普遍成立的：假设A没有构造性证明，如果知道A是经典真，那么A就是经典真，进而A可能有构造性证明，因此不知道A是经典真。

定理四K¬A →¬A被解读为：如果知道¬A是经典真，那么A没有构造性证明。其中联结K¬A和¬A的蕴涵词是经典蕴涵。在这种解读下K¬A →¬A是普遍成立的：假设知道¬A是经典真，那么A为假，进而A没有构造性证明。

最后考察对K(A ∨B)→(KA ∨KB)和KA →A的理解。

K(A∨B)→(KA∨KB)被解读为：如果知道A∨B是经典真，那么要么知道A是经典真，要么知道B是经典真。其中联结K(A ∨B)和(KA ∨KB)的蕴涵词是经典蕴涵，联结KA和KB的析取词是经典析取。在这种解读下K(A ∨B)→(KA ∨KB)不是普遍成立的：参考KA被解读为“知道A是直觉主义真或A是经典真”的情况即可。

KA →A被解读为：如果知道A是经典真，那么A就是直觉主义真。其中联结KA和A的蕴涵词是经典蕴涵。在这种解读下KA →A不是普遍成立的：参考KA被解读为“知道A是直觉主义真或A是经典真”的情况即可。

5 结语

本文论证了IEL 的预期解释与BHK 解释的偏离在于缺失了对构造性证明的要求，IEL 是对直觉主义命题逻辑的认知扩充，对于含有认知算子K的公式来说，无法再从直观上遵循直觉主义逻辑的BHK 解释。相比而言，如果对直觉主义逻辑做一定限制（比如直觉主义相干逻辑），那么所得到的直觉主义逻辑的子系统自然遵循着直觉主义逻辑的BHK 解释。对IEL 预期解释的修正还能够为IEL 系统的对应问题带来启示。首先，IPC 的内定理刻画了直觉主义真的命题逻辑规律；作为IPC 的扩充系统，IEL 还刻画了兼容直觉主义真和直觉主义知识的命题逻辑规律。再考虑中间逻辑12中间逻辑也被称作超直觉主义逻辑（superintuitionistic logics）。（intermediate logics）系统，中间逻辑系统为数众多，存在2ℵ0（ℵ0表示最小无穷基数）个中间逻辑（[4]，第59 页），这些中间逻辑系统都是对直觉主义命题逻辑公理系统的扩充，并且是经典命题逻辑公理系统的子系统。最后，将上述两种关系作类比可以提出猜测：IEL 系统对应于某个中间逻辑系统。哥德尔（K.Gödel）曾给出直觉主义命题逻辑系统IPC 和经典模态逻辑系统S4 的对应关系（[3]，第130 页）：先根据一定规则（以递归定义的方式）把IPC的公式转换为对应的S4 的公式：

在此基础上，A是IPC 系统的内定理当且仅当At是S4 系统的内定理。对这个结论做扩展可以得到中间逻辑系统KC、LC 与S4 的扩充系统S4.2、S4.3 的对应如下（[3]，第136 页）：

•A是KC 系统的内定理当且仅当At是S4.2 系统的内定理。

•A是LC 系统的内定理当且仅当At是S4.3 系统的内定理。

与之类似，上述猜测可以表述如下：

先根据一定的规则R把IPC 的公式转换为对应的IEL 的公式，令Γ 是某个中间逻辑系统，那么A是Γ 系统的内定理当且仅当Att是IEL 的内定理，其中Att是通过R从Γ 公式A转换所得的IEL 公式。

上述猜测是否正确留给进一步的研究。