\newcommand\norm[1]{\left\lVert#1\right\rVert} \newcommand\abs[1]{\left\lvert#1\right\rvert}

写在前面

第一次看这本书的时候看得比较急，也没有一个big picture的把握，所以在细节上面耗费了很多时间….现在算是重构一次笔记了

我们知道，形式逻辑是对推理的形式化（mathematical logic formalizes resoning），为了描述推理我们有各种各样的逻辑系统。对于一个逻辑系统，最关键的就是它的语法（Syntax）和语义（Semantics）。其中语法决定了逻辑系统中讨论的对象长什么样，而语义决定了我们如何解释这些逻辑系统中被研究的对象。

比如说我们有研究命题的命题逻辑（Propositional Logic）、包含了函数 算术的一阶逻辑（First Order Logic）、对真值进行扩充得到的模态逻辑等等。这些逻辑的区别就在于它们的语法和语义。

同时，在熟悉这些逻辑系统的同时，还要分清什么是我们的研究对象。因为逻辑在研究推理的形式化，因此需要区分什么是逻辑系统中的形式化推理（研究对象），什么是我们对于研究对象的推理。后者被成为元逻辑、元语言，前者就是对象逻辑、对象语言了。所有的对象逻辑都应根据相应的逻辑系统的定义赋予其含义，而在元语言的层面则可以随意一些，就是正常的平时推理。

本书是写给CSer的数理逻辑教材，因此会专门讲不同逻辑系统中的一类算法（Decision Procedure）的构造和正确性证明，这些是纯数不太感兴趣的东西，也是这本书多出来的东西。同时在看的时候，还要尤其注意什么是基础、什么是组合构造方法、这些逻辑对哪些东西做了抽象，这三板斧应该刻在DNA里。

废话不多说

命题逻辑

命题逻辑是比较常见易懂的逻辑，它主要关心在给出若干基本命题（atoms）之后，如何通过组合小命题来获得大命题、如何给组合命题递归地赋予含义（Compositionality），因此用树形结构来展示这样的命题构造就是很自然的了。

语法

给出BNF

\begin{aligned}

\end{aligned}

为了方便，引入语法符号 $\top,\bot$，规定任意解释下都有 ${\mathscr I}(\bot)=F,{\mathscr I}(\top)=T$

通常记所有公式组成的集合为 $\mathscr F$

语义

定义公式 $A$ 的一个解释 $\mathscr I$ 为一个函数 $U_A\mapsto \left{T,F\right}$，其中 $U_A$ 为公式 $A$ 中包含的所有原子所组成的集合

通过 ${\mathscr I}(A_1)$ 和 ${\mathscr I}(A_2)$ 给出 ${\mathscr I}(A_1\;op\;A_2)$ ，以此来定义命题构造子（别人都叫他运算符，但我更喜欢这么说）$op$ 的含义

若在某个解释 $\scr I$ 下公式 $A$ 满足 ${\scr I}(A)=T$，我们就说 $A$ 是可满足的（satisfiable），此时的 ${\scr I}$ 是 $A$ 的一个模型（Model）

若在任意解释 ${\scr I}$ 下公式 $A$ 满足 ${\scr I}(A)=T$，我们就说 $A$ 是永真的（valid），记作 $\models A$

类似可以定义永假的（即不可满足的 unsatisfiable）、可假的（fasifiable）记作 $\not\models A$，在某些操作下这四种性质可以互相转化

需要注意的是，我们在命题逻辑中讨论的全都是命题变元（语法上的公式），而赋予其真值是解释做的事情（语义上的含义）。这也是为什么我没有通过给“运算符”列真值表来定义，这里的定义完全是基于解释的。

定义和定理

公式组成的集合的解释

记 ${\scr U}=\left{A\right}$ 为公式的集合（在这里我们忽略无穷集，因为对于无穷的二元运算没有定义）

若在某个解释 ${\scr I}$ 下有 ${\scr I}(A)=T$ 对 ${\scr U}$ 中的每个公式都成立，则称 ${\scr U}$ 是可满足的

若在任意解释 ${\scr I}$ 下都存在 ${\scr U}$ 中的某个公式 $A$ 使得 ${\scr I}(A)=T$，则称 ${\scr U}$ 是不可满足的

容易发现这个定义就是在讨论 $\bigwedge_{A\in {\scr U} } A$ 在解释 ${\scr I}$ 下的真值

运算符

一个 $n$ 元运算实际上是 $\left{T,F\right}^n\mapsto \left{T,F\right}$ 的一个函数，因此有 $\scr F$ 上的本质不同的 $n$ 元运算有 $2^{2^n}$ 种。

在结构归纳法中我们需要讨论所有形式的公式（即，在每一种运算下产生的所有公式），非常麻烦。一种想法是找出尽可能基本的运算，在此之上构造剩余的运算。

定义运算 $\circ$ 能被 $O=\left{\circ_1,\circ_2\ldots\circ_n\right}$ 表示，当且仅当对于任意 $\scr F$ 中的公式 $A,B$，都有 $A\circ B=C_X\circ_Y C_X\cdots C_X$

其中 $C_X\in\left{A,B\right}$，$\circ_Y\in O$

特殊地，对于单目运算符 $\sim$，我们修改定义为 $\sim A=A\circ_Y A\cdots A$，其中 $\circ_Y\in O$

定义运算集 $O$ 是完备的（Adequate），当且仅当所有运算都可被 $O$ 表示。学过数电都知道 NAND和NOR 可以搭出所有电路，在逻辑系统中也有这样的性质，证明只需要简单的构造一下就好了。常用的完备集是 $\left{\wedge,\vee,\neg\right}$

定理：二元运算的最小完备集只可能是 $\uparrow$ 或 $\downarrow$，即NAND或NOR。具体的证明可以看后面的习题合辑（如果我没有咕咕咕的话）

等价、逻辑后承

定义 $\mathscr F$ 上的二元关系 $\equiv$ 逻辑等价（Logical Equivalence）为：

$A_1\equiv A_2$ 当且仅当在任意解释下，有 ${\mathscr I}(A_1)={\mathscr I}(A_2)$

定义逻辑后承（Logical Consequence）的含义为：

${\scr U}\models A$ 当且仅当在所有使得 ${\scr U}$ 可满足的解释 $\scr I$ 下，都有 ${\scr I}(A)=T$

我个人觉得也可以叫语义后承

$A\leftrightarrow B$ 永真当且仅当 $A\equiv B$

$\bigwedge_{A\in {\scr U} }A\rightarrow B$ 永真 当且仅当 ${\scr U}\models B$

这两个定理实际上是为命题逻辑系统中的语法符号作出了解释，即我们可以用一些逻辑系统内部满足的性质来代替元语言的描述

子公式、替换

子公式仍然是 $\scr F$ 上的二元关系，在不影响上下文理解的时候，我们将把 $A$ 是 $B$ 的子公式简记作 $A\subseteq B$

子公式的严格定义可以通过公式作为树结构导出，只需要照抄子树的定义就好

同样在树结构上操作，我们可以将一棵子树替换为另一棵子树，在公式中就表现为将一段子公式替换为另一个公式，记作 $A\left{B\leftarrow C\right}$，其中 $B\subseteq A$，解释为 把 $A$ 中的所有子公式 $B$ 替换为公式 $C$

若 $B\equiv C$ 且 $B\subseteq A$，则有 $A\left{B\leftarrow C\right}\equiv A$ 成立

具体的证明可以通过对树形结构来归纳做。

文字、互补对

这个翻译很怪

对于原子 $p$，我们把 $p$ 和 $\neg p$ 称为一对文字（Literals），其中 $p$ 是正文字（Positive），$\neg p$ 是负的（Negative）

同一个原子的两个文字组成一对互补对（Complementary Pair）

若公式集 ${\scr U}$ 存在一对互补对，即存在 $p,\neg p\in {\scr U}$，当且仅当 ${\scr U}$ 不可满足

这是由定义即得的。互补对定理使得我们可以构造出一种正确的Decision Procedure

理论

若公式集 $\scr F$ 在 $\models$ 二元关系下满足封闭性，则称 $\scr F$ 是一个理论（Theory），$\scr F$ 中的公式为定理（Theorem）

对于一个理论 $\scr F$，若存在 $\scr U\subseteq F$ 使得 ${\scr F=}\left{A|{\scr U}\models A\right}$，则称 $\scr F$ 是可公理化的（Axiomatizable），$\scr U$ 是 $\scr F$ 的一组公理。

需要注意的是，这里对公理集的大小没有限制。考虑皮亚诺公理系统，我们对自然数集中的每个元素都作出了公理化的定义，因此皮亚诺公理系统的公理集合实际上是由一个Axiom Scheme产生的，我们把这个单独的Scheme作用到每个元素上就得到了无穷多个公理。

Decision Procedure

对于 $\scr F$ ，一个算法 ${\scr F}\mapsto \left{T,F\right}$ 被称为是一个Decision Procedure。记使其输出为 $T$ 的公式集合为 $\scr U$，显然有 $\scr U\subseteq F$，我们称这个算法是 Decision Procedure on $\scr U$

通常我们会关注 Decision Procedure on Validity，即给定一个公式判断它是否永真

Semantic Tableaux

ST是一种Decision Procedure，它能判定一个公式是否可满足

构造

1. 令根节点的标记为由待判定的公式 $A$ 组成的集合 $\left{A\right}$，记为 $label(l)=\left{A\right}$

2. 选取一个未被标记为open或closed的叶子 $l$，若不存在则前往步骤8

3. 若 $label(l)$ 全是文字，则如果存在互补对，就标记为closed leaf并回到步骤2；如果不存在就标记为open leaf并回到步骤2。如果不全是文字，则前往步骤4

4. 记 $label(l)$ 中不是文字的公式为 $W$

5. 若 $W$ 形如 $A_1\wedge A_2$，则构造 $l$ 的儿子 $l’$，其标记为 $label(l’)=label(l)-\left{W\right}+\left{A_1,A_2\right}$，回到步骤2

6. 若 $W$ 形如 $A_1\vee A_2$，则构造 $l’,l’’$，其中 $label(l’)=label(l)-\left{W\right}+\left{A_1\right}$，$label(l’’)=label(l)-\left{W\right}+\left{A_2\right}$，回到步骤2

7. 若 $W$ 形如 $\neg A$，则根据De Morgan Law化进去，回到4

8. 如果所有叶子都是closed，则称这棵树也是closed的，输出不可满足；否则称这棵树是open的，输出可满足

Termination

记公式 $A$ 所含二元运算的数量为 $b(A)$，单目运算数量为 $s(A)$，定义 $b({\scr U})=\sum\limits_{u\in{\scr U} }b(u)$，$s({\scr U})=\sum\limits_{u\in{\scr U} }s(u)$

对于节点 $l$，构造其势能函数为 $W(l)=b(label(l))+s(label(l))$，则有如下性质：

1. 任意树上的节点 $l$ 都有 $W(l)\geqslant 0$。这是因为 $b(\cdot),s(\cdot)$ 都是非负的

2. 任意树上的节点 $l$ 及其子节点 $l’,l’’$，都有 $W(l)> W(l’),W(l)> W(l’’)$。这个只需要针对步骤5、6、7分别讨论就好了

因此上述构造必然终止。并且因为必然终止，所以每个叶子要么open，要么closed

正确性

对于Decision Procedure的正确性要分成Soundness和Completeness两方面证明

Soundness

即证明：如果Semantic Tableaux closed，那么公式不可满足

即证明：如果算法claim公式 $A$ 是不可满足的，那么 $A$ 确实是不可满足的

Completeness

即证明：如果公式不可满足，则所有的Semantic Tableaux都closed

即证明：如果公式 $A$ 不可满足，则上述算法构造出来的所有Semantic Tableaux都closed，算法永远claim $A$ 不可满足

证明就咕咕咕啦。这样，这一章就看完啦

Compactness

讨论的是任意大小的公式集 $\scr U$ 的可满足性

定义使得性质 “任意 ${\scr S}\subseteq {\scr U}$ 若 $|{\scr S}|\in\mathbb N$ 那么 ${\scr S}$ 可满足” 成立的集合 $\scr U$ 为有限可满足公式集。有限可满足的公式集的所有有限子集都可满足。那么有定理：若 $\scr U$ 有限可满足，那么 $\scr U$ 仍然可满足。

首先取有限可满足集 $\Gamma_0$。注意到公式集 $\scr F$ 是可数集，因此可以构造公式序列 ${\scr F}=\left{F_1,F_2,F_3\ldots\right}$

定义若 $\Gamma_{n}\cup{F_{n+1}}$ 可满足，那么 $\Gamma_{n+1}=\Gamma_n\cup{F_{n+1}}$，否则 $\Gamma_{n+1}=\Gamma_{n}\cup{\neg F_{n+1}}$

有如下claim：$\Gamma_n$ 的存在性对于任意的正整数 $n$ 成立。由反证法，假设存在最小的 $n’$ 使得 $\Gamma_{n’}\cup{F_{n’+1}}$ 与 $\Gamma_{n’}\cup{\neg F_{n’+1}}$ 都不是有限可满足公式集，则根据定义存在 $\Delta_1,\Delta_2\subseteq \Gamma_{n’}$ 使得 $\Delta_1\cup{F_{n’+1}}$ 与 $\Delta_2\cup{\neg F_{n’+1}}$ 都不是可满足的。又因为 $\Delta_1,\Delta_2$ 是 $\Gamma_{n’}$ 的子集，且 $\Gamma_{n’}$ 有限可满足，因此存在解释 $\scr I$ 使得 ${\scr I}\models \Delta_1\cup\Delta_2$

取这个解释

1. 若 ${\scr I}\models F_{n’+1}$，那么 ${\scr I}\models \Delta_1\cup{F_{n’+1}}$

2. 若 ${\scr I}\models \neg F_{n’+1}$，那么 ${\scr I}\models\Delta_2\cup{\neg F_{n’+1}}$

无论如何都与假设矛盾，因此假设不成立；

此时再构造 $\Delta=\bigcup\limits_{i=0}^{\infty} \Gamma_{i}$，则任取 $\Delta$ 的有限子集 $S$，其中都存在下标最大的公式 $F_{max}\in S$，那么根据定义有 $S\subseteq\Gamma_{max}\subseteq\Delta$。由 $\Gamma_{max}$ 有限可满足即得 $S$ 有限可满足。由 $S$ 的任意性即得 $\Delta$ 有限可满足

此时取所有原子命题的集合 ${\scr P}$，有 ${\scr P}$ 中的任意原子 $p$，要么 $p\in\Delta$，要么 $\neg p\in\Delta$，且二者不同时成立。

不同时成立只需要反证一下，结合 $\Delta$ 有限可满足，且 ${p,\neg p}$ 不可满足就能得到

同样反证 $p\not\in\Delta$ 且 $\neg p\not\in\Delta$，由 $p\in{\scr F}$ 可知存在自然数 $k$ 使得 $F_k=p$，构造一下 $\Gamma_{k+1}$ 就会发现必然有 $p\in\Gamma_{k+1}$ 或 $\neg p\in\Gamma_{k+1}$，由$\in$ 符号的传递性即得 $p\in\Delta$ 或 $\neg p\in\Delta$

对 $\Delta$ 中出现的原子进行 $\scr I$ 的构造：

1. 若 $p\in\Delta$，那么 ${\scr I}(p)=T$

2. 否则必然有 $\neg p\in\Delta$，此时规定 ${\scr I}(p)=F$

下面证明 ${\scr I}\models \Delta$，只需要对 $\Delta$ 中的公式做结构归纳即可。其实可以证明一个更强的结论：$A\in\Delta$ 当且仅当 $\models A$

命题对原子命题显然成立；

考虑 $A=\neg B$ 形式的命题 $A$：

1. 由 $A=\neg B\in\Delta$ 可得 $B\not\in\Delta$，故 ${\scr I}\not\models B$，即 ${\scr I}\models\neg B$，即 ${\scr I}\models A$

2. 若 $A=\neg B\not\in\Delta$，那么 $B\in\Delta$，故 ${\scr I}\models B$，即 ${\scr I}\not\models\neg B$，即 ${\scr I}\not\models A$

考虑 $A=B\wedge C$ 形式的命题 $A$：

必然有 $B,C\in\Delta$，否则不妨假设 $B\not\in\Delta$，则 ${\neg B,A}\subseteq\Delta$，此时 ${\neg B,A}$ 不可满足，这与 $\Delta$ 有限可满足矛盾；

由归纳假设，${\scr I}\models{B,C}$，故 ${\scr I}\models A$

$A=B\vee C,A=B\rightarrow C$ 同理….