写在前面
第一次看这本书的时候看得比较急，也没有一个big picture的把握，所以在细节上面耗费了很多时间....现在算是重构一次笔记了
我们知道，形式逻辑是对推理的形式化（mathematical logic formalizes resoning），为了描述推理我们有各种各样的逻辑系统。对于一个逻辑系统，最关键的就是它的语法（Syntax）和语义（Semantics）。其中语法决定了逻辑系统中讨论的对象长什么样，而语义决定了我们如何解释这些逻辑系统中被研究的对象。
比如说我们有研究命题的命题逻辑（Propositional Logic）、包含了函数 算术的一阶逻辑（First Order Logic）、对真值进行扩充得到的模态逻辑等等。这些逻辑的区别就在于它们的语法和语义。
同时，在熟悉这些逻辑系统的同时，还要分清什么是我们的研究对象。因为逻辑在研究推理的形式化，因此需要区分什么是逻辑系统中的形式化推理（研究对象），什么是我们对于研究对象的推理。后者被成为元逻辑、元语言，前者就是对象逻辑、对象语言了。所有的对象逻辑都应根据相应的逻辑系统的定义赋予其含义，而在元语言的层面则可以随意一些，就是正常的平时推理。
本书是写给CSer的数理逻辑教材，因此会专门讲不同逻辑系统中的一类算法（Decision Procedure）的构造和正确性证明，这些是纯数不太感兴趣的东西，也是这本书多出来的东西。同时在看的时候，还要尤其注意什么是基础、什么是组合构造方法、这些逻辑对哪些东西做了抽象，这三板斧应该刻在DNA里。
废话不多说
命题逻辑
命题逻辑是比较常见易懂的逻辑，它主要关心在给出若干基本命题（atoms）之后，如何通过组合小命题来获得大命题、如何给组合命题递归地赋予含义（Compositionality），因此用树形结构来展示这样的命题构造就是很自然的了。
语法
给出BNF
\[\begin{aligned} {stmt = atom\;|\;(\neg\;stmt)\;|\;(stmt_1\;op\;stmt_2)} \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，它能判定一个公式是否可满足
构造
令根节点的标记为由待判定的公式 \(A\) 组成的集合 \(\left\{A\right\}\)，记为 \(label(l)=\left\{A\right\}\)
选取一个未被标记为open或closed的叶子 \(l\)，若不存在则前往步骤8
若 \(label(l)\) 全是文字，则如果存在互补对，就标记为closed leaf并回到步骤2；如果不存在就标记为open leaf并回到步骤2。如果不全是文字，则前往步骤4
记 \(label(l)\) 中不是文字的公式为 \(W\)
若 \(W\) 形如 \(A_1\wedge A_2\)，则构造 \(l\) 的儿子 \(l'\)，其标记为 \(label(l')=label(l)-\left\{W\right\}+\left\{A_1,A_2\right\}\)，回到步骤2
若 \(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
若 \(W\) 形如 \(\neg A\)，则根据De Morgan Law化进去，回到4
如果所有叶子都是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))\)，则有如下性质：
任意树上的节点 \(l\) 都有 \(W(l)\geqslant 0\)。这是因为 \(b(\cdot),s(\cdot)\) 都是非负的
任意树上的节点 \(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\)
取这个解释
若 \({\scr I}\models F_{n'+1}\)，那么 \({\scr I}\models \Delta_1\cup\{F_{n'+1}\}\)
若 \({\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\) 的构造：
若 \(p\in\Delta\)，那么 \({\scr I}(p)=T\)
否则必然有 \(\neg p\in\Delta\)，此时规定 \({\scr I}(p)=F\)
下面证明 \({\scr I}\models \Delta\)，只需要对 \(\Delta\) 中的公式做结构归纳即可。其实可以证明一个更强的结论：\(A\in\Delta\) 当且仅当 \(\models A\)
命题对原子命题显然成立；
考虑 \(A=\neg B\) 形式的命题 \(A\)：
由 \(A=\neg B\in\Delta\) 可得 \(B\not\in\Delta\)，故 \({\scr I}\not\models B\)，即 \({\scr I}\models\neg B\)，即 \({\scr I}\models A\)
若 \(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\) 同理....