2. 一阶逻辑

2.1语言
2.2语法
2.3语义
2.4可靠性与完备性

2.1语言

一阶逻辑的语言元素 $L$ 有一个可数集的变元符号 $x_{n}$ , 命题逻辑中的 $\neg$ 、 $\to$ 两个符号, 还有以下这些内容:

1.	全称量词符号 $\forall$
2.	$n_{m}$ 元函数符号 $f_{m}$ , $m$ 和 $n_{m}$ 是两个元自然数, 常元符号看做 $0$ 元函数符号
3.	$n_{m}$ 元谓词符号 $P_{m}$ , $m$ 和 $n_{m}$ 是两个元自然数, $0$ 元谓词符号就是命题逻辑中的 $⊤$ 和 $⊥$
4.	等词符号 $\approx$ , 它是一个特别的 $2$ 元谓词符号.

注意我们可疑地令语言中的等词为 $\approx$ 而非 $=$ , 因为后者我们将用来指称元语言的 (换言之, 作为字符串的) 相等. 另一种考虑是, $=$ 指代模型上作为集合的相等 (完全一样), 而 $\approx$ 在模型上不过是一个等价关系.

今后小写字母 $u, v, w, x, y, z$ 默认是变元符号, 小写字母 $f, g, h$ 默认是函数符号, 大写字母 $P$ 默认是谓词符号.

定义 2.1.1 (项). 我们定义一阶逻辑中的项指的是按照以下操作规则得到的只有有限长度的字符串:

1.	常数符号 $c$ 是项.
2.	若 $x$ 是变量符号, 则 $x$ 是项.
3.	若 $t_{1}, t_{2}, ..., t_{n}$ 是项, $f$ 是 $n$ 元函数符号, 则 $f (t_{1}, t_{2}, ..., t_{n})$ 是项.

且若一个有限长度的字符串不能经由此过程生成, 则不称其为项.

今后小写字母

s, t

默认为项.

定义 2.1.2 (公式). 我们定义一阶逻辑中的公式是按照以下操作规则得到的只有有限长度的字符串:

1.	若 $t_{1}, t_{2}, ..., t_{n}$ 是项, $P$ 是 $n$ 元谓词符号, 则 $P (t_{1}, t_{2}, ..., t_{n})$ 是公式.
2.	若 $p$ 和 $q$ 是公式, 则 $\neg p$ 和 $(p \to q)$ 也是公式.
3.	若 $p$ 是公式, $v$ 是变元, 则 $\forall v (p)$ 也是公式.

且若一个有限长度的字符串不能经由此过程生成, 则不称其为公式.

今后小写字母

p, q, r

默认是公式.

变元与公式之间有一个重要的关系.

定义 2.1.3 (自由出现). 我们定义某个变元 $x$ 在公式 $p$ 中的自由出现, 这是一个判断, 将每个公式给到一个真或假:

1.	若 $p$ 形如 $P (t_{1}, t_{2}, ..., t_{n})$ , 则 $x$ 在 $p$ 中自由出现当且仅当 $x$ 作为字符在某个 $t_{i}$ 中出现.
2.	若 $p$ 形如 $\neg q$ , 则 $x$ 在 $p$ 中自由出现当且仅当它在 $q$ 中自由出现.
3.	若 $p$ 形如 $(q \to r)$ , 则 $x$ 在 $p$ 中自由出现当且仅当它在 $q$ 中自由出现或它在 $r$ 中自由出现.
4.	若 $p$ 形如 $\forall v (q)$ , 则 $x$ 在 $p$ 中自由出现当且仅当它在 $q$ 中自由出现且 $p$ 中那个被量化的字符 $v$ 不是 $x$ .

若 $x$ 不在 $p$ 中自由出现, 但作为字符在里面出现, 则称 $x$ 受限出现或约束出现.

若公式 $σ$ 中没有自由出现的元素, 则称它是一个语句.

注 2.1.4. 我们可以引入 $p \lor q$ 作为 $(\neg p \to q)$ 的缩写, $p \land q$ 作为 $\neg (p \to \neg q)$ 的缩写, $p \leftrightarrow q$ 作为 $(p \to q) \land (q \to p)$ 的缩写, $\exists v (p)$ 作为 $\neg\forall v (\neg p)$ 的缩写. $\exists$ 也称作存在量词.

因为有等词的语言更复杂, 我们今后默认语言里有等词; 没有等词的语言只要忽略所有等词相关的内容, 或者加入一个最简单的等词

\approx==

就可以了.

很显然, 现在项就是个无辜的, 在地位上和变元相去不远的字符串, 而推理、判断这些高级活动则交由公式来承担.

2.2语法

我们现在陈述一阶逻辑的一般形式推理系统. 首先来定义一些必要的操作.

定义 2.2.1 (全称概括). 称公式 $p$ 是公式 $q$ 的一个全称概括, 若有有限个变元 $x_{1}, x_{2}, ..., x_{n}$ 使得 $p = \forall x_{1} \forall x_{2} ...\forall x_{n} q$ .

定义 2.2.2 (替换). 若有变元 $x$ 和项 $t$ , 我们对公式 $p$ 定义替换 $p_{t}^{x}$ , 它就是按字符串操作, 在 $p$ 中每一个自由出现 $x$ 的地方都把 $x$ 改写成 $t$ .

然而, 很多时候随意的替换会改变命题的真假. 我们需要以下关系.

定义 2.2.3 (无冲突替换). 对变元 $x$ 和项 $t$ , $t$ 可无冲突替换 $x$ 是一个给所有公式的判断, 每个公式判断一个真或假, 递归定义如下:

1.	若 $p$ 形如 $P (t_{1}, t_{2}, ..., t_{n})$ , 则可以无冲突替换.
2.	若 $p$ 形如 $\neg q$ , 则 $x$ 在 $p$ 中可无冲突替换当且仅当它在 $q$ 中可无冲突替换.
3.	若 $p$ 形如 $(q \to r)$ , 则 $x$ 在 $p$ 中可无冲突替换当且仅当它在 $q$ 中可无冲突替换且它在 $r$ 中可无冲突替换.
4.	若 $p$ 形如 $\forall v (q)$ , 则 $x$ 在 $p$ 中可无冲突替换当且仅当 $x$ 不在 $p$ 中自由出现, 或 ( $v$ 不在 $t$ 中自由出现且 $q$ 可无冲突替换).

现在, 我们的公理是以下这些形式的每条公式的所有全称概括:

1.	形如命题逻辑公理的公式, 其中原来需要命题逻辑公式的地方现在以一阶逻辑公式代替之.
2.	$\forall x (p) \to p_{t}^{x}$ , 其中在 $p$ 中 $t$ 可无冲突替换 $x$ .
3.	$(\forall x (p \to q) \to (\forall x (p) \to \forall x (q)))$
4.	$(p \to \forall x (p))$ , 其中 $x$ 不在 $p$ 中自由出现.
5.	$x \approx x$
6.	$x \approx y \to (p \to p^{'})$ , 其中 $p^{'}$ 是把 $p$ 里面某些 (不一定是全部, $p_{y}^{x}$ 才是全部) $x$ 出现的地方改成 $y$ 得到的新的公式 (字符串操作).

最后, 我们仍然定义证明. $Σ ⊢ p$ 是存在一列满足以下要求的公式串 $p_{0}, ..., p_{n}$ 的缩写:

1.	$p_{i}$ 是公理, 或
2.	$p_{i}$ 在 $Σ$ 中, 或
3.	$p_{j} = p + k \to p_{i}$ , 这里 $0 \leq j, k < i$ .

我们同样略去许多元定理 (例如反证法, 逆否证法, 概括定理, 演绎定理等等) 的证明, 而默认读者有能力 (或者充分相信其他人有能力) 将这些我们直观把握的证明方法形式化为这个对象语言里面的一个推理序列的生成模式.

有一些有特殊地位的元定理, 我们将在后面证明完备性定理的时候予以特别的注意, 并加以简略的证明.

2.3语义

现在我们要考察真. 注意这里我们并不能简单的要求公式们谁真谁假, 因为有自由出现的变元们, 如果反复要求怎样怎样必须一样怎样怎样必须相反, 我们要做的事就太复杂了, 而且从这样的操作中也很难看出这个东西凭什么就是真或者假的. 因此, 我们要先考虑真假的证据, 也就是这个语言的结构. 这里我们不得不借助元语言中的朴素集合论的帮助.

定义 2.3.1 (语言的结构). 一个语言 $L$ 的结构是有限个集族构成的集族的集合 $M = {M, P, F, C}$ , 满足

1.	$M$ 是一个集合, 我们称之为论域, 又称为宇宙.
2.	$P$ 里面, 对应于语言里每个 $n$ 元谓词 $P$ 都有指定唯一的一个集合 $P^{M} \subseteq M^{n}$ , 且这就是它的全部.
3.	$F$ 里面, 对应于语言里每个 $n$ 元函数 $f$ 都有指定唯一的一个函数 $f^{M} : M^{n} \to M$ , 且这就是它的全部.
4.	$C \subseteq M$ 里面, 对应于语言里每个常元 $c$ 都有指定唯一的一个 $c^{M} \in M$ , 且这就是它的全部.

不难看出, 这其实就是给语言配上了一个集合论意义下的实例, 每个语言里的东西都可以经过这个实例翻译成集合论里的东西. 注意, 结构是元的对象. 我们的对象语言

L

只有在我们元语言人的帮助下才能提升到它身上.

现在我们来定义赋值的概念, 并依此得出语义蕴含的概念. 我们给出的这个定义方式的核心是由 Tarski 在 1933 年给出的.

定义 2.3.2 (语义蕴含). 我们先来定义赋值. 结构 $M$ 上的一个初始赋值 $s$ 是一个从全体变元的集合映到这结构的论域 $M$ 的一个映射. 现在我们来定义这个初始赋值对应的赋值 $\overset{s}{ˉ}$ , 它把对象语言能构造的对象按以下方式提升到某些元语言对象中:

首先, 每个项都将变成一个 $M$ 中的元素, 按以下方式递归定义:

1.	对每个变元符号 $x$ , 定义 $\overset{s}{ˉ} (x) = s (x)$
2.	对每个常数符号 $c$ , 定义 $\overset{s}{ˉ} (c) = c^{M}$
3.	如果 $t_{1}, t_{2}, ..., t_{n}$ 是项, $n$ 元函数符号 $f$ 将给出项 $t = f (t_{1}, t_{2}, ..., t_{n})$ , 定义 $\overset{s}{ˉ} (t) = f^{M} (\overset{s}{ˉ} (t_{1}), \overset{s}{ˉ} (t_{2}), ..., \overset{s}{ˉ} (t_{n}))$

然后, 每个原子公式 (没有量词和逻辑连接词的公式) 都会被判断:

1.	$(M, \overset{s}{ˉ})$ 判断 $t_{1} \approx t_{2}$ 为真, 记为 $(M, \overset{s}{ˉ}) ⊨ t_{1} \approx t_{2}$ , 当且仅当 $\overset{s}{ˉ} (t_{1}) = \overset{s}{ˉ} (t_{2})$
2.	$(M, \overset{s}{ˉ}) ⊨ P (t_{1}, t_{2}, ..., t_{n})$ 当且仅当 $(\overset{s}{ˉ} (t_{1}), \overset{s}{ˉ} (t_{2}), ..., \overset{s}{ˉ} (t_{n})) \in P^{M}$

可以看出, 我们就是用元语言重新解释了对象语言里的公式, 从而在元语言里面进行了判断.

最后, 每个公式都会被判断:

1.	$(M, \overset{s}{ˉ}) ⊨ \neg p$ 当且仅当 $(M, \overset{s}{ˉ})$ 不判断 $p$ 为真, 也就是判断为假, 后者又记为 $(M, \overset{s}{ˉ}) \neq ⊨ p$
2.	$(M, \overset{s}{ˉ}) ⊨ (p \to q)$ 当且仅当 $(M, \overset{s}{ˉ}) \neq ⊨ p$ 或者 $(M, \overset{s}{ˉ}) ⊨ q$
3.	$(M, \overset{s}{ˉ}) ⊨ \forall x (p)$ 当且仅当对任何 $d \in M$ , 有 $(M, \overset{s}{ˉ}_{d}^{x}) ⊨ p$ , 其中 $\overset{s}{ˉ}_{d}^{x}$ 是一个新增的从初始赋值函数 $s_{d}^{x}$ 延拓到的对所有句子长度小于 $\forall x (p)$ 的句子有定义的赋值函数, 而 $s_{d}^{x}$ 把除了 $x$ 之外的变元都按 $s$ 的方式一样的映入 $M$ , 只是把 $x$ 改成了映射到 $d$ .

这样, 判断的定义的合理性还需要对句子长度归纳一番, 这工作交由读者自己进行. 不难发现我们的定义还是仅仅是把对象语言的判断提升为元语言的判断, 但是元语言里的判断是我们先验直观而有所把握的.

我们今后不区分初始赋值 $s$ 与它对应的赋值 $\overset{s}{ˉ}$ .

这里的 $⊨$ 还不能按习惯称之为语义蕴含, 因为左边输进来的东西不对. 我们还要进一步定义.

我们称公式集 $Γ$ 语义蕴含公式 $p$ , 记作 $Γ ⊨ p$ , 如果对任何结构 $M$ 和任何赋值 $s$ , 如果有 $(M, s) ⊨ Γ$ , 换言之判断 $Γ$ 中每个公式为真, 则它一定还判断 $p$ 为真.

语义蕴含最神奇的地方在于以下定理及其推论.

定理 2.3.3 (自由出现的决定性). 固定结构 $M$ , 如果如果两个赋值在一个公式的所有自由出现变元上取相同的值, 则 $(M, s_{1}) ⊨ p$ 当且仅当 $(M, s_{2}) ⊨ p$

证明. 对公式的结构和长度进行归纳证明, 细节交予读者自证.

$□$

推论 2.3.4. 固定结构 $M$ , 对任何语句 $σ$ , 注意到它没有自由变元, 故要不然它对任何赋值都真, 要不然对任何赋值都假. 我们将这两种情况简记为 $M ⊨ σ$ 和 $M \neq ⊨ σ$ .

2.4可靠性与完备性

很显然, 这一节的主要目的是像证明零阶语言即命题逻辑的可靠性和完备性一样, 试着证明一阶逻辑的可靠性与完备性. Gödel 于 1929 年首次得到了完备性的证明, 并在 1930 年公之于世. 我们将要给出的证明方法则是 Henkin 在 1949 年提出的. 看到这些人物的名字, 读者大约能猜到这个定理并不好证.

首先, 我们还是证一下可靠性. 由于语言更复杂了, 公理的数目大大增多, 可靠性也没有之前那么显然. 先来看一个引理.

引理 2.4.1 (替换引理). 如果项 $t$ 可以在公式 $φ$ 中无冲突地替换变元 $x$ , 则 $(M, s) ⊨ φ_{t}^{x}$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ φ$ .

证明. 还是对公式 $φ$ 实行归纳.

1.	$φ$ 形如 $P (t_{1}, t_{2}, ..., t_{n})$ . 此时 $(M, s) ⊨ P (t_{1}, t_{2}, ..., t_{n})_{t}^{x}$ 当且仅当 $(s ((t_{1})_{t}^{x}), s ((t_{2})_{t}^{x}), ..., s (t_{n})_{t}^{x}) \in P^{M}$ 当且仅当 $(s_{s (t)}^{x} (t_{1}), s_{s (t)}^{x} (t_{2}), ..., s_{s (t)}^{x} (t_{n})) \in P^{M}$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ P (t_{1}, t_{2}, ..., t_{n})$ .
2.	$φ$ 形如 $t_{1} \approx t_{2}$ . 与上类似.
3.	$φ$ 形如 $\forall y (ϕ)$ . 此时若 $x$ 不在 $φ$ 中自由出现, 则由自由变元决定性显然. 下讨论自由出现的情形: 注意到无冲突替换要求 $y$ 不在 $t$ 出现且 $t$ 在 $ϕ$ 中也可以无冲突替换, 这说明对任何 $d$ 都有 $s (t) = s_{d}^{y} (t)$ . 又注意到 $φ_{t}^{x} = \forall y (ϕ_{t}^{x})$ , 可如下做连续等价推导: $(M, s) ⊨ φ_{t}^{x}$ 当且仅当对所有的 $d$ , $(M, s_{d}^{y}) ⊨ ϕ_{t}^{x}$ 当且仅当 (归纳假设) 对所有的 $d$ , $(M, (s_{d}^{y})_{s_{d}^{y} (t)}^{x}) ⊨ ϕ$ 当且仅当对所有的 $d$ , $(M, (s_{d}^{y})_{s (t)}^{x}) ⊨ ϕ$ 当且仅当对所有的 $d$ , $(M, (s_{s (t)}^{x})_{d}^{y}) ⊨ ϕ$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ ϕ$ .
4.	$φ$ 形如 $\neg ϕ$ . 此时 $(M, s) ⊨ φ_{t}^{x}$ 当且仅当 $(M, s) \neq ⊨ ϕ_{t}^{x}$ 当且仅当 $(M, s_{s (t)}^{x}) \neq ⊨ ϕ$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ φ$ .
5.	$φ$ 形如 $ϕ \to ψ$ . 类上.

$□$

下面来证明可靠性.

定理 2.4.2 (可靠性定理). 一阶逻辑是可靠的. 换言之, $Σ ⊢ φ$ 蕴含 $Σ ⊨ φ$ .

证明. 首先, 分离规则保持有效性是显然的, 因此只需要证明每条公理都普遍有效 (valid). 换言之, $\emptyset ⊨ φ$ .

由于公理有好几种, 而且还允许任意全称概括, 我们需要把这个定理归纳地拆成几个部分来证明.

(1) 第一组公理, 即从命题逻辑中继承的公理的有效性: 只需注意到赋值在所有素公式 (没有逻辑连接词的公式) 上的取值可以决定它在所有公式上的取值.

(2) 第二组公理: 我们已知的是 $(M, s) ⊨ \forall x (φ)$ , 欲证的则是 $(M, s) ⊨ φ_{t}^{x}$ , 而根据替换引理只要证 $(M, s_{s (t)}^{x}) ⊨ φ$ , 而这只要按定义展开条件中的全称量词, 然后选取 $d = s (t)$ 即可.

(3) 第三组公理: 拆开 $\forall$ 的定义, 在每个 $d$ 上面分离, 显然.

(4) 第四组公理: 拆开 $\forall$ 的定义, 由自由出现变元的决定性显然.

(5) 第五组公理: 显然.

(6) 第六组公理: 考察所有满足 $x \approx y$ 的模型与赋值, 不难归纳得出它在每个项上都可以将任意个 $x$ 替换为 $y$ 而不改变真假, 进而原子公式, 进而素公式, 进而全体公式.

最后还要证明,

φ

普遍有效当且仅当它的某个全称概括

\forall x (φ)

普遍有效, 而这由普遍有效的定义不难证明.

$□$

接下来证明完备性定理. 我们当然还是模仿在命题逻辑中使用的方法, 先使用以下引理.

引理 2.4.3. 一阶逻辑完备当且仅当任意一个一致的公式集都是可满足的.

其证明与命题逻辑中的证明也类似, 这里略去. 下面再证明三个可能用到的元定理.

引理 2.4.4 (常数概括引理). 若 $Γ ⊢ φ$ , 而常元符号 $c$ 不在 $Γ$ 中出现, 则存在同样不在 $Γ$ 中出现的变元符号 $y$ , 使得 $Γ ⊢ φ_{y}^{c}$ . 更进一步, 还存在一个 $Γ ⊢ \forall y φ_{y}^{c}$ 的不包含 $c$ 的推演序列.

证明. 我们先证明前面. 考虑 $Γ ⊢ φ$ 的推演序列 $(φ_{0}, φ_{1}, ..., φ_{n} = φ)$ . 有限个公式只出现有限个变元, 所以我们随便拿一个没出现在这些公式中的变元 $y$ , 不难发现 $((φ_{0})_{y}^{c}, (φ_{1})_{y}^{c}, ..., (φ_{n})_{y}^{c} = φ_{y}^{c})$ 是 $Γ$ 到 $φ_{y}^{c}$ 的一个推演序列.

下面验证更进一步的部分. 由于推演序列是有限长度的, 我们一定有一个

Γ_{0} \subseteq Γ

为有限集,

Γ_{0} ⊢ φ

, 进而

Γ_{0} ⊢ φ_{y}^{c}

, 进而直接从这里就能由概括公理得出

Γ_{0} ⊢ \forall y (φ_{y}^{c})

, 而这一步也没有加入新的常数符号, 所以

Γ ⊢ \forall y φ_{y}^{c}

的这个推演序列没用到

c

.

$□$

引理 2.4.5 (循环替换引理). 如果变元 $y$ 不在公式 $φ$ 中出现, 则变元 $x$ 可以在公式 $φ_{y}^{x}$ 中无冲突地替换 $y$ , 且 $(φ_{y}^{x})_{x}^{y} = φ$ .

证明. 只要无冲突替换成立, 由简单的字符串操作就不难证明最后的式子. 而由于

φ_{y}^{x}

里根本不出现

x

, 无冲突替换性由简单的归纳就能证出来.

$□$

引理 2.4.6 (约束变元替换引理). 如果有公式 $φ$ , 变元 $x$ 和项 $t$ , 则存在公式 $φ^{'}$ , 它和 $φ$ 只有某些约束变元不一样, 而且满足

(1) $φ ⊢ φ^{'}$ , $φ^{'} ⊢ φ$ ;

(2) $t$ 可以在 $φ^{'}$ 中无冲突地替换 $x$ .

证明. 固定 $t$ 和 $x$ , 我们递归地构造 $φ^{'}$ . 对未提到的情况, 我们构造的 $φ^{'}$ 都是完全不改变句子结构的, 原子公式甚至不改变句子.

对于 $φ$ 形如 $\forall y ϕ$ 的情况, 我们由归纳假设选一个 $ϕ^{'}$ 然后再选一个 $t$ 和 $x$ 和 $φ$ 和 $ϕ^{'}$ 中都没出现过的变元 $z$ , 定义 $φ^{'} = \forall z (ϕ^{'})_{z}^{y}$ .

现在只需要递归证明这个构造确实合理. 这里只录入最重要的量词情况的 (1) 的证明, 别的都很简单留给读者自己证明.

首先根据归纳假设, $ϕ ⊢ ϕ^{'}$ , 于是 $\forall y ϕ ⊢ \forall y ϕ^{'}$ , 又因为 $z$ 不出现, 而 $\forall y ϕ^{'} ⊢ (ϕ^{'})_{z}^{y}$ , 概括得到 $\forall y ϕ^{'} ⊢ \forall z (ϕ^{'})_{z}^{y}$ , 于是 $\forall y ϕ ⊢ \forall z (ϕ^{'})_{z}^{y}$ .

另一方面, 有归纳假设

ϕ^{'} ⊢ ϕ

. 显然有

\forall z (ϕ^{'})_{z}^{y} ⊢ ((ϕ^{'})_{z}^{y})_{y}^{z}

, 由

z

不出现可用循环替换得到

\forall z (ϕ^{'})_{z}^{y} ⊢ ϕ^{'}

, 进而

\forall z (ϕ^{'})_{z}^{y} ⊢ ϕ

, 最后由

y

不在左边自由出现可以概括为

\forall z (ϕ^{'})_{z}^{y} ⊢ \forall y ϕ

.

$□$

现在我们准备充分, 向完备性定理发起挑战.

定理 2.4.7 (Gödel 完备性定理). 一阶逻辑是完备的.

证明. 只要证明一致则可满足. 假定有一个一致的公式集 $Γ$ , 我们自然的想像命题逻辑一样得到极大一致集, 然后构造一个结构, 最后得到一个赋值, 来满足这个公式集. 以下默认理论有等词, 因为没有等词的理论显然更简单.

Step1. 扩充得到极大一致集

为了能最后能得到结构, 我们必须给这个极大一致集附带一些额外的东西. 具体而言, 我们向原来的语言 $L$ 中加入可数多个新的常元符号 $c_{1}, c_{2}, ...$ , 从而它们不在 $L$ 的任何公式中出现. 我们记 $L_{C}$ 为扩充后的语言.

首先, $Γ$ 在 $L_{C}$ 中一致. 证明是用反证法, 若它变得不一致了, 那把推演序列里的新常元用常数概括引理改成变元, 就会得到 $Γ$ 在 $L$ 中不一致的证据, 矛盾.

接下来添加 Henkin 公理. 我们 (由可数性) 列举 $L_{C}$ 中全体 (公式, 变元) 的有序对为 $(ϕ_{1}, x_{1}), (ϕ_{2}, x_{2}), ...$ . 我们递归地令

1.	$θ_{1}$ 为 $\neg\forall x_{1} ϕ_{1} \to \neg (ϕ_{1})_{c_{i_{1}}}^{x_{1}}$ , 其中 $c_{i_{1}}$ 是第一个不在 $ϕ_{1}$ 中出现的新常元.
2.	$θ_{k + 1}$ 为 $\neg\forall x_{k + 1} ϕ_{k + 1} \to \neg (ϕ_{k + 1})_{c_{i_{k + 1}}}^{x_{k + 1}}$ , 其中 $c_{i_{k + 1}}$ 是第一个在 $ϕ_{1}, ..., ϕ_{k}, ϕ_{k + 1}, θ_{1}, ..., θ_{k}$ 中都没出现过的新常元符号.

我们记 $Θ = {θ_{1}, θ_{2}, ...}$ , 然后来验证 $Γ \cup Θ$ 一致.

反证. 如果不一致, 由证明序列的有限性一定可以找到一个最小的 $n$ 使得 $Γ \cup {θ_{1}, ..., θ_{n + 1}}$ 不一致. 由反证法元定理, 这指出 $Γ \cup {θ_{1}, ..., θ_{n}} ⊢ \neg θ_{n + 1}$ . 假定 $θ_{n + 1} = \neg\forall x ϕ \to \neg ϕ_{c}^{x}$ , 则 $Γ \cup {θ_{1}, ..., θ_{n}} ⊢ {\neg\forall x ϕ, ϕ_{c}^{x}}$ , 由定义 $c$ 不在左边出现, 于是常数概括得到 $Γ \cup {θ_{1}, ..., θ_{n}} ⊢ \forall x ϕ$ , 这与 $n$ 极小是矛盾的.

类似 Lindenbaum 定理, 我们通过枚举句子做 $L_{C}$ 中 $Γ \cup Θ$ 的极大一致扩张 $Δ$ , 并且从过程中得到它对语法蕴含封闭 (即 $Δ ⊢ ϕ$ 指出 $ϕ \in Δ$ ).

Step2. 构造无等词公式的解释

这个结构非常有趣, 因为这个结构就是我们语言里面的东西.

记 $L_{C}$ 上所有项的集合为 $M$ , 定义二元关系 $E^{M}$ 为 $(t_{1}, t_{2}) \in E^{M} \leftrightarrow (t_{1} \approx t_{2}) \in Δ$ , 对谓词 $P$ 定义 $(t_{1}, t_{2}, ..., t_{n}) \in P^{M} \leftrightarrow (P (t_{1}, t_{2}, ..., t_{n})) \in Δ$ , 对函数 $f$ 定义 $f^{M} (t_{1}, t_{2}, ..., t_{n}) = (f (t_{1}, t_{2}, ..., t_{n}))$ , 对常数 $c$ 定义 $c^{M} = c$ , 得到结构 $M$ . 最后定义初始赋值 $s$ 把变元 $x$ 变到它自己这个项 $x$ 上面, 并令其扩展, 得到结构 $M$ 上的赋值 $s$ .

注意, 这个 $E$ 也可以当成是我们给 $L_{C}$ 添加的一个新的二元谓词.

我们证明: 对任意公式 $φ$ , $(M, s) ⊨ φ^{'}$ 当且仅当 $φ \in Δ$ , 其中 $φ^{'}$ 是在 $φ$ 中把等词 $\approx$ 换成 $E$ 得到的公式.

(1) 通过对项归纳不难得知 $s (t) = t$ .

接下来对公式 $φ$ 实行归纳, 证明 $(M, s) ⊨ φ^{'}$ 当且仅当 $φ \in Δ$ . 我们还是只证明最复杂的量词情形, 把其他简单情形交由读者自行完成. 假设 $φ = \forall x ϕ$ .

(2) 从左向右; 由定义 $(ϕ, x)$ 有一条对应的 Henkin 公理 $θ = \neg\forall x ϕ \to \neg ϕ_{c}^{x}$ . 注意 $(\forall x ϕ)^{'} = \forall x ϕ^{'}$ , 我们有 $(M, s) ⊨ \forall x ϕ^{'}$ 蕴含 $(M, s_{c}^{x}) ⊨ ϕ^{'}$ 由替换引理蕴含 $(M, s) ⊨ ϕ_{c}^{' x}$ 蕴含 $(M, s) ⊨ (ϕ_{c}^{x})^{'}$ 由假设蕴含 $ϕ_{c}^{x} \in Δ$ 蕴含 $\neg ϕ_{c}^{x} \neq \in Δ$ 由封闭性和 Henkin 公理蕴含 $(\neg\forall x ϕ) \in Δ$ 蕴含 $\forall x ϕ \in Δ$ .

(3) 从右向左: 我们来证明逆否. 若 $(M, s) \neq ⊨ \forall x ϕ^{'}$ , 我们想证明 $\forall x ϕ^{'} \neq \in Δ$ . 条件中拆掉 $\forall$ 的定义已经给我们了一个反例项 $t$ , 满足 $(M, s_{t}^{x}) \neq ⊨ ϕ^{'}$ . 运用约束变元替代引理, 选择一个 $ψ$ , 它与 $ϕ$ 的差别只有约束变元, 而且 $t$ 在 $ψ$ 中可以无冲突地替代 $x$ . 做连续推导: $(M, s_{t}^{x}) \neq ⊨ ϕ^{'}$ 由语义等价推出 $(M, s_{t}^{x}) \neq ⊨ ψ^{'}$ 由替换引理推出 $(M, s) \neq ⊨ ψ_{t}^{x}^{'}$ 由归纳假设就得到 $ψ_{t}^{x}^{'} \neq \in Δ$ 推出 $\forall x ψ \neq \in Δ$ 推出 $\forall x ϕ \neq \in Δ$ .

Step3. 构造一般公式的解释

注意上面已经证明了无等词公式的完备性. 由于等词和元语言的等于不一样, 直接做会出事, 我们要考虑一个商结构. 首先, 读者不难验证, $E$ 是 $M$ 上的一个等价关系, 且和每个谓词和函数都是相容的 (即相等的东西判断/映射到同一个东西).

我们重新定义结构 $U$ 的论域为 $M / E$ , 谓词 $P$ 对应 $([t_{1}], [t_{2}], ..., [t_{n}]) \in P^{U} \leftrightarrow P (t_{1}, t_{2}, ..., t_{n}) \in Δ$ , 函数 $f$ 对应 $f^{U} ([t_{1}], [t_{2}], ..., [t_{n}]) = [f (t_{1}, t_{2}, ..., t_{n})]$ , 常元 $c$ 对应 $c^{U} = [c]$ . 定义初始赋值 $S (x) = [x]$ , 然后令其自然地延拓为赋值. 我们只要证明:

对任意公式 $φ$ , $(U, S) ⊨ φ$ 当且仅当 $φ \in Δ$ .

归纳验证是惯常的归纳, 注意我们可以引用

M

中已经证明的结论来简化过程.

$□$

名字空间

视图

2. 一阶逻辑

2.1语言

2.2语法

2.3语义

2.4可靠性与完备性