1.2. 一阶语言中的证明

Hilbert 式推演系统一例

接下来, 我们在最少的语境下定义证明这个概念. 我们用到的定义方法并不是最简单的, 但它是最经典的.

定义 1.2.0.1 (全称概括). 对公式 $φ$ , 我们称形如 $\forall x_{m_{1}} (\forall x_{m_{2}} (... (\forall x_{m_{n}} (φ))))$ 的公式为它的全称概括, 这里 $n$ 和 $m_{1}, ..., m_{n}$ 都是自然数.

定义 1.2.0.2 (逻辑公理). 我们称以下六类公式的全称概括为逻辑公理.

1.	$φ \to (ψ \to φ)$ , 这里 $φ$ 和 $ψ$ 是任意两个公式.
2.	$(φ \to (ψ \to ϕ)) \to ((φ \to ψ) \to (φ \to ϕ))$ , 这里 $φ$ , $ψ$ 和 $ϕ$ 是任意三个公式.
3.	$(\neg ψ \to \neg φ) \to ((\neg ψ \to φ) \to ψ)$ , 这里 $φ$ 和 $ψ$ 是任意两个公式.
4.	$\forall x (φ) \to sub_{t}^{x} (φ)$ , 这里 $sub_{t}^{x}$ 对 $φ$ 是无冲突替换.
5.	$\forall x (φ \to ψ) \to (\forall x (φ) \to \forall x (ψ))$
6.	$φ \to \forall x (φ)$ , 这里 $x$ 不在 $φ$ 中自由出现.
7.	$x \approx x$ .
8.	$x \approx y \to (φ \to φ^{'})$ , 这里 $φ$ 是一个原子公式, $φ^{'}$ 是把 $φ$ 中的一部分 $x$ 替换为 $y$ 得到的新的原子公式.

所有的逻辑公理可以列举出来, 我们记这个列举为 $Λ_{f o l}$ . fol 是 first order logic 的简写.

评注. 所有的公理可以被列举出来并不是一件平凡的事实.

定义 1.2.0.3 (证明). 列举有穷或无穷个公式 ${φ_{0}, φ_{1}, ...}$ , 我们记这个列举为 $Γ$ . 我们称有序的有穷公式序列 ${ϕ_{0}, ϕ_{1}, ..., ϕ_{n}}$ 是从 $Γ$ 到公式 $ϕ_{n}$ 的证明, 若对每个下标 $i \leq n$ :

1.	$ϕ_{i}$ 是公理, 或
2.	$ϕ_{i}$ 是某个 $φ_{k}$ , 或
3.	存在两个小于 $i$ 的下标 $j, k$ , 使得 $ϕ_{j}$ 形如 $(ϕ_{k} \to ϕ_{i})$ .

如果存在 $Γ$ 到 $φ$ 的证明, 则称 $Γ$ 证明 $φ$ , 记为 $Γ ⊢_{Λ} φ$ , 通常简记为 $Γ ⊢ φ$ .

如果我们的 $Γ$ 没有列举任何公式, 则特别地记之为 $\emptyset$ . $\emptyset ⊢ φ$ 通常简记为 $⊢ φ$ . 我们将在 $⊢ φ$ 时称 $φ$ 为一个定理.

接下来, 我们摆出一些关于证明的元定理, 读者可以自行尝试证明它们. 它们都是常见的证明手段, 因此直接承认其正确性也没太大关系.

引理 1.2.0.4 (循环替换). 如果 $y$ 作为符号不在公式 $φ$ 中出现, 则对任意变元 $x$ 总有 $sub_{x}^{y}$ 对 $sub_{y}^{x} (φ)$ 是无冲突替换, 且进一步有 $sub_{x}^{y} (sub_{y}^{x} (φ))$ 就是 $φ$ .

引理 1.2.0.5 (自由替换). 对任意 $φ$ 的自由变元 $x$ 和项 $t$ , 总有 $sub_{t}^{x} (φ)$ 是无冲突替换.

引理 1.2.0.6 (约束替换). 任给公式 $φ$ , 项 $t$ 与变元 $x$ , 我们总能构造一个公式 $ϕ$ , 满足:

1.	$φ ⊢ ϕ$ 且 $ϕ ⊢ φ$ .
2.	$sub_{t}^{x}$ 对 $ϕ$ 是无冲突替换.

定理 1.2.0.7 (概括定理). 如果 $x$ 不在 $Γ$ 的任何公式中自由出现, 且 $Γ ⊢ φ$ , 则 $Γ ⊢ \forall x (φ)$ .

定理 1.2.0.8 (紧致定理). 如果 $Γ ⊢ φ$ , 则可以列举出 $Γ$ 中的有限个公式 $_{f in} Γ = {φ_{0}, ..., φ_{n}}$ 使得 $_{f in} Γ ⊢ φ$ . fin 是 finite 的简写.

定理 1.2.0.9 (演绎定理). ${φ_{0}, ..., φ_{n}} ⊢ φ$ 当且仅当 ${φ_{0}, ..., φ_{n - 1}} ⊢ (φ_{n} \to φ)$ .

定理 1.2.0.10 (逆否定理). ${φ_{0}, ..., φ_{n}} ⊢ \neg φ$ 当且仅当 ${φ_{0}, ..., φ_{n - 1}, φ} ⊢ \neg φ_{n}$ .

定理 1.2.0.11 (反证法). 如果有公式 $ψ$ 使得 ${φ_{0}, ..., φ_{n}, φ} ⊢ ψ$ 且 ${φ_{0}, ..., φ_{n}, φ} ⊢ \neg ψ$ , 则 ${φ_{0}, ..., φ_{n}} ⊢ φ$ .

公理化理论

接下来, 我们讨论给定了一些非逻辑公理后能证明的全体公式.

定义 1.2.0.12 (公理). 任意一次对有穷或无穷个公式 ${φ_{0}, ...}$ 的列举 $Λ$ 都可以称作公理组, 其中的公式称作公理.

定义 1.2.0.13 (公理组中的证明与定理). 类比 $Λ = Λ_{f o l}$ 的情况, 我们可以定义 $Γ ⊢_{Λ} φ$ . 这称作公理组中的证明.

我们将在 $⊢_{Λ} φ$ 即 $Λ ⊢ φ$ 时称 $φ$ 是公理组 $Λ$ 下的定理.

定义 1.2.0.14 (一致与完全). 如果存在公式 $φ$ 使得 $⊢_{Λ} φ$ 且 $⊢_{Λ} \neg φ$ , 则称公理组 $Λ$ 不一致. 如果 $Λ$ 不是不一致的, 则称 $Λ$ 是一致的.

如果对任何公式 $φ$ , 总有 $⊢_{Λ} φ$ 或 $⊢_{Λ} \neg φ$ 之一, 则称公理组 $Λ$ 完全. 如果 $Λ$ 不是完全的, 则称 $Λ$ 是不完全的.

评注. 显然按照这个定义不一致的公理组一定是完全的, 但我们很少考虑这种堪称恶堕的情况.

我们的数学总是在某个公理系统下进行推理, 并证明各种各样的定理. 然而, 我们还常常进行定义, 以简化定理的表述, 在此我们有必要对这一行动做一形式化的解释. 我们显然只能定义两种对象: 一种是谓词, 一种是函数. 我们将在下面处理它们.

定义 1.2.0.15 (定义谓词). 在语言 $L = (n_{f}, n_{P}, a_{f}, a_{P})$ 的公理组 $Λ$ 下, 含有 $n$ 个自由变元 $x_{m_{1}}, ..., x_{m_{n}}$ 的公式 $φ$ 定义了一个 $n$ 元谓词 $P_{φ}$ 指的是以下行为:

考虑新的语言 $L^{'} = (n_{f}, n_{P} + 1, a_{f}, a_{P}^{'})$ , $a_{P}^{'}$ 与 $a_{P}$ 对 $m < n_{P}$ 的取值相同, 且 $a_{P}^{'} (n_{P})$ 等于上面指定的 $n$ . 我们记这一新语言中的 $P_{n_{P}}$ 为 $P_{φ}$ , 并考虑以下的翻译操作 $T$ , 它将 $L^{'}$ 下的公式 $ϕ^{'}$ 翻译为 $L$ 中的公式 $T (ϕ^{'})$ :

1.	对形如 $P_{m} (t_{1}, ..., t_{k})$ 的 $ϕ^{'}$ , 若 $m < n_{P}$ 则 $T (ϕ^{'})$ 就是 $ϕ^{'}$ , 若 $m = n_{P}$ 则 $T (ϕ^{'})$ 是 $sub_{t_{1}}^{x_{m_{1}}} (... (sub_{t_{n}}^{x_{m_{n}}} (φ^{'})))$ , 显然这 $n$ 次替换对 $φ^{'}$ 都是无冲突的.
2.	别的情况归纳新增的部分没有变化.

显然 $L$ 中的公式与项都可以自然地视为 $L^{'}$ 中的公式与项, 因此 $Λ$ 也可以视为 $L^{'}$ 的公理组. 我们向其中再引入全体以下两条公理, 形成一个 $L^{'}$ 中的公理组 $Λ^{'}$ :

1.	$φ (x_{m_{1}}, ..., x_{m_{n}}) \to P_{φ} (x_{m_{1}}, ..., x_{m_{n}})$
2.	$P_{φ} (x_{m_{1}}, ..., x_{m_{n}}) \to φ (x_{m_{1}}, ..., x_{m_{n}})$

另一个显然的观察是对 $L$ 中的公式 $ϕ$ 总有 $T (ϕ) = ϕ$ .

定理 1.2.0.16. 在 $L^{'}$ 中总有 $T (ϕ^{'}) ⊢_{Λ^{'}} ϕ^{'}$ 且 $ϕ^{'} ⊢_{Λ^{'}} T (ϕ^{'})$ .

证明. 归纳, 细节是简单的.

$□$

推论 1.2.0.17. 特别的, 在 $L^{'}$ 中 $⊢_{Λ^{'}} ϕ^{'}$ 当且仅当在 $L$ 中 $⊢_{Λ} T (ϕ^{'})$ . 因此, $Λ^{'}$ 与 $Λ$ 具有相同的一致性和完全性.

定义 1.2.0.18 (定义函数). 在语言 $L = (n_{f}, n_{P}, a_{f}, a_{P})$ 的公理组 $Λ$ 下, 一个含有 $n + 1$ 个自由变元 $x_{m_{0}}, x_{m_{1}}, ..., x_{m_{n}}$ 的公式 $φ$ 若还满足 $⊢_{Λ} \forall x_{m_{1}} (... (\forall x_{m_{n}} (\neg\forall y (sub_{y}^{x_{m_{0}}} (φ) \to \neg\forall x_{m_{0}} (φ \to y \approx x_{m_{0}})))))$ 则我们说 $φ$ 定义了一个 $n$ 元函数 $f_{φ}$ 的时候指的是以下行为:

考虑新的语言 $L^{'} = (n_{f} + 1, n_{P}, a_{f}^{'}, a_{P})$ , $a_{f}^{'}$ 与 $a_{f}$ 对 $m < n_{f}$ 取值相同, 且 $a_{f}^{'} (n_{d})$ 等于上面指定的 $n$ . 我们记这一新语言中的 $f_{n_{f}}$ 为 $f_{φ}$ , 并考虑以下的翻译操作 $T$ , 它将 $L^{'}$ 下的项 $t^{'}$ 和公式 $ϕ^{'}$ 都翻译为 $L$ 中的公式:

1.	对于形如 $x_{m}$ 的项 $t^{'}$ , $T (t^{'})$ 就是 $y \approx x_{m}$ , 这里 $y$ 是一个新引入的不同于 $x_{m}$ 的变元符号.
2.	对于形如 $f_{m} (t_{1}, ..., t_{a_{f}^{'} (m)})$ 且 $m < n_{f}$ 的项 $t^{'}$ , 列举每个项 $t_{i}$ 的自由变元记为 $t_{i} (x_{i, 1}, ..., x_{i, k_{i}})$ , 假定 $T (t_{i})$ 新引入的变元符号是 $y_{i}$ , 由自由替换引理不妨设以上所有变元符号皆两两不同, 这个 $T (t^{'})$ 是 $\neg\forall y_{1} (... (\forall y_{a_{f}^{'} (m)} (T (t_{1}) \to (... \to (T (t_{a_{f}^{'} (m)}) \to \neg y \approx f_{m} (y_{1}, ..., y_{a_{f}^{'} (m)}))))))$ , 这里 $y$ 是一个新引入的不同于以上所有变元符号的变元符号.
3.	对于形如 $f_{m} (t_{1}, ..., t_{a_{f}^{'} (m)})$ 且 $m = n_{f}$ 的项 $t^{'}$ , 此时 $a_{f}^{'} (m) = n$ , 仍列举每个项 $t_{i}$ 的自由变元记为 $t_{i} (x_{i, 1}, ..., x_{i, k_{i}})$ , 假定 $T (t_{i})$ 新引入的变元符号是 $y_{i}$ , 由自由替换引理不妨设以上所有变元符号皆两两不同, 且均与 $x_{m_{0}}, ..., x_{m_{n}}$ 两两不同, 这个 $T (t^{'})$ 是 $\neg\forall y_{1} (... (\forall y_{n} (T (t_{1}) \to (... \to (T (t_{n}) \to \neg sub_{y}^{x_{m_{0}}} (sub_{y_{1}}^{x_{m_{1}}} (... (sub_{y_{n}}^{x_{m_{n}}} (φ)))))))))$ , 这里 $y$ 是一个新引入的不同于以上所有变元符号的变元符号.
4.	对于形如 $P_{m} (t_{1}, ..., t_{a_{P} (m)})$ 的公式 $ϕ^{'}$ , 仍列举每个项 $t_{i}$ 的自由变元记为 $t_{i} (x_{i, 1}, ..., x_{i, k_{i}})$ , 假定 $T (t_{i})$ 新引入的变元符号是 $y_{i}$ , 不妨设以上所有变元符号皆两两不同, $T (ϕ^{'})$ 是 $\forall y_{1} (... (\forall y_{a_{P} (m)} (\neg (T (t_{1}) \to (... \to (T (t_{a_{P} (m)}) \to \neg P_{m} (y_{1}, ..., y_{a_{P} (m)})))))))$ .
5.	对于别的情况的公式, 归纳新增的部分没有变化.

显然 $L$ 中的公式与项都可以自然地视为 $L^{'}$ 中的公式与项, 因此 $Λ$ 也可以视为 $L^{'}$ 的公理组. 我们向其中再引入全体以下两条公理, 形成一个 $L^{'}$ 中的公理组 $Λ^{'}$ :

1.	$φ (x_{m_{0}}, x_{m_{1}}, ..., x_{m_{n}}) \to x_{m_{0}} \approx f_{φ} (x_{m_{1}}, ..., x_{m_{n}})$
2.	$x_{m_{0}} \approx f_{φ} (x_{m_{1}}, ..., x_{m_{n}}) \to φ (x_{m_{0}}, x_{m_{1}}, ..., x_{m_{n}})$

定理 1.2.0.19. 对 $L$ 中的公式 $ϕ$ , 将之视为 $L^{'}$ 中的公式后得到的 $T (ϕ)$ 仍是 $L$ 中的公式, 且 $ϕ ⊢ T (ϕ)$ 且 $T (ϕ) ⊢ ϕ$ .

证明. 归纳, 细节繁而不难.

$□$

定理 1.2.0.20. 在 $L^{'}$ 中总有 $T (ϕ^{'}) ⊢_{Λ^{'}} ϕ^{'}$ 且 $ϕ^{'} ⊢_{Λ^{'}} T (ϕ^{'})$ .

证明. 归纳, 细节繁而不难.

$□$

推论 1.2.0.21. 特别的, 在 $L^{'}$ 中 $⊢_{Λ^{'}} ϕ^{'}$ 当且仅当在 $L$ 中 $⊢_{Λ} T (ϕ^{'})$ . 因此, $Λ^{'}$ 与 $Λ$ 具有相同的一致性和完全性.

最后, 我们定义一些通用的逻辑符号. 用它们写的句子将被视为对应的句子转写.

定义 1.2.0.22. 我们定义以下符号.

1.	$\exists x (φ)$ 指的是 $\neg\forall x (\neg φ)$ .
2.	$φ \lor ψ$ 指的是 $\neg φ \to ψ$ .
3.	$φ \land ψ$ 指的是 $\neg (\neg φ \lor \neg ψ)$ .
4.	$φ \leftrightarrow ψ$ 指的是 $(φ \to ψ) \land (ψ \to φ)$ .

名字空间

视图

1.2. 一阶语言中的证明

Hilbert 式推演系统一例

公理化理论