直觉主义认知逻辑与不同程度的真_程华清.pdf

逻辑学研究2023 年第 1 期，5567文章编号：1674-3202(2023)-01-0055-13直觉主义认知逻辑与不同程度的真程华清摘要：直觉主义认知逻辑 IEL 不仅为邱奇费奇悖论提供了解悖思路，还促进了直觉主义认识论的研究。IEL 的构建旨在遵循 BHK 解释，以“直觉主义知识就是证实的结果”作为核心观点，接纳 A KA 和 KA A。IEL 的预期解释借助“证实”概念给出了“直觉主义知识 KA 的证明”的定义，并以此扩展 BHK 解释。但直觉主义逻辑依赖于直觉主义数学，这使得 BHK 解释的核心在于对构造性证明的要求，基于此，IEL 的预期解释偏离了 BHK 解释的初衷，进而 IEL 未能达到预期构建目标。通过对KA 作新解读，能引出直觉主义真和经典真之间不同程度的真，IEL 系统的一些重要内定理也将获得新理解。此外，关于 IEL 系统对应问题的一个猜测被提出来。关键词：直觉主义认知逻辑；BHK 解释；真；中间逻辑中图分类号：B81文献标识码：A1引言对邱奇费奇悖论1（ChurchFitchparadox）的解悖促进了直觉主义认知逻辑的研究。直觉主义认知逻辑是基于直觉主义逻辑的认知扩充，直觉主义逻辑的构建遵循 BrouwerHeytingKolmogrov 解释2，这意味着直觉主义逻辑包含认知因素3，但其形式语言中不含认知算子，而直觉主义认知逻辑的形式语言能够表达含有认知算子 K 的公式 KA，对认知算子的不同理解形成了不同的直觉主义认知逻辑。直觉主义认知逻辑的研究当前可分为两条进路：(1)接纳知识的事实性（factivity of knowledge）原则 KA A，它也被称为反射（reflection）原则。这方面的代表是9中所构建的系统 IKT，构建 IKT不依赖于 BHK 解释，而是基于以下观点：收稿日期：2022-05-26；修订日期：2022-09-08作者信息：程华清安徽师范大学文学院Huaqing_C基金项目：教育部人文社会科学研究青年基金项目“直觉主义认知逻辑及其哲学意蕴研究”（21YJC72040001）；国家社科基金重大项目“逻辑词汇的历史演进与哲学问题研究”（20&ZD046）。1邱奇费奇悖论指的是：在“任意命题的真都可能被知道”和“存在不知道的真命题”的前提下，通过经典的模态和认知逻辑推演会导致结论“任意命题的真都被知道”，这违背了我们的直觉。2简称 BHK 解释。BHK 解释是从构造性语境下对逻辑算子的解释，关于 BHK 解释的详细阐释见本文第二节。3直觉主义把数学理解为心智的构造性活动，这可被视作一种认知活动，直觉主义逻辑是直觉主义数学的衍生品，更多阐释详见文中第二节内容。56逻辑学研究第 16 卷 第 1 期 2023 年真在于证实（verification）的可能性，其中“证实”被理解为实时（real time）呈现给一个真实主体（real subject）的事物，但真仅仅需要这样事物的可能性而不是其实际的出现。（9，第 63 页）(2)接纳真的构造性（constructivity of truth）原则 A KA，它也被称为余反射（coreflection）原则。这方面的代表是1中所构建的系统 IEL，对 IEL 的构建旨在遵循 BHK 解释，并持有观点：直觉主义认知状态（信念或知识）是证实的结果，其中“证实”指的是足以达到实际目的而给出的确凿的（conclusive）证据（evidence）。4（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 系统对应问题的一个猜测。2IEL 的预期解释与 BHK 解释的偏离IEL 的构建试图遵循 BHK 解释，但这种尝试有一定局限性，本节从直觉主义视角下逻辑和数学的关系出发来论证：IEL 的预期解释偏离了 BHK 解释，进而IEL 并未达到预期构建目标。BHK 解释是直觉主义对基本逻辑联结词和量词的标准解释，它经由布劳威尔（L.E.J.Brouwer）、海廷（A.Heyting）和柯尔莫哥洛夫（A.Kolmogorov）发展而来。基本逻辑联结词的 BHK 解释如下所述（8，第 9 页）：4这种对“证实”的理解与9中所理解的“证实”稍有不同，参见1中第 288 页的注释 30。程华清直觉主义认知逻辑与不同程度的真57(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（mental constructions，6，第 87 页）。这种对证明和构造的理解基于直觉主义对数学以及数学和逻辑关系的独特理解：（一）直觉主义把数学理解为心智的构造性活动，这意味着直觉主义只接受心智可构造的数学对象和心智可构造的数学证明，即：数学对象能够通过直观能行的方法得到，数学命题所表达的内容能够通过直观能行的方法直接验证。数学定理表达的是纯粹经验的事实，数学不能建立在公理化基础之上，直觉（intuition）就是数学可靠性的基础。直觉主义数学的代表是选择序列（choice sequences）理论，利用选择序列能够遵循直觉主义思想构造连续统（continuum），形象地说，可以利用选择序列把连续统“算术化”，进而发展直觉主义分析学。（二）数学不依赖于语言，语言仅仅是记录数学构造的工具，逻辑是利用语言记录数学构造所产生的形式规律，它的有效性自然依赖于数学的构造性。逻辑可以看作是数学的应用，如 6所述：逻辑可被视作语言学的一部分或者关于世界的哲学理论，在这两种理解下它都属于应用数学。仅仅第三种解释处于纯数学讨论范围内。逻辑定理是数学定理。逻辑不是数学的基础，恰恰相反，在概念上它是数学的复杂而精细的部分。（6，第 8687 页）综上所述，对构造性证明的要求是 BHK 解释的核心，这是由直觉主义逻辑依赖于直觉主义数学所决定的。5可称其为构造性证明，它可被理解为直观的能行（effective）方法。58逻辑学研究第 16 卷 第 1 期 2023 年由于对数学的理解不同，导致直觉主义意义上的“真”有别于经典意义上的“真”。经典意义下，一个命题的真独立于对它的证明；但是在直觉主义看来，一个数学命题被判定为直觉主义真就意味着这个命题获得构造性证明。例 1.简单命题“1+1=2”被判定为直觉主义真，其构造性证明为：我们的心智先构造出一个自然数 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（1，第 270 页）这个定义是有缺陷的：根据前面的阐释，对构造性证明的要求是BHK 解释的核心，而命题 KA 的证明并没有对构造性证明的要求，这偏离了 BHK解释的初衷。从另一角度来说，直觉主义数学的数学对象都是从自然数出发而构造性得到的（10，第 4748 页），直觉主义数学命题是关于直觉主义数学对象的命题，直觉主义逻辑依赖于直觉主义数学，上述对“命题 KA 的证明”的定义超出了直觉主义数学的考虑范围，无法严格遵循 BHK 解释。尽管 1 中对此作了一定辩护：反对的要点在于 BHK 解释不能容纳非数学命题。然而这很清楚是错误的，因为在 BHK 解释的表述中没有特别数学化的东西，它并未提到数、函数、集合、范畴、类型等等。（1，第 290 页）但这段辩护并不成立，因为它把 BHK 解释独立于直觉主义数学来看待，并未抓住“直觉主义逻辑依赖于直觉主义数学”这点。Artemov在构建IEL时主张“直觉主义真蕴涵直觉主义知识”：从BHK解释出发，命题 A 是直觉主义真意味着 A 获得证明，证明是一种证实，由于直觉主义知识是证实的结果，因此直觉主义真蕴涵直觉主义知识，进而余反射原则 A KA被 IEL 接受。（1，第 266267 页）但是 IEL 所接受的余反射原则 A KA 仅仅适用于 A 是数学命题的情况：当 A 是数学命题时，A 中不含认知算子 K，对于任意假设的 A 的证明 p，由于证明是最严格意义上的证实，因此 p 可以作为确凿的证据证实“A 有证明”，进而 KA 获得证明；（1，第 271 页）当 A 中包含认知算6比如基于零知识协议的证实便是这类证实：零知识协议是一类密码协议，通常是概率性的，证明者利用这种协议能够使得验证者确信一个给定命题为真，而无需提供任何额外有用的信息。在此基础上，反射原则 KA A不被 IEL 接受。（1，第 273274 页）程华清直觉主义认知逻辑与不同程度的真59子 K 时（不妨令 A 为 KB），A 的真仅仅意味着对 A 的证实，并未体现对构造性证明的要求（构造性证明一定是证实，而证实不一定是构造性证明），这时“命题A 为真”要弱于“A 是直觉主义真”。同样的道理，对于 IEL 所接受的直觉主义反射原则 KA A 来说，它也仅仅适用于 A 是数学命题的情况。当 A 是不含认知算子 K 的公式时，余反射原则和直觉主义反射原则可以分别解读为“直觉主义真蕴涵直觉主义知识”以及“直觉主义知识蕴涵经典真”，可合并简记为“直觉主义真=直觉主义知识=经典真”。（1，第 268 页）此时可以对 A 作 BHK 解释，但是 BHK 解释无法扩展到含有认知算子 K 的公式上，因为一旦把 BHK 解释扩展到认知算子 K 上，那么就没办法保证对构造性证明的要求。综上所述，IEL 的预期解释偏离了 BHK 解释，进而构建 IEL 的预期目标并未达到。3IEL 的形式化工作本节简要回顾 IEL 的形式化工作，并在第二节的讨论基础上重新理解 IEL。令 LK为 IEL 的形式语言，LK的初始符号由以下部分构成：命题变元：p1,p2,p3,.；逻辑联结词：否定词 、合取词 、析取词 和蕴含词 ；认知算子 K；左、右括号：(和)。初始符号中的四个逻辑联结词是相互独立的，公式的递归定义遵循认知逻辑的一般定义方式，在公式省略括号时，逻辑联结词以及认知算子的联结强度遵循认知逻辑通常的约定。对 IEL 的构建可采用 2 中使用的直觉主义命题逻辑公理系统（记为 IPC）为基础（2，第 219220 页），在 LK语言下对 IPC 做认知扩充。在 LK语言下，IEL通过在 IPC 基础上添加如下三条认知公理模式而得到（1，第 276 页）：分配（distribution）公理模式：K(A B)(KA KB)余反射公理模式：A KA 直觉主义反射公理模式：KA A值得一提的是，2 对正规（normal）直觉主义模态逻辑的模型论研究为直觉主义认知逻辑的模型论研究奠定了技术性基础。2 对含有模态算子 的正规直觉主义模态命题逻辑系统 HK 做了研究，给出了相应的克里普克语义，并保持了直觉主义命题逻辑的基本模型论性质。60逻辑学研究第 16 卷 第 1 期 2023 年在 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，第 279280 页）：（一）首先，IEL 模型指的是四元有序组 W,R,E,V，其中 W,R,V 是 IPC的克里普克模型，即：W,R 是非空偏序（partial order），W 被称为结点集，其中的元素被称为结点，W 上的二元关系 R 被称为 W 上的“认知”关系，是命题变元在 W 上的满足单调性的赋值（evaluation）7。其次，W 上的二元关系 E 被称为 W 上的“知识”关系，E 满足：(1)对于任意的结点 u，E(u)R(u)成立8；(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基础上，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公式，对任意的 IEL7对于任意结点 w 和任意命题变元 p 来说，w p 也被称为“w 力迫（forces）p”。8E(x)表示 x|wEx,x W，R(x)表示 x|wRx,x W。9直觉主义命题逻辑克里普克模型的认识论解释参见10中第 6970 页。程华清直觉主义认知逻辑与不同程度的真61模型 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，第280281、283 页）IEL有如下一些重要内定理，其中A是任意的LK公式，比如（1，第276277、第 282 页）：定理一“知识的真值条件”K(A A)定理二“知识的真值条件”(KA A)定理三“知识的真值条件”A KA 定理四 KA A另外，利用 IEL 模型能够证明：K(AB)(KAKB)和 KA A 都不是IEL 的内定理。（1，第 281282 页）根据第二节的讨论，在 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 的预期解释下不是普遍成立的。4KA 的新解读及不同程度的真在 IEL 的预期解释中，当 A 是不含认知算子 K 的数学命题时，除了可以把KA 解读为“A 是直觉主义知识”或“直觉主义知识 A 获得证实”以外，还可以62逻辑学研究第 16 卷 第 1 期 2023 年将其理解为“知道A 是直觉主义真（A 获得构造性证明）或 A 是经典真”，其中联结“A 是直觉主义真”和“A 是经典真”的析取词“或”是经典意义下的析取10。值得注意的是，这种新解读已经不再坚持直觉主义立场了。在这样的解读下，“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.1KA 被解读为“知道 A 是直觉主义真或 A 是经典真”的情况“余反射公理模式”A KA 被解读为：如果 A 是直觉主义真，那么知道 A是直觉主义真或 A 是经典真。其中联结 A 和 KA 的蕴涵词是经典蕴涵。根据不同10这个析取是元语言，而非 IEL 的形式语言。程华清直觉主义认知逻辑与不同程度的真63程度真的关系，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(AA)被解读为：不知道矛盾是直觉主义真或矛盾是经典真。其中联结 K(AA)的否定词是经典否定。在这种解读下 K(AA)是普遍成立的：假设知道矛盾是直觉主义或矛盾是经典真，那么矛盾就是经典真，而矛盾恒假，所以假设不成立。“知识的真值条件”(KAA)被解读为：并非不仅知道 A 是直觉主义真或A 是经典真，而且 A 是直觉主义真。其中联结(KAA)的否定词是经典否定，联结 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 是经典真。定理四 KA A 被解读为：如果知道 A 是直觉主义真或 A 是经典真，那么 A 没有构造性证明。其中联结 KA 和 A 的蕴涵词是经典蕴涵。在这种解读下 KA A 是普遍成立的：假设知道 A 是直觉主义真或 A 是经典真，那么 A 没有构造性证明或 A 为假，进而 A 没有构造性证明。最后考察对 K(A B)(KA KB)和 KA A 的理解。K(AB)(KAKB)被解读为：如果知道 AB 是直觉主义真或 AB是经典真，那么要么知道 A 是直觉主义真或 A 是经典真，要么知道 B 是直觉主义真或 B 是经典真。其中联结 K(AB)和(KAKB)的蕴涵词是经典蕴涵，联64逻辑学研究第 16 卷 第 1 期 2023 年结 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，使用正整数的最小自然数原理，通过反证法可以证明 A 成立（A 是经典真），进而知道 A 是经典真，因此也知道 A 是直觉主义真或 A 是经典真，但是并未给出 A 的构造性证明。4.2KA 被解读为“知道 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(AA)被解读为：不知道矛盾是经典真。其中联结K(AA)的否定词是经典否定。容易证明在这种解读下 K(AA)是普遍成立的。“知识的真值条件”(KAA)被解读为：并非不仅知道 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 是经典真。11这个命题也被称为正整数的阿基米德性质（Archimedean property）。程华清直觉主义认知逻辑与不同程度的真65定理四 KA A 被解读为：如果知道 A 是经典真，那么 A 没有构造性证明。其中联结 KA 和 A 的蕴涵词是经典蕴涵。在这种解读下 KA A 是普遍成立的：假设知道 A 是经典真，那么 A 为假，进而 A 没有构造性证明。最后考察对 K(A B)(KA KB)和 KA A 的理解。K(AB)(KAKB)被解读为：如果知道 AB 是经典真，那么要么知道A 是经典真，要么知道 B 是经典真。其中联结 K(AB)和(KAKB)的蕴涵词是经典蕴涵，联结 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（intermediate logics）系统，中间逻辑系统为数众多，存在 20（0表示最小无穷基数）个中间逻辑（4，第 59 页），这些中间逻辑系统都是对直觉主义命题逻辑公理系统的扩充，并且是经典命题逻辑公理系统的子系统。最后，将上述两种关系作类比可以提出猜测：IEL 系统对应于某个中间逻辑系统。哥德尔（K.Gdel）曾给出直觉主义命题逻辑系统 IPC 和经典模态逻辑系统 S4 的对应关系（3，第 130 页）：先根据一定规则（以递归定义的方式）把 IPC的公式转换为对应的 S4 的公式：pt=p(A B)t=At Bt(A B)t=At Bt(A B)t=At Bt(A)t=At12中间逻辑也被称作超直觉主义逻辑（superintuitionistic logics）。66逻辑学研究第 16 卷 第 1 期 2023 年在此基础上，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 公式。上述猜测是否正确留给进一步的研究。参考文献1S.Artemov and T.Protopopescu,2016,“Intuitionistic epistemic logic”,The Review of SymbolicLogic,9(2):266298.2M.Boi and K.Doen,1984,“Models for normal intuitionistic modal logics”,Studia Logica,43(3):217245.3J.P.Burgess,2009,Philosophical Logic,Princeton:Princeton University Press.4D.M.Gabbay and F.Guenthner,2014,Handbook of Philosophical Logic,Vol.5,Netherlands:Springer Netherlands.5L.Goble,2001,The Blackwell Guide to Philosophical Logic,Oxford:Blackwell Publishers.6A.Heyting,1974,“Intuitionistic views on the nature of mathematics”,Synthese,27(1/2):7991.7S.Lewitzka,2019,“Reasoning about proof and knowledge”,Annals of Pure and Applied Logic,170(2):218250.8A.S.Troelstra and D.van Dalen,1988,Constructivism in Mathematics:An Introduction,Vol.1,Amsterdam:Elsevier Science Publishers.9T.Williamson,1992,“On intuitionistic modal epistemic logic”,Journal of Philosophical Logic,21(1):6389.10冯棉，经典逻辑与直觉主义逻辑，1989 年，上海：上海人民出版社。（责任编辑：袁之）程华清直觉主义认知逻辑与不同程度的真67Intuitionistic Epistemic Logic and Truthof Varying DegreesHuaqing ChengAbstractTheintuitionisticepistemiclogicsystemIELoffersanewwayofresolvingChurchFitch paradox,moreover,it inspires studies on intuitionistic epistemology.It attemptsto establish IEL in maintaining BHK interpretation.Based on the view of“intuitionisticknowledge be regarded as the result of verification”,both A KA and KA AholdinIEL.IntheintendedinterpretationofIEL,itdefines“proofofintuitionisticknowl-edge KA”in virtue of“verification”,and BHK interpretation gets extended in this way.However,it should be noted that“constructive proof”plays a core role in BHK interpre-tation because intuitionistic logic relies on intuitionistic mathematics,this results in thedeviation between the intended interpretation of IEL and BHK interpretation.So IELfails to reach its original purpose.In additio