写在前面
第一次看这本书的时候看得比较急，也没有一个big picture的把握，所以在细节上面耗费了很多时间....现在算是重构一次笔记了
我们知道，形式逻辑是对推理的形式化（mathematical logic formalizes resoning），为了描述推理我们有各种各样的逻辑系统。对于一个逻辑系统，最关键的就是它的语法（Syntax）和语义（Semantics）。其中语法决定了逻辑系统中讨论的对象长什么样，而语义决定了我们如何解释这些逻辑系统中被研究的对象。
比如说我们有研究命题的命题逻辑（Propositional Logic）、包含了函数 算术的一阶逻辑（First Order Logic）、对真值进行扩充得到的模态逻辑等等。这些逻辑的区别就在于它们的语法和语义（当然应用也不一样，这是废话）。
同时，在熟悉这些逻辑系统的同时，还要分清什么是我们的研究对象。因为逻辑在研究推理的形式化，因此需要区分什么是逻辑系统中的形式化推理（研究对象），什么是我们对于研究对象的推理。后者被成为元逻辑、元语言，前者就是对象逻辑、对象语言了。所有的对象逻辑都应根据相应的逻辑系统的定义赋予其含义，而在元语言的层面则可以随意一些，就是正常的平时推理。
本书是写给CSer的数理逻辑教材，因此会专门讲不同逻辑系统中的一类算法（Decision Procedure）的构造和正确性证明，这些是纯数不太感兴趣的东西，也是这本书多出来的东西。同时在看的时候，还要尤其注意什么是基础、什么是组合构造方法、这些逻辑对哪些东西做了抽象，这三板斧应该刻在DNA里。
废话不多说
命题逻辑
命题逻辑是比较常见易懂的逻辑，它主要关心在给出若干基本命题（atoms）之后，如何通过组合小命题来获得大命题、如何给组合命题递归地赋予含义（Compositionality），因此用树形结构来展示这样的命题构造就是很自然的了。
语法
给出BNF
\[{stmt = atom\;|\;(\neg\;stmt)\;|\;(stmt_1\;op\;stmt_2)} \]为了方便，引入语法符号 \(\top,\bot\)，规定任意解释下都有 \({\mathscr I}(\bot)=F,{\mathscr I}(\top)=T\)
注意，我们给出这样的定义之后，无穷多项的公式就不存在了（回忆BNF的推导序列是有限的）
通常记所有公式组成的集合为 \(\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作用到每个元素上就得到了无穷多个公理。