写在前面

在上一章给出了命题逻辑的语法、语义，公理化的定义，以及一种判定公式是否可满足/永真的算法，但是这还不够，因为：

1. 并不是所有逻辑都有Decision Procedure，因此这种方法不够普遍
2. 即使有，在有无穷多的公理时，Decision Procedure很可能没法处理无穷项的公式（算法不一定终止）
3. 即使终止，Decision Procedure也只能展示一件事情：命题的真值。我们没法得到中间结果，对理解逻辑没有帮助

于是就有了推演系统（Deductive System），这是对推理证明的形式化。同样的，推演系统有很多种，每一个都有自己的语法（公理+推导规则）和语义（对应逻辑的语义）。在命题逻辑中，不同的一致完备推演系统相互等价，这可以看成是对同一个东西的不同解释（模型）。我们所有的推演都是基于语法的推导，而一致性和完备性则是连接了语法和语义的桥梁，它保证了推演系统足够强大又不会出错。

推演系统

包括一组公理集（Set of Axioms）和一组推演规则（Rules of Inference）

证明

一个证明（Proof）指的是一段长度有限的公式序列 \(A_1,A_2\ldots A_n\)，其中每个公式 \(A_i,i\in\left\{1\ldots n\right\}\)

1. 要么是公理
2. 要么可以由前面的公式+推演规则得到
3. 要么是前面出现过的公式
4. 要么是已经证明过的定理

用 \(\vdash A\) 表示 \(A\) 在推演系统中可证明，即存在一个证明使得 \(A\) 是最后出现的公式，称 \(A\) 为一个定理（Theorem）。对于中间出现的公式我们称为引理（Lemma）。

\(\scr G\)

给出 Gentzen 系统的（语法）定义

公理

含有互补对的公式集是公理

推演规则

有两类规则

\[\frac{\vdash U\cup\left\{\alpha_1,\alpha_2\right\}}{\vdash U\cup\left\{\alpha\right\}} \\ \frac{\vdash U\cup\left\{\beta_1\right\}\text{\quad}\vdash U\cup\left\{\beta_2\right\}}{\vdash U\cup\left\{\beta\right\}} \]

一个常见的例子是令 \(\alpha=\alpha_1\vee\alpha_2\)，\(\beta=\beta_1\wedge\beta_2\)

在 \(\scr G\) 中，一个证明即是一个由公式集组成的序列。

正确性

\(\scr G\) 的正确性由如下重要定理给出：

设 \(\scr U\) 是一个公式集，\(\scr \bar U\) 定义为 \({\scr\bar U}=\left\{\bar A\mid A\in{\scr U}\right\}\)，那么有 \(\vdash {\scr U}\) 当且仅当 \({\scr \bar U}\) 存在closed Semantic Tableaux

该定理的特殊情况是 \({\scr U}=\left\{U\right\}\)，此时定理表述为：在 \(\scr G\) 中 \(\vdash U\) 当且仅当 \(\neg U\) 存在closed Semantic Tableaux

证明

先证明充分性，即：若 \(\scr\bar U\) 存在closed Semantic Tableaux \(\scr T\)，则 \(\vdash\scr U\)

考虑对 \(\scr T\) 这个树形结构做结构归纳

1. \(\scr\bar V\) 是 \(\scr T\) 的叶子，则其存在互补对，此时 \(\scr V\) 也存在互补对，因此 \(\scr V\) 是 \(\scr G\) 中的公理，\(\vdash\scr V\)

2. \(\scr\bar V\) 不是 \(\scr T\) 的叶子，不妨设 \(\scr\bar V\) 中的新增公式为 \(\phi\)，分类讨论：

   1. \(\scr\bar V\) 是一个 Semantic Tableaux 上的 \(\alpha\) 推导，则不妨设 \(\phi=\alpha_1\wedge\alpha_2\)，则其子树 \(\scr\bar V'\) 根据归纳假设有 \(\vdash\scr V'\)，并且有 \(\scr\bar V'=\bar V-\left\{\alpha_1\wedge\alpha_2\right\}\cup\left\{\alpha_1,\alpha_2\right\}\)。

      此时可得 \({\scr V}={\scr V'}\cup\left\{\neg(\alpha_1\wedge\alpha_2)\right\}-\left\{\neg\alpha_1,\neg\alpha_2\right\}\)，再根据 \(\scr G\) 中的 \(\alpha\) 推导规则就可得到 \(\vdash\scr V\)。对于 \(\phi\) 为其它情况的证明是类似的。

   2. \(\scr\bar V\) 是一个 Semantic Tableaux 上的 \(\beta\) 推导，则不妨设 \(\phi=\beta_1\vee\beta_2\)，则其子树 \(\scr\bar V_1,\bar V_2\) 根据归纳假设有 \(\vdash\scr V_1,\vdash V_2\)，并且有 \(\scr\bar V_1=\bar V-\left\{\beta_1\vee\beta_2\right\}\cup\left\{\beta_1\right\},\;\bar V_2=\bar V-\left\{\beta_1\vee\beta_2\right\}\cup\left\{\beta_2\right\}\)。

      此时可得 \({\scr V}={\scr V_1\cup V_2}\cup\left\{\neg(\beta_1\vee\beta_2)\right\}-\left\{\neg\beta_1,\neg\beta_2\right\}\)，再根据 \(\scr G\) 中的 \(\beta\) 推导规则就可得到 \(\vdash\scr V\)。对于 \(\phi\) 为其它情况的证明是类似的。

再证明必要性，即：若 \(\vdash \scr U\)，那么 \(\scr\bar U\) 存在closed Semantic Tableaux \(\scr T\)

注意到 \(\scr G\) 中的证明本身也有某种树形结构（不过是倒置的），因此也考虑对 \(\scr U\) 做结构归纳

1. \(\scr U\) 是 \(\scr G\) 中的公理，故存在互补对，此时 \(\scr\bar U\) 也存在互补对，故 \(\scr\bar U\) 必然构造出 \(\scr T\)
2. \(\scr U\) 经推导而来，不妨记新增公式为 \(\phi\)，记 \({\scr U}={\scr U'}\cup\left\{\phi\right\}\)
   1. \(\phi = \alpha_1\vee\alpha_2\)，此时记前提（Premise）为 \(\scr U_1=\scr U'\cup\left\{\alpha_1,\alpha_2\right\}\)，必然已有 \(\vdash {\scr U_1}\)。根据归纳假设有 \(\scr\bar U_1\) 存在closed Semantic Tableaux，并且有 \({\scr\bar U} = {\scr \bar U_1}\cup\left\{\neg(\alpha_1\vee\alpha_2)\right\}-\left\{\neg\alpha_1,\neg\alpha_2\right\}\)，只需要根据Semantic Tableaux中的 \(\alpha\) 推导规则就可以通过 \(\scr\bar U_1\) 的Tableaux来得到 \(\scr\bar U\) 的Tableaux了。其余形式的 \(\phi\) 的证明是类似的。
   2. \(\phi = \beta_1\wedge\beta_2\)，此时记前提（Premise）为 \(\scr U_1=\scr U'\cup\left\{\beta_1\right\},U_2=U'\cup\left\{\beta_2\right\}\)，必然已有 \(\vdash {\scr U_1},\vdash{\scr U_2}\)。根据归纳假设有 \(\scr\bar U_1\) 和 \(\scr\bar U_2\) 都存在closed Semantic Tableaux，并且有 \({\scr\bar U} = {\scr \bar U_1}\cup{\scr\bar U_2}\cup\left\{\neg(\beta_1\wedge\beta_2)\right\}-\left\{\neg\beta_1,\neg\beta_2\right\}\)，只需要根据Semantic Tableaux中的 \(\beta\) 推导规则就可以通过 \(\scr\bar U_1,\bar U_2\) 的Tableaux来得到 \(\scr\bar U\) 的Tableaux了。其余形式的 \(\phi\) 的证明是类似的。

回过头看这个证明，无非是把 \(\scr G\) 中的每个公式集取反后就对应到了 Semantic Tableaux 上，并且可以发现两个系统里的推导规则可以一一对应。再结合对公式集可满足性的定义就会发现，本质上是对整个公式集组成的大公式做了取反，仅此而已。

Soundness & Completeness

在 \(\scr G\) 中，\(\vdash A\) 当且仅当 \(\neg A\) 存在closed Semantic Tableaux 当且仅当 \(\neg A\) 不可满足 当且仅当 \(\models A\)

这样就证完了。只需要建立起 \(\scr G\) 到 \(\scr T\) 的一一对应，就可以利用 \(\scr T\) 的一致完备性得到 \(\scr G\) 的一致完备性，这正是推演证明的一种。

\(\scr H\)

我靠这个花体字实在是太帅了，奈何我怎么都写不出这种感觉。

在 \(\scr H\) 中用大写字母表示命题变元（即可带入任意的命题）

下面给出Hilbert 系统的定义

公理

\[\begin{aligned} \textbf{Axiom 1 } &\vdash A\rightarrow (B\rightarrow A) \\ \textbf{Axiom 2 } &\vdash (A\rightarrow (B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow (A\rightarrow C)) \\ \textbf{Axiom 3 } &\vdash (\neg B\rightarrow\neg A)\rightarrow(A\rightarrow B) \end{aligned} \]

推演规则

只有一条

\[\frac{\vdash A\;\;\;\vdash A\rightarrow B}{\vdash B} \]

也叫做肯定前件（modus ponens），记为MP

对证明的拓展

设 \(\scr U\) 是公式集，\(A\) 是某个公式，则符号 \({\scr U}\vdash A\) 表示 \(\scr U\) 中的公式是证明 \(A\) 的假设

\(\scr H\) 中的证明是一系列形如 \({\scr U_i}\vdash A_i\) 的公式，其中 \(A_i\)

1. 要么是公理
2. 要么是已经证明过的引理
3. \(A_i\in {\scr U_i}\)
4. 可由已经证明过的定理+MP得到

这一拓展反映的是证明形如“如果 \(A\) 那么 \(B\) ”的命题时，我们可以假设 \(A\) 成立，然后检查 \(B\) 是否可被证明。

衍生规则

虽然只有MP是足够的，但是只用MP就像在裸奔，因此需要包装MP和公理来得到一些更抽象的推演规则。We are now doing composition!

具体可以把这些规则看成是一些语法上的宏，展开就能得到纯MP和公理组成的推演规则。

Deduction Rule

\[\frac{{\scr U}\cup \left\{A\right\}\vdash B}{{\scr U}\vdash A\rightarrow B} \]

这条规则就反映了拓展证明的意图，这条规则保证了我们可以在证明 \(A\rightarrow B\) 时先假设 \(A\)，再证明 \(B\)

下面需要证明拓展是sound的，即不会引入原本不能证明的命题。其completeness是显然的。

对 \({\scr U}\cup\left\{A\right\}\vdash B\) 的推导步骤数 \(n\) 作数学归纳法

1. \(n=1\)，此时 \(B\) 一步就得到了，因此 \(B\) 要么是公理，要么是 \(A\)，要么是已经证过的定理，下面给出 \(B\neq A\) 的证明：

   \[\begin{aligned} &{\scr U}\vdash B \\ &{\scr U}\vdash B\rightarrow (A\rightarrow B) &\textbf{Axiom 1} \\ &{\scr U}\vdash A\rightarrow B &\text{MP 1, 2} \end{aligned} \]

   故sound

   当 \(A=B\)，该命题退化为 \({\scr U}\vdash A\rightarrow A\)

2. \(n>1\)，因此 \({\scr U}\cup\left\{A\right\}\vdash B\) 是一个MP

   不妨设

   \[\begin{aligned} &{\scr U}\cup\left\{A\right\}\vdash C \\ &{\scr U}\cup\left\{A\right\}\vdash C\rightarrow B \end{aligned} \]

   上面两式根据归纳假设有

   \[\begin{aligned} &{\scr U}\vdash A\rightarrow C &\text{Deduction Rule} \\ &{\scr U}\vdash A\rightarrow (C\rightarrow B) &\text{Deduction Rule} \\ &{\scr U}\vdash (A\rightarrow (C\rightarrow B))\rightarrow ((A\rightarrow C)\rightarrow (A\rightarrow B)) &\textbf{Axiom 2} \\ &{\scr U}\vdash (A\rightarrow C)\rightarrow (A\rightarrow B) &\text{MP 2, 3} \\ &{\scr U}\vdash A\rightarrow B &\text{MP 1, 4} \end{aligned} \]

   故sound

Contrapositive Rule

\[\begin{aligned} \frac{{\scr U}\vdash\neg B\rightarrow \neg A}{{\scr U}\vdash A\rightarrow B} \end{aligned} \]

只需要用一下 \(\textbf{Axiom 3}\) 就可以得到的规则，注意这条规则和如下规则的区别：

\[\begin{aligned} \frac{{\scr U}\vdash A\rightarrow B}{{\scr U}\vdash \neg B\rightarrow \neg A} \end{aligned} \]

因为我们目前都只在语法层面操作公式，因此二者是有本质区别的规则，需要分别单独证明

Transitivity Rule

\[\frac{{\scr U}\vdash A\rightarrow B\;\;\;\;\;{\scr U}\vdash B\rightarrow C} {{\scr U}\vdash A\rightarrow C} \]

证明如下：

\[\begin{aligned} & {\scr U}\vdash A\rightarrow B \\ & {\scr U}\vdash B\rightarrow C \\ & {\scr U}\vdash (B\rightarrow C)\rightarrow(A\rightarrow (B\rightarrow C)) &\textbf{Axiom 1} \\ & {\scr U}\vdash A\rightarrow (B\rightarrow C) &\text{MP 2, 3} \\ & {\scr U}\vdash (A\rightarrow (B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow (A\rightarrow C)) &\textbf{Axiom 2} \\ & {\scr U}\vdash (A\rightarrow B)\rightarrow (A\rightarrow C) &\text{MP 4, 5} \\ & {\scr U}\vdash A\rightarrow C &\text{MP 1, 6} \end{aligned} \]

Exchange of antecedent Rule

\[\frac{{\scr U}\vdash A\rightarrow(B\rightarrow C)}{{\scr U}\vdash B\rightarrow (A\rightarrow C)} \]

证明如下：

\[\begin{aligned} & {\scr U}&\vdash& A\rightarrow(B\rightarrow C) \\ & {\scr U}\cup\left\{A\right\}&\vdash& B\rightarrow C &\text{Deduction Rule} \\ & {\scr U}\cup\left\{A,B\right\}&\vdash& C &\text{Deduction Rule} \\ & {\scr U}\cup\left\{B\right\}&\vdash& A\rightarrow C &\text{Deduction Rule} \\ & {\scr U}&\vdash& B\rightarrow(A\rightarrow C) &\text{Deduction Rule} \\ \end{aligned} \]

Double negation Rule

\[\frac{{\scr U}\vdash\neg\neg A}{{\scr U}\vdash A},\;\frac{{\scr U}\vdash A}{{\scr U}\vdash\neg\neg A} \]

证明如下：

引理：

\[\begin{aligned} & \left\{\neg\neg A\right\}&\vdash& \neg\neg A\rightarrow(\neg\neg\neg\neg A\rightarrow \neg\neg A) &\textbf{Axiom 1} \\ & \left\{\neg\neg A\right\}&\vdash& \neg\neg A \\ & \left\{\neg\neg A\right\}&\vdash& \neg\neg\neg\neg A\rightarrow \neg\neg A &\text{MP 1, 2} \\ & \left\{\neg\neg A\right\}&\vdash& \neg A\rightarrow \neg\neg\neg A &\text{Contrapositive Rule} \\ & \left\{\neg\neg A\right\}&\vdash& \neg\neg A\rightarrow A &\text{Contrapositive Rule} \\ & \left\{\neg\neg A\right\}&\vdash& A &\text{MP 2, 5} \\ & &\vdash& \neg\neg A\rightarrow A &\text{Deduction Rule} \end{aligned} \]

因此

\[\begin{aligned} & {\scr U}\vdash \neg\neg A \\ & {\scr U}\vdash \neg\neg A\rightarrow A \\ & {\scr U}\vdash A \end{aligned} \]

另一个的证明是类似的

Reductio ad absurdum

也就是所谓的排中律

即

\[\frac{{\scr U}\vdash \neg A\rightarrow false}{{\scr U}\vdash A} \]

规定 \(false \overset{def}=A\wedge\neg A\overset{def}=\neg(A\rightarrow A)\)，\(true\overset{def}=A\vee\neg A\overset{def}=A\rightarrow A\)，注意这是语法上的定义，即两侧可以等价替换。

那么有 \(\vdash \neg false\)，且 \(\vdash true\)，这个证明是显然的。

关于排中律的"证明"：

\[\begin{aligned} & {\scr U}\vdash \neg A\rightarrow false \\ & {\scr U}\vdash \neg false\rightarrow \neg\neg A &\text{Contrapositive Rule} \\ & {\scr U}\vdash \neg false &\text{By Lemma} \\ & {\scr U}\vdash \neg \neg A &\text{MP 2, 3} \\ & {\scr U}\vdash A &\text{Double negation Rule} \end{aligned} \]

在某些逻辑里，\(\vdash A\vee\neg A\) 是可以不成立的。比如说Constructive Logic里就没法通过反证法证明一个东西，你必须提供一个构造才能说明某些存在性。在这里不是重点

先去吃饭，咕咕咕