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

写在前面

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

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 系统的（语法）定义

公理

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

推演规则

有两类规则 $$ \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$ 这个树形结构做结构归纳

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$，分类讨论：

3. $\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$ 为其它情况的证明是类似的。

1. $\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}$
3. $\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$ 的证明是类似的。
4. $\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}

\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$

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

这条规则就反映了拓展证明的意图，这条规则保证了我们可以在证明 $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} \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$

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

不妨设 \begin{aligned} \begin{aligned} &{\scr U}\cup\left{A\right}\vdash C
&{\scr U}\cup\left{A\right}\vdash C\rightarrow B \end{aligned} \end{aligned} 上面两式根据归纳假设有 \begin{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} \end{aligned} 故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$，因为所有后面的定理和规则都可以规约回去。

1. $n=1$，此时 $A$ 是三公理之一，构建 $\neg A$ 的Semantic Tableaux即可发现都是closed的，因此 $\models A$

2. $n>1$，此时 $A$ 经由MP得到，前面必然有 $\vdash B\rightarrow A$，$\vdash B$。根据归纳假设有 $\models B\rightarrow A$，$\models B$，根据 $\rightarrow $ 的语义即得 $\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$ 中的推导用结构归纳法：

1. $\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$

2. $\scr U$ 在 $\scr G$ 中经过至少一步推导得到，不妨记新增公式为 $\phi$，记 ${\scr U}=\left{\phi\right}\cup {\scr V}$

3. $\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$

4. $\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}$ 的特殊结构使得它的完全性证明可以比较简单地由归纳得到。因此这里实际上是走了一个小捷径的。

利用一致性可以给出完全性的另一定义，即下列命题等价：

1. 若 $\Gamma$ 一致则 $\Gamma$ 可满足
2. 若 $\Gamma\models \phi$ 则 $\Gamma\vdash\phi$

因此完全性证明只需要针对(1)的情况即可。 假定有一个一致的公式集 $\Gamma$，我们可以通过一些手段对其扩充，得到极大一致的公式集 $\Gamma’$。 然后我们根据 $\Gamma’$ 可以构造一个赋值/指派，从而可以证明 $\Gamma’$ 在这个赋值下可满足，自然有 $\Gamma$ 可满足，于是命题得证。