这篇文章是相当早之前，为了给数理逻辑更进一步的学习所做的一个总结. 如今当然已经无足轻重，但我仍然将之放在此处作为一个参考. 其原始文本是使用 typst 写成的，用 agent 转换为 markdown 文本，并把公式转换成 katex，我希望不要有什么错误.

本文主要是启发性地介绍，因此在严谨性上可能稍有纰漏，但想必这个世界上并不真的需要更多的文本来提供严谨论述. 在写作计划上，本文还有最后一章，关于一节逻辑的可靠性与完备性的证明. 但由于我过懒所以略去，如果读者有需要，可以参考复旦大学的郝兆宽等所写的《数理逻辑：证明及其限度》作为一个相当容易理解的补充.

一阶逻辑的”隐喻”和”纲要”

让我们回到解代数方程这件事情上.

我们创造了一些符号，用她们组成公式来描述现实世界的对象间的一些关系，也就是数、未知数组成的方程. 在这个基础上，我们形成了一系列推理方法，把一个方程变成另一个. 并且我们认为，这些得到的结果与现实世界是吻合的：也就是说每一个方程都在她的”论域”下描绘了一个现实情况，同时每个现实的情况都能用方程来描述.

这样，我们就得到了一套方法论，用符号和公式间的操作来研究现实中的问题，并且也可以用现实中的问题反过来理解这些符号的公式.

数理逻辑在很大程度上就是这样的思路，我们类比地说：在逻辑学的世界里，我们的现实就是各种各样已经发展出的数学理论，我们用一些标准化的符号构成公式，并用她们来描述理论. 同时，我们可以定义公式上的推理，用她们来研究数学的理论世界中的若干问题——在这里很容易想到理论公理化的出发点——比如有关证明的可能性的问题.

代数方程	数理逻辑
未知数、数字、运算	逻辑符号
方程式	公式、语句
数学运算	推演系统
现实世界	数学理论

而一阶逻辑就是我们核心的工具，作为逻辑世界里的”方程”.

作为疾风怒涛的一阶逻辑恶补，我们会按照上述的思路，快速地构建起整个框架，并给出一些基本的定理和证明——这些，至少到目前为止，主要是为了阅读 Kunen 的《Set Theory》而写作的.

一阶逻辑的”语言”和”公式”

所谓一阶逻辑的语言，简单说就是我们所要用来描述数学理论的符号的总体.

她主要由两部分组成：逻辑符号和非逻辑符号. 其中逻辑符号是在所有的语言中都一致的，用来完成核心的叙述和推理，而非逻辑符号是由不同的情形所决定的，也就是说为了描述不同的理论，我们选取不同的非逻辑符号的系统来数学理论.

具体地说，一个语言 $\mathcal{L}$ 包括：

逻辑符号（必要）：

• 括号：$()$，这是为了避免歧义和易于阅读引入的
• 逻辑连词：$\neg$、$\to$、$\leftrightarrow$、$\land$、$\lor$，她们分别可以被理解为否定（非）、推出、等价、且、或
• 量词符号：$\forall$、$\exists$，分别被理解成任意和存在，又被叫做全称量词和存在量词
• 变元：$v_1, v_2, v_3, \cdots$，她们用来表示数学理论中的”元素”

非逻辑符号（非必要）：

• 若干常数符号 $c$，用来表示数学理论中的必要元素
• 若干 $n$-元函数符号 $f$，一般用来表示数学理论中的运算，比如加减乘除
• 若干 $n$-元关系符号 $P$，一般用来表示数学理论中的关系判断，比如大小（序关系）等
• 等词符号 $\approx$，用来表示逻辑上的相等，也就是两个逻辑对象是一致的

这些内容看起来有些庞杂，难以记忆也不易理解，我们给出一个尚未完整定义的句子，用以提供一个直觉的理解. 在讨论整数的大小的时候，我们可以选取常数符号 $2$（这里事实上仅仅是一个符号）表示数字 $2$，又以 $\times$ 作为一个函数，把两个数字映射到她们的积上，还能定义关系符号 $<$，用来表示小于. 如此，句子”任意整数 $x<y$，都有 $2x < 2y$“就可以写成：

$\forall x \forall y(x<y \to 2 \times x < 2 \times y)$

在这里，$x$、$y$ 就是逻辑符号里的变元，表示我们讨论的问题里可以选取的那些元素.

为了更严格地讨论，我们还要定义项和公式两个概念. 直观的说，项就是上述句子里诸如 $x$、$y$、$2 \times x$、$2 \times y$ 这样的东西，而公式就是带有判断的、由项组成的内容，比如上面的整个句子.

形式上，所有的变元和常数都是项，而由项填入函数得到的还是项. 这里有一个”递归式”的定义，所谓由项得到的项，其实就是说填入函数的未必一定是变元和常数，也可以是”已经填入了变元或常数的函数”.

至于公式，是将项填入关系符号以后，用来表示对项的关系进行判断的语句，就好比是”方程”用来表示数量关系那样，我们把这样的公式成为”原子公式”，意味着她们是最小的公式. 而对于公式，用逻辑连词连接起来的也是公式，表示公式的否定、推出等. 最后，如果 $\phi$ 是一个公式，那么选取一个变元 $v$，$\forall v \phi$ 也是一个公式.

比如上面的那个例子中，$x<y \to 2 \times x < 2 \times y$ 就是一个公式.

现在，我们就得到了一个完整定义的一阶逻辑语言，我们有了”词汇”和”语法”，可以顺利地造出句子来，并能用她标准化的表达一些数学中的判断.

然而，还有一些语法上的问题需要澄清，那就是全称量词的意义. 考察如下两个句子：

$(x < y) \to (x < y)$ $(x < y) \to \forall x \forall y(x < y)$

稍加思考就能知道，前一个公式总是真的，但后一个公式总是假的.

这就告诉我们，全称量词对一个公式的影响是深刻的. 更细致地说，如果有全称量词存在，那么变元就从不固定的变得固定了. 对于上一个公式，要验证她是真的，就代入 $x$ 和 $y$ 即可，很容易发现公式的前半部分和后半部分始终保持相同. 而对于下一个公式，前半部分的 $x$ 和 $y$ 可以任意代值进入，但后半部分却不能代入数值，因为我们不能理解”任意的 $2$“是什么东西.

直观地说：当一个公式有全称量词在前面，那么公式里的变元就被”约束”住了，反之，这个变元是可以”自由”替换的. 我们把前一种变元叫做”约束出现的”，后一种则称为”自由出现的”. 自由出现者称为”自由变元”，而约束出现的则称为”哑元”.

更形式地说：

• 若 $\phi$ 是原子公式，则变元 $x$ 在其中自由出现当且仅当 $x$ 出现在里面
• 若 $\phi$ 是 $\neg \psi$ 的形式，那么变元 $x$ 在其中自由出现当且仅当 $x$ 在 $\psi$ 中自由出现
• 若 $\phi$ 是 $\psi \to \gamma$ 的形式，那么变元 $x$ 在其中自由出现当且仅当 $x$ 在 $\phi$ 或在 $\gamma$ 中自由出现
• 若 $\phi$ 是 $\forall v \psi$ 的形式，那么变元 $x$ 在其中自由出现当且仅当 $x$ 在 $\psi$ 中自由出现且 $x \neq v$

对于一个公式，如果里面出现的所有变元都是哑元，也就是她们都被全称量词在最前端约束了，那么就称她们是”闭公式”. 对于一个公式，如果把它里面的所有变元都用全称量词约束住，得到新的公式，就新的公式称为这个公式的”全称闭包”. 特别的，对于一个闭公式，她的全称闭包就是她自己.

一个闭公式，又被叫做一个”语句”.

细心的读者也许还会发现，有一些其它的逻辑连词没有在上述定义中出现，这是为什么？原因在于其它的逻辑连词都能用 $\neg$ 和 $\to$ 表示. 类似的，存在量词也可以用全称量词表示成 $\exists x \leftrightarrow \neg \forall x \neg$，也就是”存在”等价于”不是所有都不是”. 因此，我们在讨论中略去这些情况. 如果读者希望更多的信息，可以自行学习命题逻辑中”功能完全”这个概念.

一阶逻辑的”解释”和”模型”

现在，我们已经基本上定义好了”方程”，然而上面所说的所有，事实上都应当被看成是纯粹的符号，而对于方程的意义，尚未给一个说法. 我们不应因为我们可以直观地阅读符号来获得意义，就认为它们的意义已经是确定了的.

现在，我们就要来完成这一点. 其实就直观而言，我们要做的事情很好理解，就是给我们定义的语言里的每个符号一个”解释”. 形式地说：

对于一个语言 $\mathcal{L}$，它的结构 $\mathfrak{A}$ 指的是一个二元组 $(A, \cdot^{\mathfrak{A}})$. 其中 $A$ 是一个集合，称为论域，$\cdot^{\mathfrak{A}}$ 是以 $\mathcal{L}$ 为定义域，$A$ 为值域的函数：

$f: \mathcal{L} \to A$ $x \mapsto x^{\mathfrak{A}}$

将常数符号映射为 $A$ 中的元素；将 $n$-元函数 $\mathcal{L}$ 的函数映射为 $A^n$ 到 $A$ 的函数；将 $n$-元关系映射为 $A$ 中 $n$-元组构成的集合，即 $A^n$ 的子集.

然而，给了这些解释还不够，因为它们描述的是数学理论，我们希望有一个方法来说明一个公式是不是”真的”，这就涉及到对变元的处理. 比如以有理数为论域的公式 $x \geq 0$，我们当然知道它描述的是两个数字的大小，然而这个式子是不是对的呢？为了解决这一点，我们就需要给其中的变元赋值.

考虑语言 $\mathcal{L}$ 中所有自由变元的集合 $\mathcal{V}$，一个结构 $\mathfrak{A}$ 上的一个赋值指的是函数 $s: \mathcal{V} \to A$.

当定义了一个赋值后，我们就要考虑项的赋值，而这个可以由赋值自然地扩展出来. 回忆项的构成，是由变元、常数，以及将项填入函数得到新的项形成的. 那么对应的，扩展赋值 $\overline{s}$ 定义为：

• 对变元 $x$，$\overline{s}(x) = s(x)$
• 对常数 $c$，$\overline{s}(c) = c^{\mathfrak{A}}$
• 对项 $t_1, t_2, \cdots, t_n$ 和 $n$-元函数 $f$，

$\overline{s}[f(t_1, t_2, \cdots, t_n)] = f^{\mathfrak{A}}(\overline{s}(t_1), \overline{s}(t_2), \cdots, \overline{s}(t_n))$

最后，我们就可以给公式来定义”满足”的概念.

对于一个结构 $\mathfrak{A}$，公式 $\phi$，和一个赋值 $s$，若有以下情况，就说”$\mathfrak{A}$ 和 $s$ 满足 $\phi$“，记成 $(\mathfrak{A}, s) \vDash \phi$：

• 当 $\phi$ 是 $t_1 \approx t_2$，若 $\overline{s}(t_1) = \overline{s}(t_2)$，则 $(\mathfrak{A}, s) \vDash \phi$
• 当 $\phi$ 是 $P(t_1, \cdots, t_n)$，若 $(\overline{s}(t_1), \cdots, \overline{s}(t_n)) \in P^{\mathfrak{A}}$，则 $(\mathfrak{A}, s) \vDash \phi$
• 当 $\phi$ 是 $\neg \psi$，则 $(\mathfrak{A}, s) \vDash \phi$ 当且仅当 $(\mathfrak{A}, s) \nvDash \psi$，也就是 $(\mathfrak{A}, s)$ 没能满足 $\psi$
• 当 $\phi$ 是 $(\psi \to \gamma)$，那么 $(\mathfrak{A}, s) \vDash \phi$ 当且仅当 $(\mathfrak{A}, s) \nvDash \psi$ 或 $(\mathfrak{A}, s) \vDash \gamma$
• 当 $\phi$ 是 $\forall x \psi$，$(\mathfrak{A}, s) \vDash \phi$ 定义为对任何 $d \in A$，$(\mathfrak{A}, s_d^x) \vDash \phi$，其中

$$s^x_d(y) = \begin{cases} s(y) &\text{, } y \neq x\\ d &\text{, } y = x \end{cases}$$

也就是将 $\phi$ 中的 $x$ 只解释成 $d$.

通过这个定义，我们接下来可以定义公式之间的”语义蕴含”：

对两个公式 $\phi$ 和 $\psi$，如果任意的结构 $\mathfrak{A}$ 和赋值 $s$，当 $(\mathfrak{A}, s) \vDash \phi$ 时，一定有 $(\mathfrak{A}, s) \vDash \psi$，那么就称 $\phi$ 语义蕴含 $\psi$，记成 $\phi \vDash \psi$.

直觉地说，就是 $\phi$ 的正确性从任何意义上都蕴含着 $\psi$ 的正确性.

另外，我们还给出一些叫法上的约定. 当两个公式互相语义蕴含时，说她们是语义等价的. 如果有一个公式集 $\Gamma$，其中的每个公式都语义蕴含公式 $\phi$ 时，就说 $\Gamma$ 语义蕴含 $\phi$，记成 $\Gamma \vDash \phi$. 而当任何结构 $\mathfrak{A}$ 和赋值 $s$ 都满足 $\phi$，时，说 $\phi$ 是普遍有效的，而这等价于空公式集 $\emptyset \vDash \phi$.

我们不难发现，如果两个赋值 $s_1, s_2$ 在公式 $\phi$ 中所有自由变元上都取值相同，那么自然有 $(\mathfrak{A}, s_1) \vDash \phi$ 当且仅当 $(\mathfrak{A}, s_2) \vDash \phi$.

既然如此，对于一个语句 $\phi$，因为其中没有任何自由变元了，所以

• 要么对所有赋值 $s$，$(\mathfrak{A}, s) \vDash \phi$
• 要么对所有赋值 $s$，$(\mathfrak{A}, s) \nvDash \phi$

因此，我们就能定义当情况为前一种时，记成 $\mathfrak{A} \vDash \phi$，反之 $\mathfrak{A} \nvDash \phi$. 此时说 $\phi$ 在 $\mathfrak{A}$ 中成立，也说 $\mathfrak{A}$ 是 $\phi$ 的一个模型.

一阶逻辑的”推演”和”公理”

我们已经发展出了一套符号，并给出了严格的方法来描述符号的意义. 但这仍然是不够的，因为单单是发明一套语言来重述事实，无疑只是一种空洞的转述. 不仅没能带来新的洞见，甚至还阻碍我们理解语句的步伐. 然而，一阶逻辑当然没有在这里停下，正如学会了方程的写法和意义，我们还要学习如何”解方程”. 这就是一阶语言的证明系统.

那么，什么是一个证明？从传统的数学——比如欧氏几何——中，我们可以看到，一个证明就是从一些我们默认的公理出发，经过一系列的步骤，比如写出公理、使用三段论、通过反证法等等，最终得到一个结果.

进一步的，所谓的使用三段论、反证法等，其实是运用了一些逻辑学的知识来构造一个必然正确的命题，再从中拆分出一个结果. 比如这样一个推理：

• 苏格拉底是人
• 人都会死
• 苏格拉底会死

实质上是：

• 苏格拉底是人
• 人都会死
• 如果苏格拉底是人且人都会死，那么苏格拉底会死
• 苏格拉底会死

其中，1 和 2 是我们设定的”公理”，而 3 是一个在逻辑上必然正确的”逻辑公理”，4 是我们从前面”分离”出来的结论.

现在，用数理逻辑的语言来重述，一个从公式集 $\Gamma$（设定的公理）到公式 $\phi$ 的推演就是一个公式序列 $(\phi_0, \phi_1, \phi_2, \cdots, \phi_n)$，

其中 $\phi_n = \phi$，而 $\phi_i (i \in \{0, \cdots, n\})$ 要么是公式集 $\Gamma$ 中的（1、2），要么是逻辑公理（3），或者是从先前的公式中分离出来的公式（4）.

现在剩下的问题就是：逻辑公理究竟有哪些？分离的原则又是什么？

一阶语言的逻辑公理由如下公式的全称闭包组成：

命题逻辑公理：对于任意公式 $\phi, \psi, \gamma$，

• $\phi \to (\psi \to \phi)$
• $(\phi \to (\psi \to \gamma)) \to ((\phi \to \psi) \to (\phi \to \gamma))$
• $(\neg \phi \to \neg \psi) \to ((\neg \phi \to \psi) \to \phi)$

量词公理：

• $\forall x \phi \to \phi^x_t$，其中 $\phi^x_t$ 是把 $\phi$ 中所有的 $x$ 无冲突的替换为 $t$
• $\forall x(\phi \to \psi) \to (\forall x \phi \to \forall x \psi)$
• $\phi \to \forall x \phi$，其中 $x$ 不在 $\phi$ 中自由出现

等词公理（如果该语言中定义了等词）：

• $x \approx x$
• $x \approx y \to (\phi \to \phi')$，其中 $\phi$ 是原子公式，$\phi'$ 是将 $\phi$ 中若干 $x$ 替换成 $y$

而分离的原则是所谓的分离规则，当推演序列中有形如 $\phi$ 和 $\phi \to \psi$ 的公式时，可以分离得到 $\psi$ 这个公式.

一旦存在一个从 $\Gamma$ 到 $\phi$ 的推演，就称 $\phi$ 为 $\Gamma$ 的内定理，记作 $\Gamma \vdash \phi$. 特别的，如果存在一个推演，使其中任何一个公式都不属于 $\Gamma$，那么这个推演的结果 $\phi$ 实际上只依赖于一阶逻辑本身，把它称为一阶逻辑的内定理，记成 $\vdash \phi$.

我们应当注意，这个所谓的推演，其实只是形式性的，并没有告诉我们什么是”真”的. 尽管我们常常可以”读出”这个证明讲了什么，我们也大致可以理解逻辑公理都在表示什么（比如 1.1 是说真的命题可以被推出，1.2 就是三段论的形式化，1.3 就是矛盾律等等），但实际上我们仍然不能保证我们的推理是正确的. 要说她是正确的，就要求我们结合第 3、4 两个章节的内容，去说明 $\Gamma \vdash \phi \Leftrightarrow \Gamma \vDash \phi$，她们分别叫做可靠性定理和完全性定理.

一阶逻辑的”例子”和”演示”

通过上述的内容，我们已经基本展示了一阶逻辑的基本架构. 由于内容纷繁复杂，虽然总体思路是清楚的，但我们仍然可能迷失在细节之中. 尽管细节非常重要，但为了更加整体地把握，并快速获得一个体系的直觉，我们使用一个非常简单的例子来展示一阶逻辑.

虽然一阶逻辑主要是一个数学理论，但一方面，数学的理论往往已经足够抽象，并不利于理解，另一方面分析哲学也常常使用一阶逻辑来进行叙述，因此接下来例子将延续上一章中的”苏格拉底证明”，将它彻底形式化.

首先定义我们的语言 $\mathcal{L}$，由于逻辑符号总是必要的，因此是自然给出了的，只约定后面的变元都用 $x, y, z$ 来表示. 在非逻辑符号上，我们给出：

• 一个常数符号 $s$
• 两个 $1$-元谓词符号 $\text{Human}$、$\text{Mortal}$
• 等词符号 $\approx$

在这里我们定义了一些符号，尚没有给它们任何解释. 但直觉地看，我们可以读出此处定义了一个常量”苏格拉底”，与两个谓词，分别判断某个变量是不是人和某个变量会不会死.

我们可以写一些公式如下，比如：

• $\forall x(\text{Human}(x))$，表示所有 $x$ 都是人
• $\forall x (x \approx s)$，表示所有 $x$ 都是苏格拉底
• $\text{Mortal}(s)$，表示苏格拉底会死

现在，我们来尝试做一个证明. 先给出我们的公式集，也就是我们设定的公理：

$\Gamma = \{\text{Human}(s), \forall x(\text{Human}(x) \to \text{Mortal}(x))\}$

在此基础上，我们来证明”苏格拉底会死”：$\phi = \text{Mortal}(s)$

$\Gamma$ 到 $\phi$ 的推演由下述公式序列来定义：

1. $\forall x(\text{Human}(x) \to \text{Mortal}(x))$
2. $\forall x(\text{Human}(x) \to \text{Mortal}(x)) \to (\text{Human}(s) \to \text{Mortal}(s))$
3. $\text{Human}(s) \to \text{Mortal}(s)$
4. $\text{Human}(s)$
5. $\text{Mortal}(s)$

这里的每一步都是按照严格的推演要求完成的，具体地说：

1. 来自公式集 $\Gamma$
2. 由逻辑公理 2 构造得到
3. 由 1 和 2 通过分离规则得到
4. 来自公式集 $\Gamma$
5. 由 3 和 4 通过分离规则得到

因此，我们就完成了证明，发现苏格拉底会死是一个公式集的内命题.

下面，可以给出我们的结构 $\mathfrak{A}$，以对我们的语言和推理做真正的解释. 具体说来，论域 $A = \{\text{苏格拉底}\}$，且

• $s^{\mathfrak{A}} = \text{苏格拉底}$
• $\text{Human}^{\mathfrak{A}} = \{\text{苏格拉底}\}$
• $\text{Mortal}^{\mathfrak{A}} = \{\text{苏格拉底}\}$

在这个结构下，很容易按照定义来验证：我们在公式集中定义的两个公式都是被满足的，或者说，她们作为语句，都是真的. 不难发现，我们证明出的语句 $\text{Mortal}(s)$ 也是真的，这也就验证了我们证明是符合直觉的——从真的命题出发，证明了真的命题.