写在前面
在上一章给出了命题逻辑的语法、语义，公理化的定义，以及一种判定公式是否可满足/永真的算法，但是这还不够，因为：
并不是所有逻辑都有Decision Procedure，因此这种方法不够普遍
即使有，在有无穷多的公理时，Decision Procedure很可能没法处理无穷项的公式（算法不一定终止）
即使终止，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\}\)
要么是公理
要么可以由前面的公式+推演规则得到
要么是前面出现过的公式
要么是已经证明过的定理
用 \(\vdash A\) 表示 \(A\) 在推演系统中可证明，即存在一个证明使得 \(A\) 是最后出现的公式，称 \(A\) 为一个定理（Theorem）。对于中间出现的公式我们称为引理（Lemma）。
\(\scr G\)
给出 Gentzen 系统的（语法）定义
公理
含有互补对的公式集是公理
推演规则
有两类规则 $$ \[\begin{align*} &\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\} } \end{align*}\] $$ 一个常见的例子是令 \(\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\) 这个树形结构做结构归纳
\(\scr\bar V\) 是 \(\scr T\) 的叶子，则其存在互补对，此时 \(\scr V\) 也存在互补对，因此 \(\scr V\) 是 \(\scr G\) 中的公理，\(\vdash\scr V\)
\(\scr\bar V\) 不是 \(\scr T\) 的叶子，不妨设 \(\scr\bar V\) 中的新增公式为 \(\phi\)，分类讨论：
\(\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\) 为其它情况的证明是类似的。
- \(\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\) 做结构归纳
\(\scr U\) 是 \(\scr G\) 中的公理，故存在互补对，此时 \(\scr\bar U\) 也存在互补对，故 \(\scr\bar U\) 必然构造出 \(\scr T\)
\(\scr U\) 经推导而来，不妨记新增公式为 \(\phi\)，记 \({\scr U}={\scr U'}\cup\left\{\phi\right\}\)
\(\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\) 的证明是类似的。
\(\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}\]$$
推演规则
只有一条
$$ \[\begin{aligned} \frac{\vdash A\;\;\;\vdash A\rightarrow B}{\vdash B} \end{aligned}\]$$ 也叫做肯定前件（modus ponens），记为MP
对证明的拓展
设 \(\scr U\) 是公式集，\(A\) 是某个公式，则符号 \({\scr U}\vdash A\) 表示 \(\scr U\) 中的公式是证明 \(A\) 的假设
\(\scr H\) 中的证明是一系列形如 \({\scr U_i}\vdash A_i\) 的公式，其中 \(A_i\)
要么是公理
要么是已经证明过的引理
\(A_i\in {\scr U_i}\)
可由已经证明过的定理+MP得到
这一拓展反映的是证明形如“如果 \(A\) 那么 \(B\) ”的命题时，我们可以假设 \(A\) 成立，然后检查 \(B\) 是否可被证明。
衍生规则
虽然只有MP是足够的，但是只用MP就像在裸奔，因此需要包装MP和公理来得到一些更抽象的推演规则。We are now doing composition!
具体可以把这些规则看成是一些语法上的宏，展开就能得到纯MP和公理组成的推演规则。
Deduction Rule
$$ \[\begin{aligned} \frac{ {\scr U}\cup \left\{A\right\}\vdash B}{ {\scr U}\vdash A\rightarrow B} \end{aligned}\]$$
这条规则就反映了拓展证明的意图，这条规则保证了我们可以在证明 \(A\rightarrow B\) 时先假设 \(A\)，再证明 \(B\)
下面需要证明拓展是sound的，即不会引入原本不能证明的命题。其completeness是显然的。
对 \({\scr U}\cup\left\{A\right\}\vdash B\) 的推导步骤数 \(n\) 作数学归纳法
- \(n=1\)，此时 \(B\) 一步就得到了，因此 \(B\) 要么是公理，要么是 \(A\)，要么是已经证过的定理，下面给出 \(B\neq A\) 的证明： \[\begin{aligned} \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} \end{aligned}\] 故sound
当 \(A=B\)，该命题退化为 \({\scr U}\vdash A\rightarrow A\)
- \(n>1\)，因此 \({\scr U}\cup\left\{A\right\}\vdash B\) 是一个MP
故sound
Contrapositive Rule
\[\begin{aligned} \begin{aligned} \frac{ {\scr U}\vdash\neg B\rightarrow \neg A}{ {\scr U}\vdash A\rightarrow B} \end{aligned} \end{aligned}\]只需要用一下 \(\textbf{Axiom 3}\) 就可以得到的规则，注意这条规则和如下规则的区别：
\[\begin{aligned} \begin{aligned} \frac{ {\scr U}\vdash A\rightarrow B}{ {\scr U}\vdash \neg B\rightarrow \neg A} \end{aligned} \end{aligned}\]因为我们目前都只在语法层面操作公式，因此二者是有本质区别的规则，需要分别单独证明
Transitivity Rule
\[\begin{aligned} \frac{ {\scr U}\vdash A\rightarrow B\;\;\;\;\;{\scr U}\vdash B\rightarrow C} { {\scr U}\vdash A\rightarrow C} \end{aligned}\]证明如下：
\[\begin{aligned} \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} \end{aligned}\]Exchange of antecedent Rule
\[\begin{aligned} \frac{ {\scr U}\vdash A\rightarrow(B\rightarrow C)}{ {\scr U}\vdash B\rightarrow (A\rightarrow C)} \end{aligned}\]证明如下：
\[\begin{aligned} \begin{aligned} & \left\{A\rightarrow(B\rightarrow C),A,B\right\}\vdash A\rightarrow(B\rightarrow C) \\ & \left\{A\rightarrow(B\rightarrow C),A,B\right\}\vdash A \\ & \left\{A\rightarrow(B\rightarrow C),A,B\right\}\vdash B\rightarrow C \\ & \left\{A\rightarrow(B\rightarrow C),A,B\right\}\vdash B \\ & \left\{A\rightarrow(B\rightarrow C),A,B\right\}\vdash C \\ & \left\{A\rightarrow(B\rightarrow C),B\right\}\vdash A\rightarrow C \\ & \left\{A\rightarrow(B\rightarrow C)\right\}\vdash B\rightarrow(A\rightarrow C) \\ & \vdash (A\rightarrow(B\rightarrow C))\rightarrow(B\rightarrow(A\rightarrow C)) \end{aligned} \end{aligned}\]然后用这条定理对着前件MP一下就好了
Double negation Rule
\[\begin{aligned} \frac{ {\scr U}\vdash\neg\neg A}{ {\scr U}\vdash A},\;\frac{ {\scr U}\vdash A}{ {\scr U}\vdash\neg\neg A} \end{aligned}\]证明如下：
引理：
\[\begin{aligned} \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} \end{aligned}\]因此
\[\begin{aligned} \begin{aligned} & {\scr U}\vdash \neg\neg A \\ & {\scr U}\vdash \neg\neg A\rightarrow A \\ & {\scr U}\vdash A \end{aligned} \end{aligned}\]另一个的证明是类似的
Reductio ad absurdum
也就是所谓的归谬法
即
\[\begin{aligned} \frac{ {\scr U}\vdash \neg A\rightarrow false}{ {\scr U}\vdash A} \end{aligned}\]规定 \(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} \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} \end{aligned}\]Commutativity
\[\begin{aligned} \vdash A\vee B\rightarrow B\vee A \end{aligned}\]在 \(\scr H\) 中没有对 \(\vee \wedge\) 的直接讨论，通常通过定义 \(A\vee B\overset{def}= \neg A\rightarrow B\) 和 \(A\wedge B\overset{def}= \neg(A\rightarrow \neg B)\) 来将其转化为 \(\neg \rightarrow\) 符号集上的证明。这也说明了 \(\left\{\neg,\rightarrow\right\}\) 是完备集
交换律的证明是简单的，但是后面 \(\scr H\) 的正确性证明需要用到这个。
Weakening
\[\begin{aligned} \begin{aligned} &\vdash A\rightarrow A\vee B \\ &\vdash A\rightarrow B\vee A \\ &\vdash (A\rightarrow B)\rightarrow((C\vee A)\rightarrow(C\vee B)) \end{aligned} \end{aligned}\]证明也是简单的，只需要按定义换掉 \(\vee\) 就可以了，第三条是MP的简单应用
Associativity
\[\begin{aligned} \begin{aligned} &\vdash A\vee(B\vee C)\rightarrow (A\vee B)\vee C \\ &\vdash (A\vee B)\vee C\rightarrow A\vee(B\vee C) \end{aligned} \end{aligned}\]证明需要用一下交换律，然后推就好了
Distributivity
\[\begin{aligned} \begin{aligned} &\vdash A\vee(B\wedge C)\leftrightarrow (A\vee B)\wedge (A\vee C) \\ &\vdash A\wedge(B\vee C)\leftrightarrow (A\wedge B)\vee (A\wedge C) \end{aligned} \end{aligned}\]这里规定 \(\vdash A\leftrightarrow B\) 当且仅当 \(\vdash A\rightarrow B\) 且 \(\vdash B\rightarrow A\)
这里是 \(\scr H\) 中语法上的De morgan Law，在没有证明 \(\scr H\) 的正确性之前是不能由语义上得到的。
这个本菜菜还没想到要怎么证，好像也没找到要怎么证/(ㄒoㄒ)/
\(\scr H\) 的正确性
Soundness
对于 \(A\in{\scr H}\)，若 \(\vdash A\)，那么 \(\models A\)
即证明所有 \(\scr H\) 可证明的公式都永真，只需要对 \(A\) 的证明步骤数 \(n\) 做归纳即可。这里可以仅考虑原始的三条公理+MP的 \(\scr H\)，因为所有后面的定理和规则都可以规约回去。
\(n=1\)，此时 \(A\) 是三公理之一，构建 \(\neg A\) 的Semantic Tableaux即可发现都是closed的，因此 \(\models A\)
\(n>1\)，此时 \(A\) 经由MP得到，前面必然有 \(\vdash B\rightarrow A\)，\(\vdash B\)。根据归纳假设有 \(\models B\rightarrow A\)，\(\models B\)，根据 $$ 的语义即得 \(\models A\)。注意我们这里在讨论 \(\models\)，因此可以用语义上的定义来进行证明。
Completeness
对于 \(A\in{\scr H}\)，若 \(\models A\)，那么 \(\vdash A\)。注意到 \(\scr G\) 是sound&complete的，因此可以通过 \(\scr G\) 作为媒介证明
引理1：若 \(\vdash{\scr U}\) in \(\scr G\)，那么 \(\vdash \bigvee{\scr U}\) in \(\scr H\)
理解引理1是很简单的，只需要注意到 \(\scr G\) 中的定理是一个隐含的 \(\bigvee\) 公式，同时结合 \(\vdash A\) 当且仅当 \(\models A\) in \(\scr G\) 就好了。
引理2：若 \({\scr U'}\subseteq{\scr U}\)，\(\vdash \bigvee{\scr U'}\) in \(\scr H\)，那么 \(\vdash\bigvee{\scr U}\) in \(\scr H\)
之所以提出引理2是因为我们很难直接获得整个公式集 \(\scr U\) 构成的公式在 \(\scr H\) 中的推导。但是注意到 \(\scr G\) 中的公理都有互补对，而互补对是我们可以在 \(\scr H\) 中推导的，因此考虑证明这个弱化前提的引理2。
引理3：\(\vdash A\rightarrow(B\rightarrow A\wedge B)\)
引理2的证明：
由 \(\vdash\bigvee{\scr U'}\)，可以得到 \(\scr H\) 中的一个证明。又根据 Weakening Theorem，可以将 \(\scr U-\scr U'\) 中的公式一个个加上得到 \(\vdash\bigvee{\scr U''}\)，其中 \(\bigvee\scr U''\) 是 \(\bigvee\scr U\) 的一个排列，这一步可以对 \(|\scr U-U'|\) 作数学归纳法。
又根据 Commutativity Theorem可以交换 \(\bigvee\scr U''\) 中的任意两个相邻的公式，因此可以排序得到 \(\vdash\bigvee\scr U\)，这一步可以给公式编号，然后对逆序对作数学归纳法。
引理1的证明可以对 \(\scr U\) 在 \(\scr G\) 中的推导用结构归纳法：
\(\scr U\) 是 \(\scr G\) 中公理，因此存在 \({\scr U'}=\left\{p,\neg p\right\}\subseteq{\scr U}\)。此时显然有 \(\vdash\bigvee \scr U'\) in \(\scr H\)，根据引理2就有 \(\vdash\bigvee \scr U\) in \(\scr H\)
\(\scr U\) 在 \(\scr G\) 中经过至少一步推导得到，不妨记新增公式为 \(\phi\)，记 \({\scr U}=\left\{\phi\right\}\cup {\scr V}\)
\(\phi=\alpha_1\vee\alpha_2\)，记 \({\scr U_1}={\scr V}\cup\left\{\alpha_1,\alpha_2\right\}\)，则根据归纳假设有 \(\vdash\bigvee{\scr U_1}\) in \(\scr H\)，也就是 \(\vdash(\bigvee{\scr V})\vee\alpha_1\vee\alpha_2\)。根据 Associativity Theorem即得 \(\vdash(\bigvee{\scr V})\vee(\alpha_1\vee\alpha_2)\)，也就是 \(\vdash\bigvee\scr U\) in \(\scr H\)
\(\phi=\beta_1\wedge\beta_2\)，记\({\scr U_1}={\scr V_1}\cup\left\{\beta_1\right\}\)，记 \({\scr U_2}={\scr V_2}\cup\left\{\beta_2\right\}\)，则根据归纳假设有 \(\vdash\bigvee{\scr U_1},\;\vdash\bigvee{\scr U_2}\) in \(\scr H\)，也就是 \(\vdash(\bigvee{\scr V_1})\vee\beta_1,\;\vdash(\bigvee{\scr V_2})\vee\beta_2\)
\[\begin{aligned} \begin{aligned} & \vdash \bigvee{\scr V_1}\vee\beta_1 \\ & \vdash \neg\bigvee{\scr V_1}\rightarrow \beta_1&\text{By Definition of $\vee$} \\ & \vdash \beta_1\rightarrow(\beta_2\rightarrow\beta_1\wedge\beta_2)&\text{Lemma 3} \\ & \vdash \neg\bigvee{\scr V_1}\rightarrow(\beta_2\rightarrow \beta_1\wedge\beta_2)&\text{By Transitivity} \\ & \vdash \beta_2\rightarrow(\neg\bigvee{\scr V_1}\rightarrow\beta_1\wedge\beta_2)&\text{Exchange of Antecedent Rule} \\ & \vdash \bigvee{\scr V_2}\vee\beta_2&\text{} \\ & \vdash \neg\bigvee{\scr V_2}\rightarrow\beta_2&\text{By Definition of $\vee$} \\ & \vdash \neg\bigvee{\scr V_2}\rightarrow(\neg\bigvee{\scr V_1}\rightarrow\beta_1\wedge\beta_2)&\text{By Transitivity} \\ & \vdash (\bigvee{\scr V_2})\vee(\bigvee{\scr V_1})\vee(\beta_1\wedge\beta_2)&\text{By Definition of $\vee$} \end{aligned} \end{aligned}\]这样就证明了 \(\vdash \scr U\) in \(\scr H\)
最后考虑怎么证明 \(\models A\) 则 \(\vdash A\) in \(\scr H\)
构造 \({\scr U}=\left\{A\right\}\)，\(\models A\) 当且仅当 \(\vdash \scr U\) in \(\scr G\) 当且仅当 \(\vdash \bigvee\scr U\) in \(\scr H\) 当且仅当 \(\vdash A\) in \(\scr G\)
于是就证明了 \(\scr H\) 是Sound & Complete的
一致性
称公式集 \(\scr U\) 是不一致的，当且仅当存在公式 \(A\) 使得 \({\scr U}\vdash A\) 并且 \({\scr U}\vdash \neg A\)
称 \(\scr U\) 是一致的，当且仅当它不是不一致的
若 \(\scr U\) 是不一致的，那么对于任意公式 \(A\) 都有 \({\scr U}\vdash A\)
证明就不写了咕咕咕咕
由此可以得到一个很有用的定理，\({\scr U}\vdash A\) 当且仅当 \({\scr U}\cup\left\{\neg A\right\}\) 不一致
Consistency & Completeness
前文关于命题逻辑 \({\scr H}\) 的完全性证明依赖于 \({\scr G}\) 的完全性证明，而 \({\scr G}\) 的特殊结构使得它的完全性证明可以比较简单地由归纳得到。因此这里实际上是走了一个小捷径的。
利用一致性可以给出完全性的另一定义，即下列命题等价：
- 若 \(\Gamma\) 一致则 \(\Gamma\) 可满足
- 若 \(\Gamma\models \phi\) 则 \(\Gamma\vdash\phi\)
因此完全性证明只需要针对(1)的情况即可。 假定有一个一致的公式集 \(\Gamma\)，我们可以通过一些手段对其扩充，得到极大一致的公式集 \(\Gamma'\)。 然后我们根据 \(\Gamma'\) 可以构造一个赋值/指派，从而可以证明 \(\Gamma'\) 在这个赋值下可满足，自然有 \(\Gamma\) 可满足，于是命题得证。