数理逻辑及其 python 实现:0

本文是围绕 Mathematical Logic through Python 的个人笔记，书中每个任务都放在一小节中，比如小节标题里的 T1.4 表示围绕书本里 Task 1.4 的代码实现和理解，其中可能会穿插一些从其他逻辑相关资料里阅读到的值得一提的背景或扩展。

本文给出了前 6 章命题逻辑中所有必要任务的代码实现， 但考虑到文章篇幅，删除了类和函数的 docstring ，后六章由于代码量太大，同样因篇幅问题只保留对各章节核心内容的文字说明以及少量关键代码。

所有任务的个人实现参见： metaescape/logicpy

本书基于 python 实现命题逻辑和谓词逻辑语言，以一种 "我创造不了的东西，我就没有理解它" 的理念来教人理解数理逻辑。它不是面向应用层面的，也就是说， 本书不是构建一个类似 lean 或者 prolog 的语言用来帮助人类进行定理证明或者基于知识进行推理实现某种人工智能的工具，而是阐明 (基于公理的)逻辑语言的特点，最终想要证明的是谓词逻辑的语义完备性（以及引出公理不完备性的简介）。

哥德尔在 1930 年第一次给出了完备性的一种证明，也称为哥德尔完备定理（但本书采用了后人的更精简的证明方式）。它描述的是，谓词逻辑作为一种证明系统 – 机械地从初始字符串根据变换规则不断产生新的字符串的机器，其内部的语法替换规则在语义视角上来看是完备的，或者说是充分的。

为了说明 "完备性" 、“语义” 等概念，需要引入对字符串的分类，这包括两个维度：

• 字符串的合法性（或者叫作 well-formed）：和编程语言一样，你不能在 python 中用数字作为变量名的第一字符，比如 1234_cat, 同样你不能在本书规定的逻辑语言里写出 p~q 这样的命题。

  这是绝对的二分类问题，根据这种分类法，我们淘汰了大部分随机的字符串序列， 正如以下 python 语句在执行前就会被报错，无法进入真正的解释阶段。

  832_a=2
  

• 对于那些入围的合法字符串，则继续对其进行三分类：真、假或未知。

  由于逻辑运算符可以对不同字符串进行连接，那么拼接的结果字符串也需要有一个类型， 它取决于子字符串的类型以及连接符号对类型的组合或变换能力，对于或运算(记为 |), 那么 p|q 有以下组合情况（与 python 中 or 的语义是类似的）：

  print(True or True)
  print(False or True)
  print(True or False)
  print(False or False)
  

  True
  True
  True
  False
  

接着我们对字符串定义了一套变换规则，比如若前文中已经得到了 p 和 p->q 字符串，那么可以生成 q 字符串。对这些变换的基本要求是，在变换过程中，对于已经是 True 分类的字符串，永远都只产生 True 分类的其他句子，这称为保真性，而对于分类为 False 的字符串没有任何约束，即变换后可以变成任意是真或者假甚至真假未知的字符串，所以对于一个可靠的或者或一致的系统，不允许能够生成任何分类为假的字符串。

这些逻辑连接符的语义规则以及字符串之间的变换规则是如何设计的？它来自于笛卡尔式地不断怀疑和精简的结果，也来自历史上人们对真和假的概念的打磨，比如矛盾律表明：一个事实不可能既是真的又是假的，因此它的语义被认为定义的符号 ~ 所刻画，如果 p 是真的那么 ~p 就是假的，反之亦然，且 p&~p 必须是假的（& 是与运算）。在 python 中的体现是：

p = True
print(not p)
print(not p and p)

False
False

再比如排中律表明：两个互相矛盾的命题，不可能同时为假，必有一真，因此 p|~p 的语义就是真：

p = True
print(not p)
print(not p or p)

False
True

以上只是对逻辑连接符语义的结晶，对于命题变换规则，最核心的是肯定前件规则（modus ponens, 简称 MP）， 它说的是，如果 p->q；且 p 为真，那么 q 为真。

这些规则都是看似无可辩驳的阿基米德点（一切思想牢固而不可动摇的起点，或者第一性），然而，一旦我们确定了这些基本语义规则，不再陷于以上哲学倾向的讨论中，而只是用这套规则去构造逻辑系统并用规则进行推理时，几乎不再需要真和假的概念，它们纯粹是一种类型标记，可以用猫和狗，A 和 B 或者其他任何二元对来替代，以至于罗素说到：纯数学是一门我们不知谈论的是什么，或者不知所谈的是否是真的一门学科。

引入这些概念后，哥德尔完备性说的是，如果某个命题在给定前提是猫的情况下也是猫，那么这个命题一定可以通过变换规则从给定前提下变换得到。注意前文说到，在设计这些变换规则的时候，就已经带着对猫（真）的执着，因此完备性表明的是另外一个方向，即知道结果是真的情况下，反过来一定可以论断出它是能够通过某种确定性的有限的手段构造出来的。这就好比高考复习资料是按照从易到难的标准设计的，只要学生遵照着从头学到尾，总能考到一个不错的成绩，而完备性则说，只要考到一个不错成绩的同学都是按照这种方式按部就班努力获得的（这对于编写教辅资料的人来说是一大利好）。

如果要把真和假的概念代入，完备性说的是：如果字符串在某些字符串背景下是有意义的，那么我们可以从这些背景字符串出发通过无意义的字符串变换旋转跳跃着去"嘲讽"其意义（如果 p 为真，那么可以机械地证明出 p, 如果 p 为假，那么可以证明出 ~p）。但如果字符串在某些字符串背景下是无意义的，那么我们也无法通过无意义手段去嘲讽它，因为它本身就是无意义的。

比如说：

• 在 p&q 为猫的背景下，根据 & 的语义规则，p 是猫，而完备性表明，是猫的字符串一定能从其前提 p&q 根据预定义的变换手段把单独的字符串 p 给生成出来。
• p 在 ~p&~q 为猫的背景下是狗，因此完备性表明，我们一定能从 ~p&~q 根据预定义的变换手段把字符串 ~p 给推导出来。
• 但 p 在 p|q 为真的背景下分类是未知的，所以我们无法从字符串 p|q 出发通过替换算法得到 p 。

可以看到，完备性实际涉及逻辑系统机制的内在和谐：

• 我们需要一套解释，比如 ~p|p 为真（或属于猫）
• 我们需要根据这套解释定义一些生成字符串的规则，比如根据 p 和 p->q, 可以生成字符串 q

如果我们修改语义，比如说在其他语义不变的情况下定义 ~p|p 为假（也就是唐吉可德般挑战排中律），那么整个系统的性质都会改变。 同样，如果我们尊重这些语义分类的定义，但删除某些变换规则，比如禁止一切替换规则，那么除了能从初始字符串得到初始字符串本身，什么也得不到，显然系统就不再完备。

另一方面，以上讨论的完备性只适用于包含这些语义和预定义好的变换规则的逻辑系统本身，这称为语义完备性。 从 p|q 无法推导出 p 可以展示出另外一种完备的概念，即初始命题集的完备性，集合 {p|q} 是不完备的，因为它甚至无法决定初始集合里明确存在的某个子命题 p 的分类。而初始命题集 {p&q} 是完备的，因为对于任何在初始命题里提及的字符串以及其任意合法组合字符串，比如 p->q, ~p|(p->q) 的语义分类都是明确的，根据逻辑系统语义完备性，所以这些字符串都可以被无意义地推导出来。

在 1931 年，也就是证明谓词逻辑本身完备性的一年后，哥德尔证明，以谓词逻辑作为推理引擎、 Peano 自然数公理集作为初始字符串集合是不完备的，也就是说，一定有一些关于自然数的命题是无法被证明的，就像在 p|q 为前提下 p 是无法被证明的一样。但对于后者来说，这是容易理解的，p|q 只是概括性地说明了 p 或者 q 为真，无法精确到具体的某个命题的真假， 就像任何法律法规都可能会有一些没有说清楚的条款，导致有人钻空子一样，这不是很正常的事情吗？为什么哥德尔不完备定理会获得那么高的评价？核心在于在该定理被证明之前，人们认为数学这种精确的系统不同于可能充满悖论或歧义的自然语言系统（如法律），正是出于这种目的，以希尔伯特为核心的数学家们才希望用无意义的手段去绕开因为有意义才出现的 "悖论" 或 "歧义", 从而认为一切数学知识都是确定并且能够机械地被证明出来。

哥德尔指出这是不可能的，尽管它用了一个现实中几乎不会出现的无法被证明的命题（所以也许实际大部分定理还是可以被机械证明），但至少打破了 "一切皆可证" 的独断。更重要的点在于，哥德尔说明某个自然数命题不可证，是因为描述自然数的初始字符串所蕴含的意义本身过于丰富，强大到可以表达用来描述本身的谓词逻辑语言，于是哥德尔可以通过自然数里的函数套娃式地编写逻辑语言解释器（就像本书用 python 编写出逻辑语言解释器一样，而 python 最底层都是二进制的数字表示），以至于连同加减乘除操作的自然数就可以表达出"我无法被证明" 这一命题（被称为哥德尔命题），如果这个命题可以被证明，那么它就是假的，谓词逻辑推理规则的保真性就出了问题，如果它不能被证明，那么它就是真的，说明有些真的命题是无法被证明的。注意这里讨论的真和假必须是现实中真和假概念，而不再是猫和狗了，因为根据谓词逻辑语义的完备性，如果它是猫或者是狗，系统就一定能证明它，因此 "我无法被证明" 这一命题在逻辑系统内的语义类型一定是未知的，但从系统外，它是真的。原本想要极力避免的意义，又莫名其妙地回来了，以至于哥德尔本人在后半生不疯魔不成活，把意义概念泛化，认为世界和世界中的万事万物都有意义或理由，而人的潜能从未在一生一世中实现（而人又是比自然数更加强大而灵活的系统），因此人必有来生。（参考《逻辑人生》第五章）

然而，这实际反应的是 Peano 公理不只有一个解释模型，比如 {p|q} 集合因缺乏细粒度信息而无法证明出 p 或者 ~p ，这说明 p|q 对应了多个令该语句为真（猫）的模型，实际这样的解释模型有三个： {p=True,q=True}, {p=True,q=False},{p=False,q=True}, 这才导致了 p 在不同模型有不同解释，因此 p 无法被证明，就好比你想去朋友所在城市旅游，但你只和朋友说了一句如来，对应了两种可解释的模型，因此对方不知道你到底来不来，也就无法给你规划时间和路线。

Peano 公理集的不完备性揭示了，人们所认为的那个精确而唯一的对自然数的描述（人类以此进行计算已经沿用几千甚至上万年）实际仍然会有歧义， 这种歧义并非来自公理集信息明显的匮乏，因为人们对公理集本身是精细打磨并挑选的，它们看上去精确而完善，但由于能力过强，语言过于灵活产生了反噬，最终仍然呈现出精确性的丧失。因此存在另外的关于自然数的解释模型，其中 "我无法被证明" 这个命题是假的，这是导致它无法被无意义推导所"嘲讽" 的核心原因。

但另一方面，这种歧义可能只在远离日常的极端情况下出现，比如花费很大努力精心构造出的哥德尔命题。不过在追求构造这种极端命题的努力中，又无心插柳般地催生出了图灵机以至于开启了整个现代计算机时代，这是该定理对实际生活深远影响的体现。

本书在多个层次上都体现了不完备定理的影响，根据图灵机所实现的计算机，以及在计算机上实现的 python 语言本身强大到可以编写任何其他语言的解释器。而本文就是用 python 先编写命题逻辑的解释，在此基础上继续实现谓词逻辑解释器，以此证明了命题逻辑和谓词逻辑在有限数量命题作为前提下的完备性，对于无限情况则用文字补充论证。

但为了引出公理集的不完备定理，从而更清晰理解什么是语义的完备性。作者在最后一章说明，谓词逻辑语言加上额外的 Peano 公理集（体现为用户自定义的一套宏模板）可以编写出自然数的描述，但通过自然数及其运算又可以描述一个谓词逻辑解释器，后者工作量巨大，因为要用自然数里的运算对应上谓词逻辑里所有操作（因此本文不讨论）。 谓词逻辑本身可以用来描述某类数的性质，比如偶数是那些可以写成 2y 的自然数，那就是使得命题 \( \forall x \exists y[x=2y] \) 为真的 自然数集合，而当自然数可以编码谓词逻辑里的语法对象时，谓词逻辑系统就可以描述其自身的特性了，比如它可以写出一个谓词逻辑命题，该命题的内容是 "以 ~ 作为初始符号的命题所编码对应的数"，类似以下 python 函数可以看到自己的函数名，从而谈论那些函数名以 this 开头的函数：

import inspect

def this_function_name_have_n_words():
    # 获取当前函数的名称
    function_name = inspect.currentframe().f_code.co_name
    word_count = len(function_name.split('_'))
    return function_name.startswith("this")

this_function_name_have_n_words()

True

最终理论上可以写出 "我无法被证明" 的逻辑描述，如果在谓词逻辑系统上实现一个通用的自动推理算法，这个算法无法生成 "我无法被证明" 所对应的字符串。 就像最终沿着以上 python 程序的思路也可以描述出一个判断程序否会停机的函数，但无法实现通用的这类算法，因为计算机本身可以看作是一个运行着的推理系统，我们可以从逻辑上描述具有某种功能的句子（或程序），但无法将其转换成一个只通过规则进行字符串（或者 bit 和 byte）替换的推理过程（算法），这正是哥德尔不完备定理所论述的。

本文的抽象度和注意力控制在底层哲学问题（比如语义为什么这样定义）和上层应用问题（如何用逻辑模拟智能）之间，只讨论技术上如何实现一个特别的逻辑语言的解释器，用其中实现的各个模块的合理性来说明逻辑系统的可靠性、一致性、完备性等性质，并在部分溢出抽象层的场景附带一些说明。最后要说明的是，后文不会再讨论公理集的完备或不完备性质，即本节已经覆盖了对原书第 13 章的理解。

整个目录的结构如下：

• 一、命题逻辑的语法 ：定义一套语法，并根据语法实现一个 parser
• 二、命题逻辑的语义 ：用真值表的方式定义逻辑联结词的语义，用模型来定义某些初始原子命题的语义，同时定义语义等价的替换操作
• 三、更多逻辑运算符 ：比较其他运算符，例如 <->, nand 等
• 四、命题逻辑的演绎证明: 引出 "证明" 以及其所对应的 python 对象，证明可以看作是从假设起点按照推理规则"搜索"到目标命题的整个路径。
• 五、对"证明"的处理: 这部分引入了证明的 soundness 性质以及非常重要的演绎定理，从而可以谈论逻辑系统一致性以及反证法的合理性
• 六、命题逻辑的语义完备性 通过对重言公式构造指数级别数量的捕获集合并对证明进行合并来证明命题的语义完备性

其他参考资料包括：

• CS221: Artificial Intelligence: Principles and Techniques 中的逻辑部分
• Introduction to Logic - Lessons
• 哥德尔证明
• 逻辑人生
• 逻辑的引擎