2.2. 一阶逻辑的语法

我们先来考虑一类最简单的逻辑系统, 它容许有穷长的公式.

语言对象的定义

定义 2.2.0.1. 一个一阶语言要求提供以下资料:

1.	一个固定的可列集 $X=\{x_n|n\in \omega \}$, 这里面的元素称为变元符号.
2.	一个固定的集合 $\mathrm{LSym}=\{\forall ,\neg ,\to ,\approx ,(,),,\}$, 最后的逗号是这个集合中的元素.
3.	一个集合 $\mathcal{F}=\{f_i|i\in I_F\}$ 和一个 $a_F:\mathcal{F}\to \omega$, $\mathcal{F}$ 中的元素称为函数符号, $a_F$ 给它的值称为这个函数的元数.
4.	一个集合 $\mathcal{P}=\{P_i|i\in I_P\}$ 和一个 $a_P:\mathcal{P}\to \omega$, $\mathcal{P}$ 中的元素称为谓词符号, $a_P$ 给它的值称为这个谓词的元数.

不妨要求它们两两不交. 我们将它们合计为 $\mathcal{L}=\{a_F,a_P\}$, 但很多时候我们会根据上下文来确定元数, 所以也会写 $\mathcal{L}=\{\mathcal{F},\mathcal{P}\}$.

我们将记它的字符表为 $\mathrm{Char}=X\cup \mathrm{LSym}\cup \mathcal{F}\cup \mathcal{P}$, 因为我们已经默认了这些集合两两不交因此我们也默认可以从一个字符 $c\in \mathrm{Char}$ 直接看出它是以上四个集合中哪一个集合中的元素.

我们将记 ${\mathrm{Char}}^{<\omega }=\{f:n\to \mathrm{Char}|n\in \omega \}$ 中的元素 $f:n\to \mathrm{Char}$ 为 $⟨f(0),...,f(n-1)⟩$, 称为一个字符串. 字符串的串接操作我们记为 $\square$, 即 $⟨f_0,...,f_{n-1}⟩\square ⟨g_0,...,g_{m-1}⟩=⟨f_0,...,f_{n-1},g_0,...,g_{m-1}⟩$.

我们称 $|\mathcal{L}|=|{\mathrm{Char}}^{<\omega }|=\max \{{\aleph }_0,|\mathrm{Char}|\}$ 为这个语言的基数.

评注. 如果没有选择公理, $\mathcal{F}$ 与 $\mathcal{P}$ 上面是否有良序就可能造成阻碍, 我们会默认它们是良序化了的. 我们会用 $\mathcal{L}::I_F$ 来指代这个语言中的刚才的定义中提到的指标集 $I_F$, 同样的记法可以在符号使用过多的时候避免一定的困惑, 就好像是在访问一个结构体的内部对象一样.

定义 2.2.0.2. 给定一个 $\mathcal{L}$, 我们要指定其中一些具有特殊意义的字符串.

我们如下递归地定义项:

1.	$⟨x_n⟩$ 是项.
2.	如果 $t_0,...,t_{n-1}$ 是项, $f$ 是 $n$ 元函数符号, 则 $$\begin{gathered} ⟨f,(⟩\square t_0\square ⟨,⟩\square t_1\square ...\square \\ {t}_{n-1}\square ⟨)⟩ \end{gathered}$$ 是项.

所有项构成的集合不妨记为 $\mathrm{Term}\subseteq {\mathrm{Char}}^{<\omega }$.

我们如下递归地定义公式:

1.	如果 $t_0,t_1$ 是项, 则 $t_0\square ⟨\approx ⟩\square t_1$ 是公式.
2.	如果 $t_0,...,t_{n-1}$ 是项, $P$ 是 $n$ 元谓词符号, 则 $$\begin{gathered} ⟨P,(⟩\square t_0\square ⟨,⟩\square t_1\square ...\square \\ {t}_{n-1}\square ⟨)⟩ \end{gathered}$$ 是公式.
3.	如果 $\phi$ 是公式, 则 $⟨\neg ⟩\square \phi$ 是公式.
4.	如果 $\phi$ 和 $\psi$ 是公式, 则 $⟨(⟩\square \phi \square ⟨\to ⟩\square \psi \square ⟨)⟩$ 是公式.
5.	如果 $\phi$ 是公式, $x$ 是变元符号, 则 $⟨\forall ,x,(⟩\square \phi \square ⟨)⟩$ 是公式.

所有公式构成的集合不妨记为 $\mathrm{Formula}\subseteq {\mathrm{Char}}^{<\omega }$. 全体形如 $t_0\approx t_1$ 或 $P(t_0,...,t_{n-1})$ 的公式均称为原子公式, 构成的集合记为 $\mathrm{AFormula}$. 不含量词 $\forall$ 的公式称作无量词公式, 全体无量词公式构成的集记为 $\mathrm{qfFormula}$.

由于显而易见的原因, 今后我们会在元语言里面直接操作字符串, 例如 $⟨\neg ⟩\square \phi$ 就会直接写成 $\neg \phi$.

评注. 这里的递归定义基于以下事实: $\mathrm{Char}$ 有一个天然的良序, 进而 ${\mathrm{Char}}^{<\omega }$ 上也有一个天然的良序. 我们所做的事就是在这个良序上给出一个判断, 指出每个字符串是项或者不是项, 是公式或者不是公式. 如果你不会构造 ${\mathrm{Char}}^{<\omega }$ 上的这个良序, 可以看定理 5.7.13.

证明

接下来是证明的概念, 我们目前还是先用 Hilbert 式的推演系统. 首先我们复刻之前定义过的对公式的操作.

定义 2.2.0.3 (自由出现). 我们称变元 $x$ 在公式 $\phi$ 中出现, 若 $x\in \mathrm{dom}\phi$. 由于 $\phi$ 有穷, 我们得到一个函数 $\mathrm{Var}:\mathrm{Formula}\to [X{]}^{<\omega }$, 这里 $[X{]}^{<\omega }={\{}_{fin}X\subseteq X|{|}_{fin}X|<{\aleph }_0\}$, 它指出出现在这个公式中的全体变元.

对每个变元 $x$, 我们对公式 $\phi$ 递归地定义 $x\in \mathrm{fVar}(\phi )$, 称作 $x$ 在 $\phi$ 中自由出现, 如下:

1.	$x$ 在 $t_0\approx t_1$ 中自由出现当且仅当它出现.
2.	$x$ 在 $P(t_0,...,t_{n-1})$ 中自由出现当且仅当它出现.
3.	$x$ 在 $\neg \phi$ 中自由出现当且仅当它在 $\phi$ 中自由出现.
4.	$x$ 在 $(\phi \to \psi )$ 中自由出现当且仅当它在 $\phi$ 或 $\psi$ 中自由出现.
5.	$x$ 在 $\forall x_n(\phi )$ 中自由出现当且仅当它在 $\phi$ 中自由出现且 $x_n$ 不是 $x$.

自然地, 我们定义的这个性质给出一个函数 $\mathrm{fVar}:\mathrm{Formula}\to [X{]}^{<\omega }$, 它指出自由出现在这个公式中的全体变元. 我们有时也会写 $\phi (x_0,...,x_n)$ 以指出 $\mathrm{fVar}(\phi )=\{x_0,...,x_n\}$.

如果 $\mathrm{fVar}(\phi )=\varnothing$, 则称 $\phi$ 是一个闭公式, 或者称之为一个语句. 通常我们用 $\sigma ,\tau$ 等符号表示语句, 全体语句构成 $\mathrm{Formula}$ 的子集 $\mathrm{Sentence}$.

定义 2.2.0.4 (无冲突替换). 给定 $x\in X$ 与 $t\in \mathrm{Term}$, 我们定义一个操作 ${\mathrm{sub}}_t^x:\mathrm{Formula}\to \mathrm{Formula}$, 它递归地将公式变为另一个公式:

1.	${\mathrm{sub}}_t^x(t_0\approx t_1)$ 是 $\phi =t_0\approx t_1$ 这一字符串中所有 $x$ 出现的地方都将 $x$ 替换为 $t$ 得到的新公式. 具体而言, 我们将 $\phi$ 分解为 $$\begin{gathered} {\phi }_0\square ⟨x⟩\square {\phi }_1\square ...\square \\ ⟨x⟩\square {\phi }_n \end{gathered}$$, 使得 ${\phi }_i$ 中 $x$ 均不出现, 然后令 ${\mathrm{sub}}_t^x(\phi )={\phi }_0\square t\square {\phi }_1\square ...\square t\square {\phi }_n$
2.	${\mathrm{sub}}_t^x(P(t_0,...,t_{n-1}))$ 是 $\phi =P(t_0,...,t_{n-1})$ 这一字符串中所有 $x$ 出现的地方都将 $x$ 替换为 $t$ 得到的新公式, 具体操作同上.
3.	${\mathrm{sub}}_t^x(\neg \phi )$ 是 $\neg {\mathrm{sub}}_t^x(\phi )$.
4.	${\mathrm{sub}}_t^x((\phi \to \psi ))$ 是 $({\mathrm{sub}}_t^x(\phi )\to {\mathrm{sub}}_t^x(\psi ))$.
5.	若 $y=x$ 则 ${\mathrm{sub}}_t^x(\forall y(\phi ))$ 仍然是是 $\forall y(\phi )$, 若 $y\ne x$ 则 ${\mathrm{sub}}_t^x(\forall y(\phi ))$ 是 $\forall y({\mathrm{sub}}_t^x(\phi ))$.

我们继续递归地对每个公式 $\varphi$ 定义 ${\mathrm{sub}}_t^x$ 对 $\varphi$ 是否是无冲突替换.

1.	形如 $t_0\approx t_1$ 的公式 $\varphi$, ${\mathrm{sub}}_t^x$ 对 $\varphi$ 总是无冲突替换.
2.	形如 $P(t_1,...,t_n)$ 的公式 $\varphi$, ${\mathrm{sub}}_t^x$ 对 $\varphi$ 总是无冲突替换.
3.	形如 $\neg \phi$ 的公式 $\varphi$, ${\mathrm{sub}}_t^x$ 对 $\varphi$ 是无冲突替换当且仅当 ${\mathrm{sub}}_t^x$ 对 $\phi$ 是无冲突替换.
4.	形如 $(\phi \to \psi )$ 的公式 $\varphi$, ${\mathrm{sub}}_t^x$ 对 $\varphi$ 是无冲突替换当且仅当 ${\mathrm{sub}}_t^x$ 对 $\phi$ 和 $\varphi$ 都是无冲突替换.
5.	形如 $\forall y(\phi )$ 的公式 $\varphi$, ${\mathrm{sub}}_t^x$ 对 $\varphi$ 是无冲突替换当且仅当 $x$ 不在 $\varphi$ 中自由出现, 或 ${\mathrm{sub}}_t^x$ 对 $\phi$ 是无冲突替换且 $y$ 不在 $t$ 中出现.

我们将在无冲突替换时将 $\mathrm{sub}$ 写成 $\mathrm{Sub}$ 以示区别.

评注. 我们写 $x=y$ 指的是这两个字符是同一个字符, 这与公式 $x\approx y$ 不一样.

接下来, 我们定义逻辑公理.

定义 2.2.0.5 (逻辑公理). 对任何公式 $\phi$, 每个形如 $\forall x_{n_0}(\forall x_{n_1}(...\forall x_{n_{m-1}}(\phi )))$ 的公式都称为 $\phi$ 的全称概括, 这里 $n_0,...,n_{m-1}$ 是任意 $m$ 个自然数, $m$ 也是自然数. $\phi$ 的全体全称概括构成的集合记为 $\bar{\forall }\phi$, 称为 $\phi$ 的全称闭包.

我们称以下六类公式的全称概括为逻辑公理.

1.	$\phi \to (\psi \to \phi )$, 这里 $\phi$ 和 $\psi$ 是任意两个公式.
2.	$(\phi \to (\psi \to \varphi ))\to ((\phi \to \psi )\to (\phi \to \varphi ))$, 这里 $\phi$, $\psi$ 和 $\varphi$ 是任意三个公式.
3.	$(\neg \psi \to \neg \phi )\to ((\neg \psi \to \phi )\to \psi )$, 这里 $\phi$ 和 $\psi$ 是任意两个公式.
4.	$\forall x(\phi )\to {\mathrm{Sub}}_t^x(\phi )$, 这里 ${\mathrm{Sub}}_t^x$ 对 $\phi$ 是无冲突替换.
5.	$\forall x(\phi \to \psi )\to (\forall x(\phi )\to \forall x(\psi ))$
6.	$\phi \to \forall x(\phi )$, 这里 $x$ 不在 $\phi$ 中自由出现.
7.	$x\approx x$.
8.	$x\approx y\to (\phi \to {\phi }^{\prime })$, 这里 $\phi$ 是一个原子公式, ${\phi }^{\prime }$ 是把 $\phi$ 中的一部分 $x$ 替换为 $y$ 得到的新的原子公式. 这个部分替换的具体细节可以参考之前我们定义替换时所做的操作.

我们记所有逻辑公理构成的集合为 $\mathrm{Fol}\subseteq \mathrm{Formula}$. Fol 是 first order logic 的首字母缩写.

最后, 我们定义证明这一概念.

定义 2.2.0.6. 满足以下条件的 ${\mathrm{Formula}}^{<\omega }$ 中的元素 $⟨{\phi }_0,...,{\phi }_n⟩$ 将被称作从公式集 $\Gamma \subseteq \mathrm{Formula}$ 到公式 ${\phi }_n$ 的证明序列: 对于任意的 $i\in n+1$, ${\phi }_i$ 满足

1.	${\phi }_i\in \mathrm{Fol}$, 或
2.	${\phi }_i\in \Gamma$, 或
3.	$\exists j,k\in i({\phi }_j=({\phi }_k\to {\phi }_i))$, 这个等号是指作为字符串相等. 这个行为又称作应用分离规则 (MP,Modus Ponens) 从 ${\phi }_j$ 和 ${\phi }_k$ 中得到 ${\phi }_i$, 或者说是用 ${\phi }_k$ 从 ${\phi }_j$ 中分离出 ${\phi }_i$.

如果存在 $\Gamma$ 到 $\phi$ 的证明序列, 则称 $\Gamma$ 证明 $\phi$, 记为 $\Gamma ⊢\phi$. 我们将 $\{\psi \}⊢\phi$ 简记为 $\psi ⊢\phi$.

我们顺带定义理论的概念.

定义 2.2.0.7. $\mathrm{Sentence}$ 的子集称作理论. 我们通常用 $T$ 代表一个理论.

最后, 我们指出一致与完全的概念.

定义 2.2.0.8. 我们会把一个第七条逻辑公理的一个全称概括 $\forall x_0(x_0\approx x_0)$ 记为 $\top$, 将 $\neg \top$ 记为 $\perp$.

对句子集 $\Gamma$, 如果 $\Gamma /⊢\perp$, 则称 $\Gamma$ 是一致的. 如果任给语句 $\sigma$ 都有 $\Gamma ⊢\sigma$ 或 $\Gamma ⊢\neg \sigma$, 则称 $\Gamma$ 是完全的. 注意, 完全性并不要求证明或证否每个公式.

证明的性质

我们来形式化一系列元定理, 换言之它们都是关于证明的定理. 下面提到的 $\Gamma$ 默认是一个公式集.

定理 2.2.0.9 (证明的紧致性). 如果 $\Gamma ⊢\phi$, 则存在 $\Gamma$ 的有穷子集 ${}_{fin}\Gamma \subseteq \Gamma$ 使得 ${}_{fin}\Gamma ⊢\phi$.

证明. 任取一个证明序列, 将其中出现过的全体 $\Gamma$ 中的公式收集起来. 由于证明序列是有穷长的, 所收集到的公式自然也只有有穷多个, 且显然这些公式足以证明 $\phi$.

$\square$

接下来, 我们先给出两个重要定理.

定理 2.2.0.10 (演绎定理). $\Gamma \cup \{\psi \}⊢\phi$ 当且仅当 $\Gamma ⊢(\psi \to \phi )$.

证明. 当是因为我们可以往证明序列里面加一个 $\psi$, 然后用它从 $\psi \to \phi$ 中分离出 $\phi$.

为了证明仅当, 我们设 $⟨{\phi }_0,...,{\phi }_{n-1},{\phi }_n=\phi ⟩$ 是一个 $\Gamma \cup \{\psi \}$ 到 $\phi$ 的证明, 我们归纳地证明对每个 $i\in n+1$ 都有 $\Gamma ⊢(\psi \to {\phi }_i)$ 即可.

1.	如果 ${\phi }_i\in \mathrm{Fol}\cup \Gamma \cup \{\psi \}$, 用 ${\phi }_i$ 自己就可以直接从第一条逻辑公理中分离出 $\psi \to {\phi }_i$.
2.	如果 ${\phi }_i$ 是由 ${\phi }_k$ 从 ${\phi }_j=({\phi }_k\to {\phi }_i)$ 中分离而来的, 根据归纳假设我们有 $\Gamma ⊢(\psi \to {\phi }_k)$ 和 $\Gamma ⊢(\psi \to ({\phi }_j\to {\phi }_i))$, 将这两个证明序列拼在一起, 然后用 $(\psi \to ({\phi }_k\to {\phi }_i))$ 从第二条逻辑公理中分离出 $((\psi \to {\phi }_k)\to (\psi \to {\phi }_i))$, 再用 $(\psi \to {\phi }_k)$ 从其中分离出 $(\psi \to {\phi }_i)$.

因此归纳完毕, 取 $i=n$ 即得到 $\Gamma ⊢(\psi \to \phi )$.

$\square$

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

证明. 假设 $⟨{\phi }_0,...,{\phi }_n=\phi ⟩$ 是 $\Gamma$ 到 $\phi$ 的证明序列, 我们归纳地证明对每个 $i\in n+1$ 都有 $\Gamma ⊢\forall x({\phi }_i)$.

1.	如果 ${\phi }_i\in \mathrm{Fol}$, 则根据定义有 $\forall x({\phi }_i)\in \mathrm{Fol}$.
2.	如果 ${\phi }_i\in \Gamma$, 则我们可以用 ${\phi }_i$ 从第六条逻辑公理中分离出 $\forall x({\phi }_i)$.
3.	如果 ${\phi }_i$ 是由 ${\phi }_k$ 从 ${\phi }_j=({\phi }_k\to {\phi }_i)$ 中分离而来的, 根据归纳假设我们有 $\Gamma ⊢\forall x({\phi }_k)$ 和 $\Gamma ⊢\forall x({\phi }_j\to {\phi }_i)$, 将这两个证明序列拼在一起, 然后用 $\forall x({\phi }_k\to {\phi }_i)$ 从第五条逻辑公理中分离出 $(\forall x({\phi }_k)\to \forall x({\phi }_i))$, 再用 $\forall x({\phi }_k)$ 从其中分离出 $\forall x({\phi }_i)$.

因此归纳完毕, 取 $i=n$ 即得到 $\Gamma ⊢\forall x(\phi )$.

$\square$

评注. 可以看出, 演绎定理和概括定理的证明方法是完全一样的.

关于交换量词, 我们有以下显然的定理.

定理 2.2.0.12. $\forall x(\forall y(\phi ))⊢\forall y(\forall x(\phi ))$ 对任何公式 $\phi$ 成立.

证明. 用第四条公理得出 $\forall x(\forall y(\phi ))⊢\phi$, 然后再根据 $x,y$ 均不在左侧自由出现用概括定理把量词按照我们需要的顺序装上去即可.

$\square$

因此, 我们做以下方便的约定.

定义 2.2.0.13. $\forall x\forall y(\phi )$ 是 $\forall x(\forall y(\phi ))$ 的简写, $\phi \to \psi \to \varphi$ 是 $(\phi \to (\psi \to \varphi ))$ 的简写.

关于否定和 $\perp$ 的关系, 我们仍然有以下元定理. 它们的证明都只用到前三条逻辑公理, 详细的证明我们留给读者.

定理 2.2.0.14. 任给公式 $\phi$ 和 $\psi$, 我们总有以下定理:

1.	$⊢\neg \neg \phi \to \phi$
2.	$⊢\phi \to \neg \neg \phi$
3.	$⊢((\phi \to \psi )\to ((\phi \to \neg \psi )\to \neg \phi ))$
4.	$⊢(\neg \phi \to (\phi \to \psi ))$
5.	$⊢((\phi \to \psi )\to (\neg \psi \to \neg \phi ))$
6.	$⊢((\phi \to \psi )\to ((\phi \to \neg \psi )\to \neg \phi ))$
7.	$⊢(\phi \to (\neg \psi \to \neg (\phi \to \psi )))$

类似的只用前三条逻辑公理就能证明的事实我们今后不再特别指出.

关于等词公理给出的一些结果, 我们也列举如下, 并不再证明.

定理 2.2.0.15. 除了公理 $\forall x(x\approx x)$ 外, 我们有以下定理:

1.	$⊢\forall x\forall y(x\approx y\to y\approx x)$
2.	$⊢\forall x\forall y\forall z(x\approx y\to y\approx z\to x\approx z)$
3.	$$\begin{gathered} ⊢\forall x_{r_0}...\forall x_{r_{n-1}}\forall x_{s_0}...\forall x_{s_{n-1}}(x_{r_0}\approx x_{s_0}\to ...\to x_{r_{n-1}=x_{s_{n-1}}}\to P(x_{r_0}, \\ ...,x_{r_{n-1}})\to P(x_{s_0},...,x_{s_{n-1}})) \end{gathered}$$, 这里 $P$ 是任意一个 $n$ 元谓词符号.
4.	$$\begin{gathered} ⊢\forall x_{r_0}...\forall x_{r_{n-1}}\forall x_{s_0}...\forall x_{s_{n-1}}(x_{r_0}\approx x_{s_0}\to ...\to x_{r_{n-1}=x_{s_{n-1}}}\to f(x_{r_0}, \\ ...,x_{r_{n-1}})\approx f(x_{s_0},...,x_{s_{n-1}})) \end{gathered}$$, 这里 $f$ 是任意一个 $n$ 元函数符号.

我们最后来证明那些关于替换的元定理.

定理 2.2.0.16 (自由替换). 对任意 $\phi$ 的自由变元 $x$ 和任意项 $t$, 总有 ${\mathrm{sub}}_t^x(\phi )$ 是无冲突替换.

证明. 对 $\phi$ 的结构归纳, 根据无冲突替换的定义进行证明是简单的.

$\square$

定理 2.2.0.17 (循环替换). 如果 $y$ 作为符号不在公式 $\phi$ 中出现, 则对任意变元 $x$ 总有 ${\mathrm{sub}}_x^y$ 对 ${\mathrm{sub}}_y^x(\phi )$ 是无冲突替换, 且进一步有 ${\mathrm{sub}}_x^y({\mathrm{sub}}_y^x(\phi ))$ 就是 $\phi$.

证明. 这是因为 $y$ 在 ${\mathrm{sub}}_y^x(\phi )$ 中一定作为自由变元出现.

$\square$

定理 2.2.0.18 (约束替换). 任给公式 $\phi$, 项 $t$ 与变元 $x$, 我们总能构造一个公式 ${\phi }^{\prime }$, 满足:

1.	$\phi ⊢{\phi }^{\prime }$ 且 ${\phi }^{\prime }⊢\phi$.
2.	${\mathrm{sub}}_t^x$ 对 ${\phi }^{\prime }$ 是无冲突替换.

证明. 固定 $t$ 和 $x$, 我们对 $\phi$ 的结构作归纳.

1.	$\phi$ 形如 $t_0\approx t_1$, 则令 ${\phi }^{\prime }=\phi$.
2.	$\phi$ 形如 $P(t_0,...,t_{n-1})$, 则令 ${\phi }^{\prime }=\phi$.
3.	$\phi$ 形如 $\neg \psi$, 则令 ${\phi }^{\prime }=\neg {\psi }^{\prime }$.
4.	$\phi$ 形如 $(\psi \to \varphi )$, 则令 ${\phi }^{\prime }=({\psi }^{\prime }\to {\varphi }^{\prime })$.
5.	$\phi$ 形如 $\forall y(\psi )$, 则新选一个不在 ${\psi }^{\prime }$ 和 $t$ 中出现且不同于 $x,y$ 的新变元符号 $z$, 令 ${\phi }^{\prime }=\forall z({\mathrm{sub}}_z^y({\psi }^{\prime }))$.

归纳地可见 $\phi$ 与 ${\phi }^{\prime }$ 仅仅是约束变元 (不自由的变元) 不同. 我们归纳地证明这个构造满足题中两个要求, 唯一值得注意的就是第五条归纳满足第一条要求的证明.

对 ${\phi }^{\prime }=\forall z({\mathrm{sub}}_z^y({\psi }^{\prime }))$ 的情况, 一方面: 归纳假设给出 $\psi ⊢{\psi }^{\prime }$, 所以 $\forall y(\psi )⊢\forall y({\psi }^{\prime })$, 由 $z$ 不在 ${\psi }^{\prime }$ 中出现可知 $\forall y({\psi }^{\prime })⊢{\mathrm{sub}}_z^y({\psi }^{\prime })$, 最后由 $z$ 不在 $\forall y({\psi }^{\prime })$ 中出现用概括定理得到 $\forall y({\psi }^{\prime })⊢\forall z({\mathrm{sub}}_z^y({\psi }^{\prime }))$; 另一方面, $\forall z({\mathrm{sub}}_z^y({\psi }^{\prime }))⊢{\mathrm{sub}}_y^z{\mathrm{sub}}_z^y({\psi }^{\prime })$, 根据循环替换右侧就是 ${\psi }^{\prime }$, 然后归纳假设给出 ${\psi }^{\prime }⊢\psi$, 最后 $y$ 不在左侧自由出现和概括定理指出 $\forall z({\mathrm{sub}}_z^y({\psi }^{\prime }))⊢\forall y(\psi )$.

$\square$

语言的扩张

定义 2.2.0.19. 我们称语言 ${\mathcal{L}}^{\prime }$ 是语言 $\mathcal{L}$ 的一个扩张, 或者 $\mathcal{L}$ 是 ${\mathcal{L}}^{\prime }$ 的收缩, 若 $\mathcal{L}::a_F\subseteq {\mathcal{L}}^{\prime }::a_F$, 且 $\mathcal{L}::a_P\subseteq {\mathcal{L}}^{\prime }::a_P$.

我们先指出大部分常用的逻辑连接词的形式化.

定义 2.2.0.20. 我们作以下简写方案.

1.	$\neg \forall x(\neg (\phi ))$ 写为 $\exists x(\phi )$.
2.	$(\neg \phi \to \psi )$ 写为 $(\phi \vee \psi )$.
3.	$\neg (\phi \to \neg \psi )$ 写为 $(\phi \wedge \psi )$.
4.	$((\phi \to \psi )\wedge (\psi \to \phi ))$ 写为 $(\phi \leftrightarrow \psi )$.
5.	$\exists y(\forall z({\mathrm{sub}}_z^y(\phi )\leftrightarrow y\approx z))$ 写为 $\exists !y(\phi )$, 这里 $y$ 在 $\phi$ 中自由出现, $z$ 不在 $\phi$ 中出现.

我们现在来关心一类特别的扩张, 它好像能说的更多, 但其实只是说得更方便.

定义 2.2.0.21. 给定语言 $\mathcal{L}$ 上的理论 $T$, 再给定 ${\mathcal{L}}^{\prime }$ 作为 $\mathcal{L}$ 的扩张. 我们特别命名以下 ${\mathcal{L}}^{\prime }$ 句子:

1.	一个 $n$ 元谓词符号 $P\in {\mathcal{L}}^{\prime }::\mathcal{P}$ 的 $\mathcal{L}$ 定义指的是形如 $$\begin{gathered} \forall x_0...\forall x_{n-1}(P(x_0 \\ ,...,x_{n-1})\leftrightarrow {\phi }_P) \end{gathered}$$ 的句子, 这里 ${\phi }_P$ 是一个自由变元集包含于 $$\begin{gathered} \{x_0,..., \\ {x}_{n-1}\} \end{gathered}$$ 的 $\mathcal{L}$ 公式.
2.	一个 $n$ 元函数符号 $f\in {\mathcal{L}}^{\prime }::\mathcal{F}$ 的 $\mathcal{L}$ 定义指的是形如 $$\begin{gathered} \forall x_0...\forall x_{n-1}\forall x_n( \\ f(x_0,...,x_{n-1})\approx x_n\leftrightarrow {\phi }_f) \end{gathered}$$ 的句子, 这里 ${\phi }_f$ 是一个自由变元集包含于 $\{x_0,...,x_n\}$ 的 $\mathcal{L}$ 公式.

对函数符号 $f$ 的 $\mathcal{L}$ 定义, 如果 $T⊢\forall x_0...\forall x_{n-1}\exists !x_n({\phi }_f)$, 则称 $T$ 确证这个定义, 此时称这个定义是 $T$ 定义. 谓词符号的定义无需确证条件也可直接称为 $T$ 定义.

定义 2.2.0.22. 一个 ${\mathcal{L}}^{\prime }$ 的理论 $T^{\prime }$ 称作 $\mathcal{L}$ 理论 $T$ 的可定义扩张, 若:

1.	${\mathcal{L}}^{\prime }$ 是 $\mathcal{L}$ 的扩张, $T\subseteq T^{\prime }$.
2.	存在一个从 (${\mathcal{L}}^{\prime }$ 中不在 $\mathcal{L}$ 中的全体符号) 到 ($T^{\prime }$ 中不属于 $T^{\prime }$ 的全体句子) 的双射, 它给每个符号配备一个与之唯一对应的 $T$ 定义.

我们此时记 $T{\subseteq }_{\mathrm{def}}{T}^{\prime }$.

可定义扩张最重要的事实是保守. 事实上, 我们可以把可定义扩张的公式翻译成原语言中的公式. 首先, 我们需要一个引理.

定义 2.2.0.23. 如果一个公式中所有的原子公式片段都形如 $x\approx y$ 或 $$\begin{gathered} P(x_{m_0} \\ ,...,x_{m_{n-1}}) \end{gathered}$$ 或 $f(x_{m_0},...,x_{m_{n-1}})\approx y$, 则称这是一个无嵌套公式.

定理 2.2.0.24. 任何公式 $\phi$ 都存在一个典范的无嵌套公式 $\mathrm{unNest}(\phi )$, 满足 $⊢(\phi \leftrightarrow \mathrm{unNest}(\phi ))$.

证明.

$\square$

定义 2.2.0.25. 对可定义扩张 $T{\subseteq }_{\mathrm{def}}{T}^{\prime }$, 我们记 ${\phi }_f$ 为与 $f\in {\mathcal{L}}^{\prime }::\mathcal{F}\backslash \mathcal{L}::\mathcal{F}$ 唯一对应的 $T$ 定义, 同理记 ${\phi }_P$.

我们来定义一个典范的翻译函数 $\mathrm{Trans}:{\mathcal{L}}^{\prime }::\mathrm{Formula}\to \mathcal{L}::\mathrm{Formula}$ 如下:

1.

定理 2.2.0.26 (可定义扩张的翻译). 对可定义扩张 $T{\subseteq }_{\mathrm{def}}{T}^{\prime }$, 总有 $T^{\prime }⊢\phi \leftrightarrow \mathrm{Trans}\phi$.

证明.

$\square$

定理 2.2.0.27 (可定义扩张的保守性). 如果 $T{\subseteq }_{\mathrm{def}}{T}^{\prime }$, 则对任何 $\mathcal{L}$ 公式 $\phi$, 总有 $T⊢\phi$ 当且仅当 $T^{\prime }⊢\phi$.

证明.

$\square$