参考资料：Basic Proof Theory (Troelstra, Schwichtenberg), Proof Theory (Takeuti).

一阶逻辑

一阶逻辑语言 $L$$L$ 中包含如下内容。

• 一些（甚至可能是 $0$$0$ 个）常量；

• 一些（同上）常函数；

• 一些（同上）常谓词；

• "总是够用"个（我们最好还是暂时回避基数问题）自由变量；

• "总是够用"个受限变量；

• 逻辑连接词 $\mathrm{\neg },\vee ,\wedge ,\supset$$\lnot,\lor,\land,\supset$ 等；（其中 $\supset$$\supset$ 表示蕴含）

• 量词 $\mathrm{\forall },\mathrm{\exists }$$\forall,\exists$。

如果给定所有的常量，一个语言系统也就给定了。因此有时候在语言系统不变的情况下我们有时省略"在 $L$$L$ 中"这样的表述。

• 任何一个符号列被称为（$L$$L$ 中）的一个表达式。

• 常量、自由变量和常函数（及其可能的复合）组成的表达式被称为项。更准确来说：

• • 常量、自由变量是项。

  • 如果 $t_i$$t_i$ 都是项，那么形如 $f(t_1,\dots ,t_n)$$f(t_1,\ldots,t_n)$（其中 $f$$f$ 是常函数）的表达式也是项。

  • 项只能通过以上两种方法得到。（即项的定义是归纳的）

• 如果 $t_i$$t_i$ 都是项，那么形如 $R(t_1,\dots ,t_n)$$R(t_1,\ldots,t_n)$（其中 $R$$R$ 是常谓词）的表达式是原子命题。

• • 原子命题是命题。

  • 命题的逻辑连接是命题。

  • 如果 $A$$A$ 是命题，$x$$x$ 是一个不在 $A$$A$ 中的受限变量，那么记 $A^{\prime }$$A'$ 是 $A$$A$ 中的 $a$$a$（一个自由变量）替换为 $x$$x$ 得到的结果；形如 $\mathrm{\forall }x{A}^{\prime }$$\forall xA'$ 和 $\mathrm{\exists }x{A}^{\prime }$$\exists x A'$ 的表达式是命题。

  • 命题只能通过以上三种方法得到。

• 定义 $\left(A{\displaystyle \frac{{\tau }_1\dots {\tau }_n}{{\sigma }_1\dots {\sigma }_n}}\right)$$\left(A\dfrac{\tau_1\ldots\tau_n}{\sigma_1\ldots\sigma_n}\right)$ 是在 $A$$A$ 中把（自由变量）${\tau }_i$$\tau_i$ 替换为（项）${\sigma }_i$$\sigma_i$ 得到的结果。

• • 对于 $A=\left(B{\displaystyle \frac{b}{a}}\right)$$A=\left(B\dfrac{b}{a}\right)$，如果 $A$$A$ 中 $a$$a$ 的每一次出现都是替换得来（换言之 $a$$a$ 不出现在 $B$$B$ 中），那么称 $a$$a$ 在 $A$$A$ 中（相对于 $B$$B$）充分表现了。

列演算 / 推理

下面我们把一排命题 $A_1,A_2,\dots ,A_n$$A_1,A_2,\ldots,A_n$ 简记为 $\mathrm{\Gamma },\mathrm{\Delta }$$\Gamma,\Delta$ 等。如果 $\mathrm{\Gamma },\mathrm{\Delta }$$\Gamma,\Delta$ 都是如上的这种东西，形如 $\mathrm{\Gamma }\to \mathrm{\Delta }$$\Gamma\rightarrow \Delta$ 的东西被称为一个列。

• $A\to B$$A\rightarrow B$ 可以（直觉地）理解为"$A$$A$ 推出 $B$$B$"。（请注意把逻辑连接词 $\supset$$\supset$ 和列演算中的符号 $\to$$\rightarrow$ 区别开来。）

• $A_1,A_2,\dots ,A_n\to B_1,B_2,\dots ,B_m$$A_1,A_2,\ldots,A_n\rightarrow B_1,B_2,\ldots,B_m$ 可以（直觉地）理解为 $A_1\wedge A_2\wedge \dots \wedge A_n$$A_1\land A_2\land\ldots\land A_n$ 推出 $B_1\vee B_2\vee \dots \vee B_m$$B_1\lor B_2\lor\ldots\lor B_m$。

• 特别地，记 $\mathrm{\Gamma }\to$$\Gamma\rightarrow$ 表示 $\mathrm{\Gamma }$$\Gamma$ 推出矛盾。

• 特别地，记 $\to \mathrm{\Delta }$$\rightarrow\Delta$ 表示 $\mathrm{\Delta }$$\Delta$ 不证自明。

虽说 $A\to B$$A\rightarrow B$ 看上去和听起来都很像一个命题（尤其是许多地方喜欢把逻辑连接词"蕴含"记作 $\to$$\rightarrow$），但我们最好还是别把它们搞混。

记 $S,S_1,S_2$$S,S_1,S_2$ 等为列。形如下的东西被称为一个推理。

（直觉地）这表示如果假设 $S_1,S_2$$S_1,S_2$，那么可以推理出 $S$$S$。

但是这并没有告诉我们什么推理是合法的，什么推理是不合法的。一组推理规则被称为列演算。

下面我们介绍其中一种由 Gentzen 提出的列演算：LK 系统，Logistische Kalkül（逻辑演算）。

以下是几条（LK 系统中）无聊的结构性推理规则。

1.1) 弱化律

$${\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta }}{D,\mathrm{\Gamma }\to \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\Gamma }\to \mathrm{\Delta },D}}$$

1.2) 压缩律

$${\displaystyle \frac{D,D,\mathrm{\Gamma }\to \mathrm{\Delta }}{D,\mathrm{\Gamma }\to \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },D,D}{\mathrm{\Gamma }\to \mathrm{\Delta },D}}$$

1.3) 交换律

$${\displaystyle \frac{\mathrm{\Gamma },C,D,\mathrm{\Pi }\to \mathrm{\Delta }}{\mathrm{\Gamma },D,C,\mathrm{\Pi }\to \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },C,D,\mathrm{\Lambda }}{\mathrm{\Gamma }\to \mathrm{\Delta },D,C,\mathrm{\Lambda }}}$$

以下是唯一一条不无聊的结构性推理规则。记住它。

1.4) 切割律

$${\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },DD,\mathrm{\Pi }\to \mathrm{\Lambda }}{\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Delta },\mathrm{\Lambda }}}$$

以下是几条因为太直观而无聊的逻辑性推理规则。

2.1) $\mathrm{\neg }$$\lnot$ 律

$${\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },D}{\mathrm{\neg }D,\mathrm{\Gamma }\to \mathrm{\Delta }}}{\displaystyle \frac{D,\mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\Gamma }\to \mathrm{\Delta },\mathrm{\neg }D}}$$

2.2) $\wedge$$\land$ 律

$${\displaystyle \frac{C,\mathrm{\Gamma }\to \mathrm{\Delta }}{C\wedge D,\mathrm{\Gamma }\to \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },C\mathrm{\Gamma }\to \mathrm{\Delta },D}{\mathrm{\Gamma }\to \mathrm{\Delta },C\wedge D}}$$

2.3) $\vee$$\lor$ 律

$${\displaystyle \frac{C,\mathrm{\Gamma }\to \mathrm{\Delta }D,\mathrm{\Gamma }\to \mathrm{\Delta }}{C\vee D,\mathrm{\Gamma }\to \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },C}{\mathrm{\Gamma }\to \mathrm{\Delta },C\vee D}}$$

2.4) $\supset$$\supset$ 律

$${\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },CD,\mathrm{\Pi }\to \mathrm{\Lambda }}{C\supset D,\mathrm{\Gamma },\mathrm{\Pi }\to \mathrm{\Delta },\mathrm{\Lambda }}}{\displaystyle \frac{C,\mathrm{\Gamma }\to \mathrm{\Delta },D}{\mathrm{\Gamma }\to \mathrm{\Delta },C\supset D}}$$

以下是两条不那么容易理解的逻辑性推理规则。

2.5) $\mathrm{\forall }$$\forall$ 律

$${\displaystyle \frac{F(t),\mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\forall }xF(x),\mathrm{\Gamma }\to \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },F(a)}{\mathrm{\Gamma }\to \mathrm{\Delta },\mathrm{\forall }xF(x)}}$$

其中 $t$$t$ 是任意项；$a$$a$ 不出现在推理的下一行。

更具体来说，记号 $F(t)$$F(t)$ 是 $\left(F{\displaystyle \frac{a}{t}}\right)$$\left(F\dfrac{a}{t}\right)$，要保证 $a$$a$ 不出现在推理的下一行。

看起来很没道理，为啥 $F(a)$$F(a)$ 能推出对所有 $x$$x$ 都成立？因为 $a$$a$ 不出现在其他任何地方，因此它应当被理解为 $F$$F$ 对任意选取的 $a$$a$ 都成立，也就直接是 $\mathrm{\forall }xF(x)$$\forall xF(x)$。

这里 $a$$a$ 被称为特征变量。

2.6) $\mathrm{\exists }$$\exists$ 律

$${\displaystyle \frac{F(a),\mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\exists }xF(x),\mathrm{\Gamma }\to \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\to \mathrm{\Delta },F(t)}{\mathrm{\Gamma }\to \mathrm{\Delta },\mathrm{\exists }xF(x)}}$$

其中 $t$$t$ 是任意项；$a$$a$ 不出现在推理的下一行。

这里 $a$$a$ 也被称为特征变量。

还有一种类似的逻辑系统，被称为 LJ 系统，代表了直觉主义逻辑。LJ 和 LK 在很大程度上都是相同的，但是 $\to$$\rightarrow$ 右侧只允许有一个命题。（因此，右压缩律和右交换律没有意义。）

比如，在 LK 中我们可以有

但 LJ 中就不可能有如此证明。

不过话说回来却有

太怪了。

形式化证明

一个 LK 中的证明 $P$$P$ 是一个满足如下要求的（有限）演算树：

• 最顶上的（叶子节点）列总是形如 $A\to A$$A\rightarrow A$（称为初始列，或公理）；

• 除了根（称为终列）以外，每个列都是所在推理的依据；该推理的结论也总是在 $P$$P$ 中。

如果（在 LK 中）存在一个终列为 $S$$S$ 的证明，则称 $S$$S$ 在 LK 中是可证的，记为 $\mathsf{LK}⊢S$$\mathsf{LK}\vdash S$。如果 $\mathsf{LK}⊢\to A$$\mathsf{LK}\vdash \rightarrow A$，那么称命题 $A$$A$ 在 LK 中是可证的。

定义一个 LK-证明 是正则的，当且仅当：

• 所用的特征变量互不相同；

• 一个 $a$$a$ 如果作为特征变量出现，那么它只在对应的子树里被用到。

十分合理的要求。可以让我们避免很多麻烦。

• 如果 $\mathrm{\Gamma }(a)\to \mathrm{\Delta }(a)$$\Gamma(a)\rightarrow\Delta(a)$ 中 $a$$a$ 充分表现，而 $P(a)$$P(a)$ 是一个它的证明，那么择取一个在 $P(a)$$P(a)$ 中没有出现过的自由变元 $b$$b$，那么把 $P(a)$$P(a)$ 中的每个命题都把 $a$$a$ 替换为 $b$$b$ 所得到的 $P(b)$$P(b)$ 也是一个合法的证明，而且结论为 $\mathrm{\Gamma }(b)\to \mathrm{\Delta }(b)$$\Gamma(b)\rightarrow\Delta(b)$。

• • 归纳即可。

由此得到一个很好的性质：对于任意的 LK-证明，总存在一个与其结论相同的正则 LK-证明。仍是直接归纳即可证明。从此我们总是假设我们谈论的证明是正则的。

用相同方法还可以得到一个关于把变元替换为项的引理。

• 令 $t$$t$ 是一个项。如果 $\mathrm{\Gamma }(a)\to \mathrm{\Delta }(a)$$\Gamma(a)\rightarrow\Delta(a)$ 中 $a$$a$ 充分表现，而 $P(a)$$P(a)$ 是一个它的证明，且 $a$$a$ 没有作为特征变元出现过，那么我们可以把 $P(a)$$P(a)$ 替换为一个特征变元皆没有在 $t$$t$ 中使用过的版本 $P^{\prime }(a)$$P'(a)$。$P^{\prime }(t)$$P'(t)$ 仍是一个合法的证明。

（我靠变量替换这玩意简直是万恶之源，就不能用更文明优雅的、天然地解决了变量的作用范围的 lambda 演算吗？？？）

最后给出两个小性质。

• 如果某列是可证明的，那么它也一定可以从原子命题的公理开始证明。

• • 因为很显然任何逻辑链接都可以通过对应的推理规则构造。

• 如果某列是可以不通过切割律证明的，那么它也一定可以从原子命题的公理开始不通过切割律地证明。

• • 同上。

所以我们到底为什么这么关注切割律？这个问题还留待以后解答。

公理系统

我们以 LK 为基础推理系统。

可以发现 LK 中暂时只有无聊的重言式 $A\to A$$A\rightarrow A$ 作为推理基础。下面定义的公理系统将解决这个问题。

• 一组无自由变元的命题的集合 $\mathcal{A}$$\mathscr A$ 被称作一个公理系统 / 理论；其中的命题称为公理。

• 如果 $\mathcal{A}$$\mathscr A$ 中的一排公理 ${\mathrm{\Gamma }}_0$$\Gamma_0$ 使得 ${\mathrm{\Gamma }}_0,\mathrm{\Gamma }\to \mathrm{\Delta }$$\Gamma_0,\Gamma\rightarrow\Delta$ 在 LK 中可证，那么称 $\mathrm{\Gamma }\to \mathrm{\Delta }$$\Gamma\rightarrow\Delta$ 是（在 LK 中）可由 $\mathcal{A}$$\mathscr A$ 证明的，记为 $\mathcal{A}{⊢}_{\mathsf{LK}}\mathrm{\Gamma }\to \mathrm{\Delta }$$\mathscr A\vdash_{\mathsf{LK}}\Gamma\rightarrow\Delta$。

• 如果空列 $\to$$\rightarrow$（即矛盾）是可由 $\mathcal{A}$$\mathscr A$ 证明的，那么称 $\mathcal{A}$$\mathscr A$ 是不一致的。否则称其为一致的。

• 一个无自由变元的命题 $A$$A$ 被称为（不）一致的当且仅当公理系统 $\{A\}$$\{A\}$ 是（不）一致的。

容易证明以下三个命题是等价的：

• $\mathcal{A}$$\mathscr A$ 是不一致的；

• 任何命题 $A$$A$ 都可由 $\mathcal{A}$$\mathscr A$ 证明；（被称为 ex falso sequitur quodlibet，得到 $\to$$\rightarrow$ 就啥都有了）

• 对于某命题 $A$$A$，$A$$A$ 和 $\mathrm{\neg }A$$\lnot A$ 都可有 $\mathcal{A}$$\mathscr A$ 证明。

还有一个容易证明的小性质：

• 一个列可由 $\mathcal{A}$$\mathscr A$ 证明，当且仅当在 LK 中加入所有 $\to (A\in \mathcal{A})$$\rightarrow (A\in\mathscr A)$ 作为推理基础可证该列。

（提示：切割律。）

也就是说这两种公理系统的定义是等价的，以后我们不区分它们而是都记得到的新推理系统为 LK${}_{\mathcal{A}}$$_{\mathscr A}$。

消除切割定理 / Gentzen 主定理

定理.

一个列是 LK 可证的，那么从 LK 中删去切割律它仍可证。

这部分有繁琐且套娃的归纳、无穷无尽的分讨、一大堆一次性用完即抛的概念而且这一切根本就没人关心。因此我们将跳过证明。对于证明过程我们只需指出：

• 这个证明是构造性的。我们归纳地构造了一个新的不用切割的证明。

• 证明依赖于 ${\omega }^2$$\omega^2$ 的超限归纳。（归纳套娃）

这个定理的应用更为关键。

注意到，去除切割律之后，证明的每一步总是把列变得更复杂（命题不会凭空消失）。因此，证明 $\to A$$\rightarrow A$ 总是只可能用到 $A$$A$ 表达式树中的子命题。因此，

定理.

LK 一致。

（即 $\to$$\rightarrow$ 在 LK 中不可证）

应用消除切割定理还可以得到一个重要的引理和一堆衍生物。

引理.

记在 LK 中加入无参数常谓词 $\mathrm{\top }$$\top$ 和公理 $\to \mathrm{\top }$$\rightarrow \top$（即加入真值常谓词）得到的系统为 $\mathsf{LK}\mathrm{♯}$$\mathsf{LK}\sharp$。

令 $\mathrm{\Gamma }\to \mathrm{\Delta }$$\Gamma\rightarrow\Delta$ LK 可证，而 ${\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2$$\Gamma_1,\Gamma_2$ 和 ${\mathrm{\Delta }}_1,{\mathrm{\Delta }}_2$$\Delta_1,\Delta_2$ 分别是 $\mathrm{\Gamma }$$\Gamma$ 和 $\mathrm{\Delta }$$\Delta$ 的划分（可以为空），记为 $[\{{\mathrm{\Gamma }}_1;{\mathrm{\Delta }}_1\},\{{\mathrm{\Gamma }}_2;{\mathrm{\Delta }}_2\}]$$[\{\Gamma_1;\Delta_1\},\{\Gamma_2;\Delta_2\}]$。

那么总存在命题 $C$$C$（称为这对划分的插值）满足

• ${\mathrm{\Gamma }}_1\to {\mathrm{\Delta }}_1,C$$\Gamma_1\rightarrow\Delta_1,C$ 和 $C,{\mathrm{\Gamma }}_2\to {\mathrm{\Delta }}_2$$C,\Gamma_2\rightarrow \Delta_2$ 都 $\mathsf{LK}\mathrm{♯}$$\mathsf{LK}\sharp$ 可证；

• $C$$C$ 中所有自由变元、常变元、除 $\mathrm{\top }$$\top$ 之外的常谓词都在 $({\mathrm{\Gamma }}_1\cup {\mathrm{\Delta }}_1)\cap ({\mathrm{\Gamma }}_2\cup {\mathrm{\Delta }}_2)$$(\Gamma_1\cup\Delta_1)\cap(\Gamma_2\cup\Delta_2)$ 中。

证明.

对（无切割）证明 $\mathrm{\Gamma }\to \mathrm{\Delta }$$\Gamma\rightarrow\Delta$ 所需步数进行归纳即可。

特别关注归纳基础，即无需任何推理的情况：那么 $\mathrm{\Gamma }\to \mathrm{\Delta }$$\Gamma\rightarrow\Delta$ 必形如 $D\to D$$D\rightarrow D$。分割只有四种情况，每一种的 $C$$C$ 都是显然的：$\mathrm{\top },\mathrm{\neg }\mathrm{\top },D,\mathrm{\neg }D$$\top,\neg\top,D,\neg D$。

它可以衍生出

定理. (Craig's interpolation)

令 $A\supset B$$A\supset B$ LK 可证。

总存在命题 $C$$C$，称为 $A,B$$A,B$ 的插值，满足

• $A\supset C$$A\supset C$ 和 $C\supset B$$C\supset B$ 都 LK 可证；

• $C$$C$ 中所有自由变元、常变元、常谓词都在 $A\cap B$$A\cap B$（虽然这个记号意义不明但相信你懂我意思）中。

特别地，如果 $A,B$$A,B$ 没有公共的常谓词，那么 $A\to$$A\rightarrow$ 和 $\to B$$\rightarrow B$ 之一必 LK 可证。

证明.

$A\supset B$$A\supset B$ 可证，那么（由推断律）$A\to B$$A\rightarrow B$ 可证。划分为 $[\{A:\},\{:B\}]$$[\{A:\},\{:B\}]$ 应用前述引理，得到一个 $C$$C$ 使得 $A\to C$$A\rightarrow C$ 和 $C\to B$$C\rightarrow B$ 都 $\mathsf{LK}\mathrm{♯}$$\mathsf {LK}\sharp$ 可证。

无公共常谓词的情况已经显然了；现在假设有一个公共常谓词 $R(y_1,\dots ,y_k)$$R(y_1,\ldots,y_k)$。

令 $R^{\prime }=\mathrm{\forall }{y}_1^{\prime }\dots y_k^{\prime }R(y_1^{\prime },\dots ,y_k^{\prime })$$R'=\forall y'_1\ldots y'_k R(y'_1,\ldots,y'_k)$，其中 $y^{\prime }$$y'$ 皆为受限变量。这就构造出了一个无参常谓词。将 $\mathrm{\top }$$\top$ 替换为 $R^{\prime }\supset R^{\prime }$$R'\supset R'$ 即可。

其他衍生物都不知道有啥用啊！！！不写算了。

带等号的谓词推演

我们在 LK 中特别加入一个二元常谓词 $=$$=$ 和以下三条公理（实际上该叫公理模式，毕竟每一条实际上都是一整族命题）：

• $\to s=s$$\rightarrow s=s$​

• $s_1=t_1,\dots ,s_n=t_n\to f(s)=f(t)$$s_1=t_1,\ldots,s_n=t_n\rightarrow f(s)=f(t)$

• $s_1=t_1,\dots ,s_n=t_n,R(s)\to R(t)$$s_1=t_1,\ldots,s_n=t_n,R(s)\rightarrow R(t)$

可以得到一个新系统 ${\mathsf{LK}}_e$$\mathsf{LK}_e$。

易证得，对于任何命题 $A$$A$，

都 ${\mathsf{LK}}_e$$\mathsf{LK}_e$ 可证。

与先前的公理系统类似，我们也可以用以下命题族 ${\mathrm{\Gamma }}_e$$\Gamma_e$ 来用 ${\mathrm{\Gamma }}_e,\mathrm{\Gamma }\to \mathrm{\Delta }$$\Gamma_e,\Gamma\rightarrow\Delta$ 的方式定义 ${\mathsf{LK}}_e$$\mathsf {LK}_e$。

• $\mathrm{\forall }x(x=x)$$\forall x(x=x)$

• $\mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_n\mathrm{\forall }{y}_1\dots \mathrm{\forall }{y}_n[x_1=y_1\wedge \dots \wedge x_n=y_n\supset f(x)=f(y)]$$\forall x_1\ldots\forall x_n\forall y_1\ldots\forall y_n[x_1=y_1\land\ldots\land x_n=y_n\supset f(x)=f(y)]$

• $\mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_n\mathrm{\forall }{y}_1\dots \mathrm{\forall }{y}_n[x_1=y_1\wedge \dots \wedge x_n=y_n\wedge R(x)\supset R(y)]$$\forall x_1\ldots\forall x_n\forall y_1\ldots\forall y_n[x_1=y_1\land\ldots\land x_n=y_n\land R(x)\supset R(y)]$

${\mathsf{LK}}_e$$\mathsf{LK}_e$ 中也有切割消除定理，但有所限制。如果切掉的公式形如 $s=t$$s=t$，那么这个切割被称为非本质的。例如对于两个等号公理的切割

这里切掉了 $R(t)$$R(t)$，因而是本质的，但是我们可以通过第三条公理的一例，即 $R$$R$ 取 $=$$=$ 谓词

和另一例

的切割得到。因此得到归纳。

完备性定理

定理.

定义.

令 $L$$L$ 是一个一阶逻辑语言。$L$$L$ 上的一个结构是一个 $⟨D,\varphi ⟩$$\left<D,\phi\right>$ 的对，其中

• 常量被 $\varphi$$\phi$ 映射到 $D$$D$ 上，

• 常函数被 $\varphi$$\phi$ 映射到 $D^{D^n}$$D^{D^n}$​ 上，

• 常谓词被 $\varphi$$\phi$ 映射到 $2^{D^n}$$2^{D^n}$ 上。

特别地，如果再配上一个映射 ${\varphi }_0$$\phi_0$ 把变量也映射到 $D$$D$ 上，那么 $⟨D,\varphi ,{\varphi }_0⟩$$\left<D,\phi,\phi_0\right>$ 还被称为诠释。${\varphi }_0$$\phi_0$ 被称为一个指派。

• 半项是允许受限变量的项。我们如此定义半项 $t$$t$ 在 $\varphi ,{\varphi }_0$$\phi,\phi_0$ 上的映射 $\varphi (t)$$\phi(t)$：对于常量和变量直接应用 $\varphi ,{\varphi }_0$$\phi,\phi_0$，对于 $\varphi f(t)$$\phi f(t)$ 递归地定义 $(\varphi f)(\varphi t)$$(\phi f)(\phi t)$。

• 如果 $R$$R$ 是一个谓词常量，那么 $R(t)$$R(t)$ 被一个诠释满足当且仅当 $\varphi t\in \varphi R$$\phi t\in\phi R$​。

• $\mathrm{\neg }A$$\neg A$ 被满足当且仅当 $A$$A$ 不被满足；$A\wedge B$$A\land B$ 被满足当且仅当 $A,B$$A,B$ 都被满足；$A\vee B$$A\lor B$ 被满足当且仅当 $A,B$$A,B$ 中至少一个被满足；$A\supset B$$A\supset B$ 被满足当且仅当 $A$$A$ 不被满足或 $B$$B$ 被满足。

• $\mathrm{\forall }xB$$\forall xB$ 被满足，当且仅当，对于任何最多只在 $x$$x$ 处和 ${\varphi }_0$$\phi_0$ 不同（当然，也可以就是 $\varphi$$\phi$）的 ${\varphi }_0$$\phi_0$，$B$$B$ 都被满足。$\mathrm{\exists }xB$$\exists xB$ 被满足，当且仅当，存在一个最多只在 $x$$x$ 处和 ${\varphi }_0$$\phi_0$ 不同（当然，也可以就是 $\varphi$$\phi$）的 ${\varphi }_0$$\phi_0$，$B$$B$ 被满足。

• $A\to B$$A\rightarrow B$ 被满足当且仅当 $A$$A$ 不被满足或 $B$$B$ 被满足。

一个命题/列在结构 $⟨D,\varphi ⟩$$\left<D,\phi\right>$ 中有效，当且仅当它在任何指派下都被满足。

一个命题/列有效，当且仅当它在任何结构下都有效。

（终于，我们现在给出我们定理的陈述：）

一个命题 LK 可证当且仅当它有效。

显然，在推理系统中所有的函数/谓词都是没有"实际含义"的空壳，只服从于推理规则。而如果指定了某个结构，函数/谓词就可能有"实际含义"，从而 $R(t)$$R(t)$ 可以"随机地"被指派为真。

仅仅是顺带一提（毕竟我们不打算在此书中研究模型论），一个结构称为某公理系统 $\mathrm{\Gamma }$$\Gamma$ 的模型当且仅当 $\mathrm{\Gamma }$$\Gamma$ 中的所有公理都在该结构中有效。

"可证 $\to$$\rightarrow$ 有效"被称为可靠性。可靠性（显然）蕴含一致性（注意 $A$$A$ 和 $\mathrm{\neg }A$$\lnot A$ 不可能都被满足）。这一部分可以简单地通过在（无切割）推理上归纳得到。

"有效 $\to$$\rightarrow$ 可证"被称为完备性。这将是我们证明的重点。具体来说我们将要证明一个更一般化的命题

引理.

令 $S$$S$ 是一个列。要么它有一个无切割证明，要么存在一个不满足 $S$$S$ 的诠释。

证明. (Schütte)

下面我们将介绍一种机械化地对列进行简化的方法。

我们从列 $S$$S$ 出发，以如下方式展开它的推理树。循环以下 13 步：

• $\mathrm{\neg }$$\lnot$ 左简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Pi }$$\Pi$ 中形如 $\mathrm{\neg }{A}_i$$\lnot A_i$ 的命题去掉 $\mathrm{\neg }$$\lnot$ 移到右边，得到新的叶子列。

• $\mathrm{\neg }$$\lnot$ 右简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Lambda }$$\Lambda$ 中形如 $\mathrm{\neg }{A}_i$$\lnot A_i$ 的命题去掉 $\mathrm{\neg }$$\lnot$ 移到左边，得到新的叶子列。

• $\wedge$$\land$ 左简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Pi }$$\Pi$ 中形如 $A\wedge B$$A\land B$ 的命题直接写成 $A,B$$A,B$，得到新的叶子列。

• $\wedge$$\land$ 右简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Lambda }$$\Lambda$ 中形如 $A\wedge B$$A\land B$ 的命题任意替换为 $A,B$$A,B$ 之一，从而得到 $2^n$$2^n$ 个命题，这 $2^n$$2^n$​ 个命题全是该列的儿子。

• $\vee$$\lor$ 左简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Pi }$$\Pi$ 中形如 $A\vee B$$A\lor B$ 的命题任意替换为 $A,B$$A,B$ 之一，从而得到 $2^n$$2^n$ 个命题，这 $2^n$$2^n$​ 个命题全是该列的儿子。

• $\vee$$\lor$ 右简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Lambda }$$\Lambda$ 中形如 $A\vee B$$A\lor B$ 的命题直接写成 $A,B$$A,B$，得到新的叶子列。

• $\supset$$\supset$ 左简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，考虑所有 $\mathrm{\Pi }$$\Pi$ 中形如 $A\supset B$$A\supset B$ 的命题。新的叶子列为 $B_1,\dots ,B_n,{\mathrm{\Pi }}^{\ast }\to {\mathrm{\Lambda }}^{\ast }$$B_1,\ldots,B_n,\Pi^*\rightarrow\Lambda^*$ 和 ${\mathrm{\Pi }}^{\ast }\to {\mathrm{\Lambda }}^{\ast },A_i$$\Pi^*\rightarrow\Lambda^*,A_i$（共 $n+1$$n+1$ 个）。

• $\supset$$\supset$ 右简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，考虑所有 $\mathrm{\Lambda }$$\Lambda$ 中形如 $A\supset B$$A\supset B$ 的命题。新的叶子列为 $B_1\dots ,B_n,{\mathrm{\Pi }}^{\ast }\to {\mathrm{\Lambda }}^{\ast },A_1,\dots ,A_n$$B_1\ldots,B_n,\Pi^*\rightarrow\Lambda^*,A_1,\ldots,A_n$。

• $\mathrm{\forall }$$\forall$ 左简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Pi }$$\Pi$ 中形如 $\mathrm{\forall }xA(x)$$\forall xA(x)$ 的命题直接写成 $A(a)$$A(a)$（其中 $a$$a$​ 是一个此前没有被用于化简的自由变元）。

• $\mathrm{\forall }$$\forall$ 右简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Lambda }$$\Lambda$ 中形如 $\mathrm{\forall }xA(x)$$\forall xA(x)$ 的命题直接写成 $A(a)$$A(a)$（其中 $a$$a$​​ 是一个在之前的展开没有出现且此前没有被用于化简的自由变元）。

• $\mathrm{\exists }$$\exists$ 左简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Pi }$$\Pi$ 中形如 $\mathrm{\exists }xA(x)$$\exists xA(x)$ 的命题直接写成 $A(a)$$A(a)$（其中 $a$$a$ 是一个在之前的展开没有出现且此前没有被用于化简的自由变元）。

• $\mathrm{\exists }$$\exists$ 右简化。对于所有叶子列 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$，把所有 $\mathrm{\Lambda }$$\Lambda$ 中形如 $\mathrm{\forall }xA(x)$$\forall xA(x)$ 的命题直接写成 $A(a)$$A(a)$（其中 $a$$a$​ 是一个此前没有被用于化简的自由变元）。

• 如果 $\mathrm{\Pi }$$\Pi$ 和 $\mathrm{\Lambda }$$\Lambda$ 有公共命题，不展开它；否则仍把 $\mathrm{\Pi }\to \mathrm{\Gamma }$$\Pi\rightarrow\Gamma$ 展开为自己。

显然这 13 种展开都是有效的推理；而且上面的列如果不被满足，立刻就可以推出下面的列亦为假。

考虑得到的 $T(S)$$T(S)$ 中一条从 $S$$S$ 开始的链。前 12 种展开都会减少逻辑连接词和量词的数量；所以这条链要么终结于有公共命题、没有逻辑连接词和量词的 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$ 要么最终是一条无穷无尽不断重复的没有公共命题的 $\mathrm{\Pi }\to \mathrm{\Lambda }$$\Pi\rightarrow\Lambda$。

前者可以对公理使用弱化律立即推出。因此如果所有"叶子"都是前者，我们已经得到了一个 $S$$S$ 的证明。

如果存在一个后者情况的链，我们可以构造一个结构使得在足够远处， $\cup \mathrm{\Pi }$$\cup\Pi$ 全被满足而 $\cup \mathrm{\Lambda }$$\cup\Lambda$ 全不被满足。显然，$\cup \mathrm{\Pi }$$\cup\Pi$ 和 $\cup \mathrm{\Lambda }$$\cup\Lambda$ 一定没有公共的原子命题 $R(a)$$R(a)$，否则（由于没有切割律）我们一定展开不出无公共命题的列。剩下的工作就显然了。