集异璧(一)——形式系统、数学中的形式与意义

写在前面：最近把科普书《哥德尔埃舍尔巴赫——集异璧之大成》的部分有趣知识整理成了阅读笔记。
个人非常推荐这本书，这是一本读来令人惊艳的好书，它以精心设计的巧妙笔法深入浅出地介绍了数理逻辑、可计算理论、人工智能、复杂系统等学科领域中的许多有趣理论以及它们背后的联系。这本书的价值不在于它科普知识的深度，而在于它的美，相信这本书也会让你对很多东西重拾兴趣。
优秀的科普书就是这样，能激发人继续学习和探索的兴趣。

集异璧

本篇笔记涉及的内容是GEB的前两个章节，讨论的是关于形式系统及其意义。形式系统的一些基础知识放到了文章的最后，大多数内容只要有一点数理逻辑的基础就能理解。

形式系统WJU

GEB的开篇中探讨了这样一个有趣的问题，给定一个形式系统中的命题公式，判定该命题公式是否是形式系统中的定理。
在数理逻辑中，如果一个命题公式是形式系统的定理，那么这个定理是可以被该形式系统证明的，也就是根据系统的公理和规则能通过有限步的构造，得到这个定理的符号表达式。特别要注意有限步的限制。因为如果某个定理的证明需要无限步骤这本身就没有意义。
那么现在考虑这样一个问题，能否单靠系统本身的公理和推理规则在有限步骤内判定一个命题公式是定理还是非定理呢？
GEB书中给出了这样一个有趣的形式系统：
形式系统WJU

该符号系统是由 $W，J，U$ 所组成的字符串
初始串是 $WJ$ (相当于该系统的一条公理)
系统规则：
1 如果串的最后一个符号是 $J$ ，则可以加上一个 $U$
即：如果 $xJ$ 是定理，那么 $xJU$ 也是定理。
2 如果串是 $Wx$ 形式，则可以再加上 $x$ 生成 $Wxx$ ， $x$ 代表任意由 $W，J，U$ 组成的串
即：如果 $Wx$ 是定理，那么 $Wxx$ 也是定理
3 如果一个串中出现 $JJJ$ ，则可以用 $U$ 代替 $JJJ$ 得到新串
即：如果 $xJJJy$ 是定理，那么 $xUy$ 也是定理
4 如果串中出现 $UU$ ，则可以将 $UU$ 删掉得到新串
即：如果 $xUUy$ 是定理，那么 $xy$ 也是定理

问题： $WU$ 是否是系统中的串？( $WU$ 是否是该系统中的定理)
我们当然可以自己按规则推理出这个形式系统具有的一些定理，甚至发现这个系统产生的串的一些固定模式(比如系统中的串一定是 $W$ 开头的)，而且推导一会儿你就会发现， $WU$ 应该不会出现在该系统中了，不妨称为直觉。但是为什么会这样我们还是没法说的透彻。另外从形式系统的角度看，由公理和推理规则，我们很容易构造定理树(定理推理序列树)：

WJU定理树

其中父节点到子结点的边上的数字表示按照该系统相应的规则推理。只要我们符合这个系统的推理规则，就可以得到一棵树，这棵树上每个结点都是该系统中的定理，那么现在问题就转化为： $WU$ 是否存在于这棵定理树上？
我们可以看到，这棵树的层次是无穷的，如果 $WU$ 是该系统的定理，则必然可以在该树的某一层次上找到它，而且总会在有限步骤内找到。但是，如果 $WU$ 不在这棵树上，那我们就永远也找不到它，这样也就没办法判定它到底是不是定理了。但我们希望的是，在一个形式系统中一个命题是否定理最好能在有限步骤内给出答案。因为我们希望在把这个问题交给一个有计算能力的机器时，它能在有限时间给出问题的解答，人是一种智能生物(姑且这样认为吧)，我们可以靠直觉发现 $WU$ 应该不是系统的定理甚至非常确信，因为人类总会发现一些除了系统公理和规则之外的特定模式和规律，所以我们不会为了这个问题无休止地推理下去，但是机器并不这样，想让机器解决这个问题，它就必须能有一个可以终止的条件，能保证在有限时间解决该问题。
那么 $WU$ 到底在不在这棵树上呢？如果交给机器并按照 $WJU$ 系统自身的规则并给不了我们答案，我们需要另寻它法，借助一些系统之外的规则来帮助我们。注意这里借助系统外规则的含义，你马上就会看到它并不是改变了系统规则，而是在一个兼容该系统的系统上去做推理。我们借助的这个系统就是一个和 $WJU$ 同构的系统 $310$ 。所谓同构就是这两个系统结构是完全一样的，只是我们换用了字符来进行表示，用 $W$ 对应 $3$ ， $J$ 对应 $1$ ， $U$ 对应 $0$ ，所有规则不变。

WJU的同构系统310

看上去只是换了字符，那这样做有什么好处呢，好处就是这样做我们为这个系统引入了数论的性质， $WJU$ 由一个字符串组成的系统变成了一个由 $3,1,0$ 三个数字组成自然数集合了。
同构系统310

该符号系统是由 $3，1，0$ 所组成的自然数
自然数 $31$ 在系统中(公理)
系统规则：
如果集合中有数以 $1$ 结尾，则末尾添加一个 $0$ 也是集合中的数
如果集合中有数以 $3$ 开始，则把 $3$ 后面的数字重复一次添加在后面也是集合中的数
如果集合中有数包含 $111$ ，则把 $111$ 替换为 $0$ 也是集合中的数
如果集合中有数包含 $00$ ，去掉 $00$ 也是集合中的数

那么 $WU$ 是否是系统 $WJU$ 的定理就转化为 $30$ 是否是系统 $310$ 的定理。
在 $310$ 系统中可以很轻松地判定出，这个系统中的数都不可能被 $3$ 整除，这很显然：
首先， $31$ 不能被 $3$ 整除，其次，规则1，2，3，4都无法从不能被 $3$ 整除的数中生成能被 $3$ 整除的数。
这下清楚了， $30$ 能被 $3$ 整除，故 $30$ 不是系统 $310$ 的定理，从而 $WU$ 不是系统 $WJU$ 的定理。
怎么样，神奇吧。

给我们的启发

在上述讨论中，我们已经看到，在仅仅使用系统本身的公理和规则是难以保证在有限步骤内判定一个命题是否是该系统的定理的。有时为了判定，我们需要系统外的规则，比如同构拥有数论性质的系统。
这揭示了一种人和机器的某种区别，人能够在按照系统规则推理时发现一些特定的规律和模式，这些规律和模式促使我们寻找系统之外的手段来解决研究的问题，但是同样的任务交给机器就不会这样了。

形式系统pq

再来看另外一个有趣的形式系统——pq系统，该系统有三个不同的符号：
$p,q,-$

系统公理的描述型定义：只要 $x$ 仅由短杠组成，那么 x-qxp- 就是一条公理。
系统的唯一生成规则：假设 $x，y，z$ 都代表由短杠组成的符号串，且 $xqypz$ 是一条已知定理，那么 x-qypz- 就是一条定理。
比如让x是“ ---” ， y是“ --” ， z是“ -” ，这条规则就是：如果 ---q--p- 是一条定理，则 ----q--p-- 也是一条定理。
现在我们的问题是，给定一个符号串如何判定它是不是pq系统的定理。
首先由系统公理和规则，一个串一定要以一组短杠开头，然后有一个q，接着是第二组短杠，然后是p，最后是另一组短杠，这才有可能成为定理。这样的符号串都叫作良构符号串。凡是非良构的一定不是定理。可以发现，一个良构符号串是否是定理的标准是后两组短杠加起来是否等于第一组短杠。例如： ----q--p-- 是一条定理，因为4等于2加2，而 -q--p-- 不是一条定理，因为1不等于2加2。另外，该系统的定理是不断加长的，因为并没有缩短符号串的规则。
这样一来对于符号串是否是定理的判定就可以设计算法了：

自底向上方案：从基础公理和生成规则一步步加长字符串，这样会把系统的每一条定理都产生出来。当出现比要判定的串更长的串时还没有出现这个需要判定的串，就可以说这个串不是定理。

注意区分和WJU系统的区别，WJU由于同时有加长和缩短的规则所以不能这样简单判定。

自顶向下方案：将要判定的串按照规则往短串回溯，如果最终剩余的短串是系统的公理，则该串就是定理。

同构产生意义

从前面的讨论中可以发现，pq系统的模式特别像自然数加法，我们可以把q解释为equel，p解释为plus，短杠数目对应到自然数。是什么东西使我们那样想的呢？因为我们在pq定理与加法之间看到了同构。

pq与加法同构

“ 同构” 这个词的适用情景是：两个系统可以互相建立映射，并且每一个系统的每一部分在另一个系统中都有一个相应的部分。这里“ 相应” 的意思是：在各自的系统中，相应的两个部分起着相类似的作用。当然严格的同构需要在数学上定义。有了同构，我们就可以把对原本很复杂我们不熟悉的系统的研究转换到对同构系统的研究上，就像pq系统本身是一堆符号，但当与加法建立同构后，在相应的解释下这些符号就有了意义。定理的同构反应了世界的部分真理。
有意义的解释和无意义的解释
p:马 q:幸福 -:苹果，这样的解释就是无意义的，因为这样的解释对人来说和原来没什么区别，并不对应现实世界的真理。
主动意义与被动意义
受加法的影响我们可能认为在pq系统中 --------q--p--p--p-- 是一条定理。至少，我们可能希望这个符号串是一条定理，因为8等于2加2加2加2，但它不是定理，因为它不是良构的，这样的解释在pq系统中是错误的，我们的有意义的解释都是从良构符号串中得出的。所以在一个形式系统中，意义一定是“ 被动的” 。我们可以根据其组成符号的意义来读每个符号串，但是我们没有权力只根据我们给符号指定的意义而创造出新的定理。经过解释的形式系统是横跨在没有意义的系统与有意义的系统之间的。可以认为，它们的符号串是“ 表达” 事物的，但这也必定是系统的形式性质的产物。
多重意义
pq系统也可以解释为减法。一个系统可以有不同的解释。解释只要精确地反映现实世界的某种同构，就是有意义的。当现实世界中的不同方面彼此同构时（这里是说加法和减法），一个形式系统可以与这两者都同构，因此可以有多种被动意义。
形式系统与现实
系统的定理和有关那部分现实中的真理同构。然而，现实和形式系统是互相独立的，并不需要意识到在两者之间存在着同构关系，他们每一方面都独立存在，不论我们是否知道加法、知道2等于1加1，在pq系统的公理和规则下 --q-p- 都是一条定理，并且不论我们是否把它与加法相联系，--q-p- 总是一条定理。
就形式系统而言，我们几乎只触及了表面。人们很自然地想知道，现实的哪一部份能够用一组支配无意义符号的形式规则来加以模仿。现实世界的一切都可以变为形式系统吗？

形式系统简介

数理逻辑中，只是使用真值计算，以带入规则，替换规则进行推演是难以反应人类思维的推理过程，我们需要建立严密的符号推理体系。也就是我们要像做数学计算一样进行推理，这样的推理体系就是形式系统。
形式系统

形式系统是一个符号体系
形式系统中的概念用符号来表示，推理过程即符号变换的过程
它以若干最基本的重言式(永真式)为基础，称做公理
系统内符号变换的依据是若干由重言式导出重言式的规则，称作推理规则

公理和推理规则能确保正确的前提总能得到正确的推理结果。
证明
公式序列 $A_1,A_2,...,A_m$ 称作 $A_m$ 的一个证明，如果 $A_i(1\leq{i}\leq{m})$ :

或者是公理
或者是由 $A_{j_1},A_{j_2},...,A_{j_k}(j_1,...,j_k\leq{i})$ 用推理规则推得

当这样的证明存在时，称 $A_m$ 为系统的定理。
演绎
设 $\Gamma$ 为一公式集合，公式序列 $A_1,A_2,...,A_m$ 称作 $A_m$ 的以 $\Gamma$ 为前提的一个演绎，如果 $A_i(1\leq{i}\leq{m})$ :

或者是公理
或者是 $\Gamma$ 中的公式
或者是由 $A_{j_1},A_{j_2},...,A_{j_k}(j_1,...,j_k\leq{i})$ 用推理规则推得

当这样的演绎存在时，称 $A_m$ 为 $\Gamma$ 的演绎结果。
可以看到，其实证明就是演绎在 $\Gamma$ 为空集时的特例。

命题演算形式系统PC(Proposition Calculus)

我们将命题以及重言式变换演算构造为形式系统，成为命题演算形式系统PC：
PC的构成：

首先，PC是一个符号系统
命题变元： $p,q,r,s,...$
命题常元： $t,f$ ，分别代表真和假
联结词和括号： $\neg,\rightarrow$ (功能完备集)， $()$
命题公式：由命题常元和变元合法组成的公式，命题常元命题变元本身就是公式。 $A,B$ 是公式，则 $\neg{A}, A \rightarrow B$ 也是公式，只有有限次使用上面两条规则得到的符号串才是命题公式。

PC的公理：
$A \rightarrow (B \rightarrow A) \\ (A \rightarrow (B \rightarrow C))\rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) \\ (\neg{A} \rightarrow \neg{B}) \rightarrow (B \rightarrow A)$
PC的推理规则
分离规则： $A,A\rightarrow B\ than\ B$ ( $A,B$ 表示任意公式)，也就是如果公式序列已经有 $A$ 和 $A\rightarrow B$ 那么可以在公式序列后面添加上 $B$ 。

此外为了扩大形式系统的可研究范围以及形式语言的易理解性，还有谓词演算形式系统FD，自然推理系统ND等等。

完美的形式系统应该具有的性质：

合理性：如果 $A$ 是PC的定理，则 $A$ 是重言式；如果 $A$ 是集合 $\Gamma$ 的演绎结果，则 $A$ 是 $\Gamma$ 的逻辑结果。合理性说明了PC中的定理和演绎结果都是合乎逻辑的。
一致性： $\neg{A},A$ 不能同时出现在PC中，也就是一个符合逻辑的形式系统不可能即推出 $A$ ，又推出 $\neg{A}$ 这两个自相矛盾的命题。
完备性：如果 $A$ 是重言式，则 $A$ 一定是PC中的定理，这意味着PC中一定存在证明序列可以得到 $A$ ；如果 $A$ 是公式集合 $\Gamma$ 的逻辑结果，则 $A$ 一定是 $\Gamma$ 的演绎结果。也就是凡是合乎逻辑的命题，一定可以被该系统证明。

PC是满足上述性质的(证明太难，略了)。那么任意一个形式系统可不可能都同时满足上面3个性质呢，现在来思考一下这个问题，为了保证推得的命题是真命题，首先性质1和性质2必须被满足(否则这样的系统没有意义)。那么性质3呢？一个真命题一定能够被系统本身证明吗？或者换句话说：一个命题一定能够在该系统内部被证明是真或者是假吗？答案是否定的，这也正是哥德尔所做的工作之一。
元定理
元定理就是关于定理证明的定理。

演绎定理： $\Gamma$ 推出 $A\rightarrow B$ 当且仅当 $\Gamma \cup{\{A\}}$ 推出 $B$ ，特别当 $\Gamma$ 为空集时， $A\rightarrow B$ 当且仅当 $A$ 推出 $B$ 。
归谬定理：若 $\Gamma \cup{\neg{A}}$ 推出 $B$ 且 $\Gamma \cup{\neg{A}}$ 推出 $\neg{B}$ ，则 $\Gamma \rightarrow A$ ，其意义在于如果同一组前提能推导出相互矛盾的结论，说明这组前提之间相互不一致。那么这组前提中就存在一些前提，它的反面可以被 $\Gamma$ 推出(对立面是正确的)。
穷举定理：若 $\Gamma \cup{\neg{A}}$ 推出 $B$ 且 $\Gamma \cup{A}$ 推出 $B$ ，那么 $\Gamma$ 推出 $B$ (不依据 $A$ )，其意义在于如果一个前提和这个前提的反面都能推出相同的结论，那么说明这个结论的成立与该前提是否成立没有关系，就可以从 $\Gamma$ 中剔除这个前提。

一阶谓词演算形式系统(First order predicate Calculus)

FC的符号系统：
个体变元：x，y，z，u，v，w，...
个体常元：a，b，c，d，e，...
个体间运算符号(函数符)： $f^{(n)}，g^{(n)}，h^{(n)}，...$ ，其中n是正整数，表示函数的元数
谓词符号： $P^{(n)},Q^{(n)},R^{(n)},S^{(n)},...$ ，n表示谓词的元数，当n=0时谓词公式退化为命题常元
联结词与括号： $\neg,\rightarrow,()$
量词： $\forall$ ( $\exists{x}$ 等价于 $\neg \forall x \neg$ )
个体项(term)：简称项，个体变元和个体常元是项；若 $f^{n}$ 是n元函数符， $t_1,t_2,...t_n$ 为项，则 $f^{n}(t_1,t_2,...,t_n)$ 也为项；只有有限次使用上述规则得到的符号串才是项。
合式公式：简称公式，若 $P^{n}$ 是n元谓词符， $t_1,t_2,...t_n$ 为项，则 $P^{n}(t_1,t_2,...,t_n)$ 是公式，n=0时，命题常元也是公式；如果 $A,B$ 是公式，v为任意一个个体变元， $\neg A,A\rightarrow B,\forall{vA(v)}$ 都是公式；只有有限次使用上述规则得到的符号串才是公式。
全称封闭式：是用全称量词 $\forall$ 约束给定公式所有自由变元所得的闭公式。

FC的公理：
$A \rightarrow (B \rightarrow A) \\ (A \rightarrow (B \rightarrow C))\rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) \\ (\neg{A} \rightarrow \neg{B}) \rightarrow (B \rightarrow A) \\ \forall{xA(x)} \rightarrow A(t)\\ \forall{x}(A(x)\rightarrow B(x))\rightarrow (\forall{x}A(x)\rightarrow \forall{x}B(x)) \\ A\rightarrow \forall{xA} \\ 上述6条的全称封闭式都是FC的公理$
FC的推理规则：
分离规则： $A,A\rightarrow B\ than\ B$ ( $A,B$ 表示任意公式)，也就是如果公式序列已经有 $A$ 和 $A\rightarrow B$ 那么可以在公式序列后面添加上 $B$ 。
全称引入规则：
存在消除规则：
上述两条规则一样可以推广到演绎中。如存在消除规则，我们经常在数学证明中用“不妨设”理论依据就是这个规则。

自然推理系统ND

FC和PC都比较繁复，为了追求简洁只用了两个联结词，如果能够引入更多联结词，量词，推理规则，那么证明和演绎都会更加的自然。
(演绎)为了证明A-＞B，常假设A成立，如果能够证明B成立，则A-＞B也就被证明。
(归谬/反证)为了证明A，常假设非A，得到矛盾。
(穷举)已知A或B，常假设A和B成立分别证明C，若都能成功，则完成C的证明。
(不妨设)
在形式系统中引入带假设的推理规则，能够使推理过程更加接近人的思维，更加高效和便捷。
自然推理系统ND
采用5个联结词，2个量词
少数的公理，更多的规则，引入假设。
用推理规则体现人的推理习惯
公理只有一个 $\Gamma,A$ 可以推出 $A$ ，这也是自然推理系统的证明方式。
推理规则(18条)：
假设引入规则
假设消除规则
$\vee$ 引入规则
$\vee$ 消除规则
$\wedge$ 引入规则
$\wedge$ 消除规则
$\rightarrow$ 引入规则
$\rightarrow$ 消除规则
$\neg$ 引入规则
$\neg$ 消除规则
$\neg\neg$ 引入规则
$\neg\neg$ 消除规则
$\leftrightarrow$ 引入规则
$\leftrightarrow$ 消除规则
$\forall$ 引入规则
$\forall$ 消除规则
$\exists$ 引入规则
$\exists$ 消除规则
FC的公理和定理都是ND的定理，ND是合理的一致的完备的。

最后编辑于：2020.04.18 08:38:53

人面猴
序言：七十年代末，一起剥皮案震惊了整个滨河市，随后出现的几起案子，更是在滨河造成了极大的恐慌，老刑警刘岩，带你破解...
沈念sama阅读 193,495评论 5赞 459
死咒
序言：滨河连续发生了三起死亡事件，死亡现场离奇诡异，居然都是意外死亡，警方通过查阅死者的电脑和手机，发现死者居然都...
沈念sama阅读 81,469评论 2赞 369
救了他两次的神仙让他今天三更去死
文/潘晓璐我一进店门，熙熙楼的掌柜王于贵愁眉苦脸地迎上来，“玉大人，你说我怎么就摊上这事。” “怎么了？”我有些...
开封第一讲书人阅读 140,825评论 0赞 318
道士缉凶录：失踪的卖姜人
文/不坏的土叔我叫张陵，是天一观的道长。经常有香客问我，道长，这世上最难降的妖魔是什么？我笑而不...
开封第一讲书人阅读 51,974评论 1赞 263
港岛之恋（遗憾婚礼）
正文为了忘掉前任，我火速办了婚礼，结果婚礼上，老公的妹妹穿的比我还像新娘。我一直安慰自己，他们只是感情好，可当我...
茶点故事阅读 60,849评论 4赞 355
恶毒庶女顶嫁案：这布局不是一般人想出来的
文/花漫我一把揭开白布。她就那样静静地躺着，像睡着了一般。火红的嫁衣衬着肌肤如雪。梳的纹丝不乱的头发上，一...
开封第一讲书人阅读 45,990评论 1赞 272
城市分裂传说
那天，我揣着相机与录音，去河边找鬼。笑死，一个胖子当着我的面吹牛，可吹牛的内容都是我干的。我是一名探鬼主播，决...
沈念sama阅读 36,415评论 3赞 380
双鸳鸯连环套：你想象不到人心有多黑
文/苍兰香墨我猛地睁开眼，长吁一口气：“原来是场噩梦啊……” “哼！你这毒妇竟也来了？” 一声冷哼从身侧响起，我...
开封第一讲书人阅读 35,125评论 0赞 253
万荣杀人案实录
序言：老挝万荣一对情侣失踪，失踪者是张志新（化名）和其女友刘颖，没想到半个月后，有当地人在树林里发现了一具尸体，经...
沈念sama阅读 39,351评论 1赞 288
护林员之死
正文独居荒郊野岭守林人离奇死亡，尸身上长有42处带血的脓包…… 初始之章·张勋以下内容为张勋视角年9月15日...
茶点故事阅读 34,474评论 2赞 307
白月光启示录
正文我和宋清朗相恋三年，在试婚纱的时候发现自己被绿了。大学时的朋友给我发了我未婚夫和他白月光在一起吃饭的照片。...
茶点故事阅读 36,249评论 1赞 324
活死人
序言：一个原本活蹦乱跳的男人离奇死亡，死状恐怖，灵堂内的尸体忽然破棺而出，到底是诈尸还是另有隐情，我是刑警宁泽，带...
沈念sama阅读 32,119评论 3赞 310
日本核电站爆炸内幕
正文年R本政府宣布，位于F岛的核电站，受9级特大地震影响，放射性物质发生泄漏。R本人自食恶果不足惜，却给世界环境...
茶点故事阅读 37,496评论 3赞 298
男人毒药：我在死后第九天来索命
文/蒙蒙一、第九天我趴在偏房一处隐蔽的房顶上张望。院中可真热闹，春花似锦、人声如沸。这庄子的主人今日做“春日...
开封第一讲书人阅读 28,838评论 0赞 17
一桩弑父案，背后竟有这般阴谋
文/苍兰香墨我抬头看了看天上的太阳。三九已至，却和暖如春，着一层夹袄步出监牢的瞬间，已是汗流浃背。一阵脚步声响...
开封第一讲书人阅读 30,118评论 1赞 250
情欲美人皮
我被黑心中介骗来泰国打工，没想到刚下飞机就差点儿被人妖公主榨干…… 1. 我叫王不留，地道东北人。一个月前我还...
沈念sama阅读 41,366评论 2赞 340
代替公主和亲
正文我出身青楼，却偏偏与公主长得像，于是被迫代替她去往敌国和亲。传闻我的和亲对象是个残疾皇子，可洞房花烛夜当晚...
茶点故事阅读 40,573评论 2赞 335