#代数结构与数理逻辑学习笔记7
定义 17.1 论说、演绎与一致性
先讨论自然语言中的论说
一个论说通常由若干前提和一个结论组成： \[ \frac{P_1,\ P_2,\ \dots,\ P_n}{C} \]
其中 \(P_1,\dots,P_n\) 是前提，\(C\) 是结论
论说的好坏不取决于结论事实上是否为真，而取决于前提是否足以支持结论
若不存在前提全真而结论假的情形，则称该论说是有效的
若一组命题不可能同时为真，则称这组命题是不一致的；否则称为一致的
因此：
- 有效性关心“前提真时结论是否必真”
- 一致性关心“一组命题是否能同时为真”
- 反证法本质上把有效性转化为不一致性
定义 17.1.1 论说的好坏
论说的评价可以分成两个层次：
- 前提是否可接受
- 从前提到结论的过渡是否可靠
逻辑主要研究第二个问题，也就是说，逻辑并不首先判断前提事实上是否真，而是判断： \[ \text{如果前提都真，结论是否必真} \]
例如：
\[ \frac{\text{所有人都会死},\quad \text{苏格拉底是人}}{\text{苏格拉底会死}} \]
这个论说在形式上有效。即使有人争论某个前提，逻辑形式仍然是可靠的
而 \[ \frac{\text{所有猫都是动物},\quad \text{狗是动物}}{\text{狗是猫}} \]
前提可以都真，但结论假，所以形式无效
形式化以后，上面两个论说分别对应：
\[ \frac{\forall x(H(x)\to M(x)),\ H(s)}{M(s)} \]
和
\[ \frac{\forall x(C(x)\to A(x)),\ A(d)}{C(d)} \]
第二个形式犯的是“肯定后件”的错误
定义 17.1.2 可演绎性、可证性和独立性
设 \(T\) 是一组命题或公式，\(A\) 是一个命题或公式
若 \(A\) 可以从 \(T\) 中通过允许的推理规则推出，则称 \(A\) 从 \(T\) 可演绎，记作 \[ T\vdash A \]
若没有前提也能推出 \(A\)，则称 \(A\) 可证： \[ \vdash A \]
若 \[ T\not\vdash A \] 且 \[ T\not\vdash \neg A \] 则称 \(A\) 相对于 \(T\) 是独立的
独立性表示：在给定前提或公理系统 \(T\) 中，既不能证明 \(A\)，也不能证明其否定
定义 17.1.3 一致性与爆炸原则
若一个系统或公式集 \(T\) 能推出某个公式及其否定： \[ T\vdash A,\qquad T\vdash\neg A \] 则称 \(T\) 不一致
若不存在这样的 \(A\)，则称 \(T\) 一致
在经典逻辑中，不一致会导致爆炸原则： \[ A,\neg A\vdash B \] 其中 \(B\) 是任意公式
证明： 点击查看证明
由 \(A\) 可得 \[ A\vee B \] 这是析取引入。
又有 \(\neg A\)
由析取三段论： \[ A\vee B,\quad \neg A\vdash B \]
因此从矛盾 \(A,\neg A\) 可以推出任意 \(B\)
定理 17.1.1 有效性与不一致性
设 \(P_1,\dots,P_n,C\) 是命题，则 \[ P_1,\dots,P_n\models C \] 当且仅当 \[ P_1,\dots,P_n,\neg C \] 不一致
证明： 点击查看证明
若 \(P_1,\dots,P_n\models C\)，则不存在一种情形使所有 \(P_i\) 为真而 \(C\) 为假
但 \(C\) 为假正是 \(\neg C\) 为真，所以不存在一种情形使 \[ P_1,\dots,P_n,\neg C \] 同时为真，即它们不一致
反过来，若 \(P_1,\dots,P_n,\neg C\) 不一致，则不可能所有 \(P_i\) 为真且 \(\neg C\) 为真
也就是说，只要所有 \(P_i\) 为真，\(C\) 就不能为假，只能为真
所以 \[ P_1,\dots,P_n\models C \]
定义 17.2 形式语言与形式系统
形式逻辑首先要把自然语言论说翻译成形式语言，然后在形式系统中推演
一个形式系统通常包含：
- 字母表：允许使用哪些符号
- 形成规则：哪些符号串是合式公式
- 公理或初始公式：哪些公式可直接使用
- 推理规则：怎样从已有公式推出新公式
命题逻辑中，字母表一般包括：
- 命题变元：\(p,q,r,p_1,p_2,\dots\)
- 联结词：\(\neg,\wedge,\vee,\to,\leftrightarrow\)
- 括号和辅助符号
一阶逻辑中，还要加入：
- 个体变元与个体常元
- 函数符号
- 谓词符号
- 等词 \(=\)
- 量词 \(\forall,\exists\)
定义 17.2.1 对象语言与元语言
对象语言是被研究的形式语言。例如命题逻辑中的 \[ (p\to q)\wedge p \] 是一条对象语言公式
元语言是用来谈论对象语言的语言，例如：
- “\(A\) 是公式”
- “\(A\) 是重言式”
- “\(\Gamma\vdash A\)”
- “\(\Gamma\models A\)”
常见记号区别如下：
| 记号 | 层次 | 含义 |
|---|---|---|
| \(\to\) | 对象语言 | 公式内部的蕴含联结词 |
| \(\Rightarrow\) | 元语言 | “推出”“因此” |
| \(\vdash\) | 元语言 | 形式可证 |
| \(\models\) | 元语言 | 语义有效或语义后承 |
| \(\equiv\) | 元语言 | 两个公式等值 |
\[ A\to B \] 是一个公式；而 \[ A\models B \] 不是公式，而是说“所有使 \(A\) 为真的解释也使 \(B\) 为真”
定义 17.2.2 推演、定理与可证性
在形式系统中，从公式集 \(\Gamma\) 推出公式 \(A\)，记作 \[ \Gamma\vdash A \]
含义是：存在一个有限公式序列，每一步要么是 \(\Gamma\) 中的前提，要么是公理，要么由前面若干步按推理规则得到，最后一步是 \(A\)
若 \[ \varnothing\vdash A \] 则称 \(A\) 是系统中的定理，通常简写为 \[ \vdash A \]
这里要区分：
- \(\Gamma\models A\) 表示语义后承，即所有解释下前提真则结论真
- \(\Gamma\vdash A\) 表示形式可证，即有一个形式推演序列
可靠性和完全性正是研究这两个关系之间的联系
定义 17.2.3 形式系统的四个问题
可靠性： \[ \Gamma\vdash A \Rightarrow \Gamma\models A \]
完全性： \[ \Gamma\models A \Rightarrow \Gamma\vdash A \]
一致性： 是否存在 \(A\) 使得 \[ \Gamma\vdash A,\qquad \Gamma\vdash\neg A \]
可判定性： 是否存在机械过程，对任意公式 \(A\)，都能在有限步内判断 \(A\) 是否可证或是否有效
命题逻辑是可判定的，因为可以列真值表
一阶逻辑有效性不是一般可判定的，但它是半可判定的：若一个公式有效，原则上可以通过枚举证明最终找到证明；若无效，则不一定能有限步停机确认
定义 17.3 可靠性与完全性
一个形式系统若满足： \[ \Gamma\vdash A \Rightarrow \Gamma\models A \] 则称它是可靠的
可靠性说明：系统中能证明出来的结论不会在语义上出错
一个形式系统若满足： \[ \Gamma\models A \Rightarrow \Gamma\vdash A \] 则称它是完全的
完全性说明：所有语义上有效的结论，都能在系统中被形式证明出来
如果同时有可靠性和完全性，则形式证明与语义有效性完全吻合： \[ \Gamma\vdash A \iff \Gamma\models A \]
定理 17.3.1 可靠性的证明思路
若形式系统的每条公理都是有效式，并且每条推理规则都保持有效性，则该形式系统可靠
证明： 点击查看证明
设 \[ \Gamma\vdash A \] 即存在一个从 \(\Gamma\) 到 \(A\) 的有限推演序列
对推演序列的长度作归纳。
若某一步是前提，则它在所有满足 \(\Gamma\) 的解释下为真
若某一步是公理，则由假设，公理是有效式，在所有解释下为真
若某一步由前面若干步通过推理规则得到，由归纳假设，前面若干步在所有满足 \(\Gamma\) 的解释下为真；又推理规则保持有效性，所以这一步也为真
因此推演最后一步 \(A\) 在所有满足 \(\Gamma\) 的解释下为真，即 \[ \Gamma\models A \]
注记 17.3.2 完全性的意义
可靠性通常只要逐条检查公理和规则；完全性要说明：只要一个公式在语义上不可反驳，就一定能在形式系统中找到证明
在命题逻辑中，完全性可以借助真值表或主范式证明
在一阶逻辑中，完全性对应 Gödel 完全性定理，其内容是： \[ \Gamma\models A \Rightarrow \Gamma\vdash A \]
这和后面的 Gödel 不完全性定理不是同一个命题。完全性定理说的是“一阶逻辑本身的推理系统足够强”；不完全性定理说的是“足够表达算术的具体理论不可能同时满足某些理想性质”。
定义 17.4 命题演算的语义概念
设 \(A\) 是命题公式，\(v\) 是真值指派。
若 \(v(A)=1\)，称 \(v\) 满足 \(A\)，记作 \[ v\models A \]
若 \(v\) 满足公式集 \(\Gamma\) 中所有公式，记作 \[ v\models\Gamma \]
若存在某个 \(v\) 满足 \(\Gamma\)，则称 \(\Gamma\) 可满足
若没有任何 \(v\) 满足 \(\Gamma\)，则称 \(\Gamma\) 不可满足
若每个满足 \(\Gamma\) 的真值指派都满足 \(A\)，则称 \(A\) 是 \(\Gamma\) 的语义后承： \[ \Gamma\models A \]
特别地，若 \(\varnothing\models A\)，则称 \(A\) 是重言式或有效式
定理 17.4.1 语义后承与不可满足
\[ \Gamma\models A \iff \Gamma\cup\{\neg A\}\text{ 不可满足} \]
证明： 点击查看证明
若 \(\Gamma\models A\)，则任意满足 \(\Gamma\) 的真值指派都满足 \(A\)
因此不可能存在真值指派同时满足 \(\Gamma\) 和 \(\neg A\)
所以 \(\Gamma\cup\{\neg A\}\) 不可满足
反过来，若 \(\Gamma\cup\{\neg A\}\) 不可满足，则不存在真值指派满足 \(\Gamma\) 且使 \(A\) 为假
于是每个满足 \(\Gamma\) 的真值指派都满足 \(A\)，即 \[ \Gamma\models A \]
定理 17.4.2 命题逻辑的可判定性
命题公式 \(A\) 是否为重言式是可判定的
证明： 点击查看证明
若 \(A\) 中只出现 \[ p_1,\dots,p_n \] 这 \(n\) 个命题变元，则 \(A\) 的真值只由这 \(n\) 个变元的取值决定
共有 \(2^n\) 种赋值
逐一计算 \(A\) 在这 \(2^n\) 个赋值下的真值：
- 若每行都为 \(1\)，则 \(A\) 是重言式
- 若至少一行为 \(0\)，则 \(A\) 不是重言式
这个过程有限步结束，所以重言式判定是可判定的
定义 17.5 费奇式推演
讲义把命题演算看成从“语义判断”进入“形式推演”的阶段：
- 语义判断使用 \(\models\)，依靠真值指派
- 形式推演使用 \(\vdash\)，依靠推理规则
- 可靠性证明 \(\vdash\) 不会推出语义错误的结论
- 完全性证明所有语义有效的结论都能被规则推出
费奇式推演的特点是用缩进或竖线表示临时假设的作用范围。
典型结构如下：
\[ \begin{array}{ll} 1. & A \quad \text{假设}\\ 2. & \cdots\\ 3. & B\\ 4. & A\to B \quad \to\text{ 引入} \end{array} \]
这表示：若在临时假设 \(A\) 下推出了 \(B\)，则可退出该假设，得到 \(A\to B\)
费奇式推演常用规则包括：
- 合取引入：由 \(A\) 与 \(B\) 得 \(A\wedge B\)
- 合取消去：由 \(A\wedge B\) 得 \(A\)，也可得 \(B\)
- 析取引入：由 \(A\) 得 \(A\vee B\)
- 蕴含消去：由 \(A\to B\) 与 \(A\) 得 \(B\)
- 蕴含引入：若假设 \(A\) 能推出 \(B\)，则得 \(A\to B\)
- 否定引入：若假设 \(A\) 导出矛盾，则得 \(\neg A\)
- 否定消去：由 \(A\) 与 \(\neg A\) 得矛盾
定义 17.5.1 子证明
费奇式推演的核心是子证明
子证明以一个临时假设开始： \[ [A] \]
在该假设作用范围内推出若干公式。退出子证明后，可以使用引入规则把整段子证明包装成一个公式
最常见的是蕴含引入： \[ \begin{array}{c} [A]\\ \vdots\\ B\\ \hline A\to B \end{array} \]
其意思是：如果在假设 \(A\) 的条件下可以推出 \(B\)，那么无条件地可以推出 \(A\to B\)
否定引入类似： \[ \begin{array}{c} [A]\\ \vdots\\ \bot\\ \hline \neg A \end{array} \]
其中 \(\bot\) 表示矛盾
定义 17.5.2 析取消去
费奇式推演中，析取消去常写为分情况讨论：
若有 \[ A\vee B \] 并且：
- 在假设 \(A\) 下能推出 \(C\)
- 在假设 \(B\) 下也能推出 \(C\)
则可推出 \(C\)。
形式为： \[ \begin{array}{c} A\vee B\\ [A]\quad \vdots\quad C\\ [B]\quad \vdots\quad C\\ \hline C \end{array} \]
这对应自然语言中的“分情况讨论”：无论析取式哪一边成立，结论 \(C\) 都成立
例 17.5.3 费奇式证明假言三段论
证明： \[ A\to B,\ B\to C\vdash A\to C \]
推演：
| 步骤 | 公式 | 理由 |
|---|---|---|
| 1 | \(A\to B\) | 前提 |
| 2 | \(B\to C\) | 前提 |
| 3 | \(A\) | 临时假设 |
| 4 | \(B\) | 1,3 蕴含消去 |
| 5 | \(C\) | 2,4 蕴含消去 |
| 6 | \(A\to C\) | 3-5 蕴含引入 |
其中第 3 步的假设只在子证明中有效；第 6 步退出该假设，得到条件命题
例 17.5.4 费奇式证明反证法
证明： \[ A\to B,\ A\to\neg B\vdash \neg A \]
推演：
| 步骤 | 公式 | 理由 |
|---|---|---|
| 1 | \(A\to B\) | 前提 |
| 2 | \(A\to\neg B\) | 前提 |
| 3 | \(A\) | 临时假设 |
| 4 | \(B\) | 1,3 蕴含消去 |
| 5 | \(\neg B\) | 2,3 蕴含消去 |
| 6 | \(\bot\) | 4,5 矛盾 |
| 7 | \(\neg A\) | 3-6 否定引入 |
这正是反证思路：假设 \(A\)，推出矛盾，于是得到 \(\neg A\)
定义 17.6 命题演算中的极大一致集
设 \(\Gamma\) 是一组命题公式
若 \(\Gamma\) 不能推出矛盾，则称 \(\Gamma\) 是一致的
若 \(\Gamma\) 一致，并且对任意公式 \(A\)，只要 \(A\notin\Gamma\)，则 \[ \Gamma\cup\{A\} \] 不一致，则称 \(\Gamma\) 是极大一致集
极大一致集可以理解为“已经尽可能完整而又不矛盾的一套命题选择”
定理 17.6.1 Lindenbaum 扩张思想
任意一致的命题公式集 \(\Gamma\) 都可以扩张为某个极大一致集 \(\Delta\)，使得 \[ \Gamma\subseteq\Delta \]
证明： 点击查看证明
把所有命题公式排成一个序列： \[ A_1,A_2,A_3,\dots \]
从 \(\Gamma_0=\Gamma\) 开始递归构造：
若 \[ \Gamma_n\cup\{A_{n+1}\} \] 一致，则令 \[ \Gamma_{n+1}=\Gamma_n\cup\{A_{n+1}\} \]
否则令 \[ \Gamma_{n+1}=\Gamma_n\cup\{\neg A_{n+1}\} \]
最后令 \[ \Delta=\bigcup_{n=0}^{\infty}\Gamma_n \]
每一步都保持一致；若加入 \(A_{n+1}\) 会不一致，则加入 \(\neg A_{n+1}\) 保持一致，否则原来的 \(\Gamma_n\) 会已经推出 \(A_{n+1}\) 与 \(\neg A_{n+1}\) 的矛盾
构造后，对任意公式 \(A_i\)，恰有 \(A_i\) 或 \(\neg A_i\) 被加入 \(\Delta\)
因此 \(\Delta\) 是极大一致集
定理 17.6.2 极大一致集的基本性质
若 \(\Delta\) 是极大一致集，则对任意命题公式 \(A,B\)：
- 恰有一个在 \(\Delta\) 中：\(A\) 或 \(\neg A\)
- \(A\wedge B\in\Delta\) 当且仅当 \(A\in\Delta\) 且 \(B\in\Delta\)
- \(A\vee B\in\Delta\) 当且仅当 \(A\in\Delta\) 或 \(B\in\Delta\)
- \(A\to B\in\Delta\) 当且仅当 \(A\notin\Delta\) 或 \(B\in\Delta\)
证明： 点击查看证明
这里只说明思路
由于 \(\Delta\) 极大一致，对任意公式 \(A\)，若 \(A\notin\Delta\)，则加入 \(A\) 会导致不一致
这意味着从 \(\Delta\cup\{A\}\) 可推出矛盾，因此从 \(\Delta\) 可推出 \(\neg A\)，于是 \(\neg A\) 必须属于极大一致集
同时 \(A\) 与 \(\neg A\) 不能都在 \(\Delta\) 中，否则 \(\Delta\) 本身不一致
所以 \(A\) 与 \(\neg A\) 恰有一个在 \(\Delta\) 中
其他三条由对应联结词的引入和消去规则推出。例如 \(A\wedge B\) 在 \(\Delta\) 中，则由合取消去得 \(A,B\) 都应在 \(\Delta\) 中；反过来若 \(A,B\) 都在 \(\Delta\) 中，则由合取引入得 \(A\wedge B\) 在 \(\Delta\) 中
析取和蕴含情形类似
定理 17.6.3 命题演算完全性的证明骨架
若 \[ \Gamma\models A \] 则 \[ \Gamma\vdash A \]
证明： 点击查看证明
证明逆否命题
假设 \[ \Gamma\not\vdash A \]
则 \[ \Gamma\cup\{\neg A\} \] 是一致的；否则若它不一致，就可由反证法推出 \(\Gamma\vdash A\)
由 Lindenbaum 扩张思想，把 \[ \Gamma\cup\{\neg A\} \] 扩张为极大一致集 \(\Delta\)
根据极大一致集的性质，定义真值指派 \(v_\Delta\)： \[ v_\Delta(p)=1 \iff p\in\Delta \]
再由极大一致集关于联结词的性质可得： \[ v_\Delta(B)=1 \iff B\in\Delta \] 对任意命题公式 \(B\) 成立
由于 \[ \Gamma\subseteq\Delta \] 所以 \(v_\Delta\) 满足 \(\Gamma\)。
又因为 \[ \neg A\in\Delta \] 所以 \(v_\Delta(A)=0\)
因此存在一个满足 \(\Gamma\) 但不满足 \(A\) 的赋值，说明 \[ \Gamma\not\models A \]
于是逆否命题成立，即 \[ \Gamma\models A\Rightarrow\Gamma\vdash A \]
定义 17.7 谓词演算中的量词规则
在一阶谓词演算中，除了命题联结词规则，还需要量词规则
- 先处理没有等词的一阶推演，核心是量词引入和量词消去
- 再加入等词，得到带等词的谓词逻辑
- 最后讨论谓词演算的可靠性、完全性以及由完全性导出的元逻辑结果
量词规则比命题规则更容易出错，因为它们涉及“任意对象”“某个对象”和变量是否自由。
定义 17.7.1 自由变元、约束变元和可替换性
在公式 \[ \forall xA \] 或 \[ \exists xA \] 中，量词后面的 \(A\) 是量词的辖域
若变元 \(x\) 的出现位于某个 \(\forall x\) 或 \(\exists x\) 的辖域内，则这次出现是约束的；否则是自由的
例如： \[ \forall x(P(x)\to Q(y)) \] 中，\(x\) 是约束变元，\(y\) 是自由变元
在量词规则中，经常需要把项 \(t\) 代入公式 \(A(x)\) 中的自由 \(x\)
这种代入必须避免变量捕获
例如： \[ \forall yR(x,y) \] 中，把 \(y\) 代入 \(x\) 会得到 \[ \forall yR(y,y) \]
原来作为自由项出现的 \(y\) 被 \(\forall y\) 捕获，因此这个代入不合法
所以全称消去和存在引入中都要附加条件：项 \(t\) 对 \(x\) 可自由代入
常见规则包括：
全称消去： \[ \frac{\forall xA(x)}{A(t)} \] 其中 \(t\) 可以代入 \(x\)，且不能造成变量捕获
存在引入： \[ \frac{A(t)}{\exists xA(x)} \]
全称引入： 若在不依赖于关于 \(x\) 的特殊假设的情况下推出 \(A(x)\)，则可推出 \[ \forall xA(x) \]
存在消去： 若由 \(\exists xA(x)\) 可临时取一个新的对象 \(c\) 满足 \(A(c)\)，并在不依赖 \(c\) 特殊性的情况下推出 \(B\)，则可推出 \(B\)
存在消去中的“新对象”条件很重要：\(c\) 不能已经出现在未解除的前提或结论中，否则会把“存在某个对象”误用成“某个指定对象”
定理 17.7.2 全称消去可靠
若 \[ \forall xA(x) \] 成立，则对任意可代入项 \(t\)， \[ A(t) \] 成立。
证明： 点击查看证明
\(\forall xA(x)\) 的含义是：论域中任意对象都满足 \(A\)
项 \(t\) 在给定解释下表示论域中的某个对象
既然任意对象都满足 \(A\)，那么 \(t\) 所表示的对象也满足 \(A\)
所以可推出 \[ A(t) \]
可代入条件保证代入没有改变公式中变量的绑定关系。
定理 17.7.3 存在消去的新常元条件
从 \[ \exists xA(x) \] 使用存在消去时，引入的新常元 \(c\) 不能出现在当前未解除的前提或最终结论中
证明： 点击查看证明
\(\exists xA(x)\) 只说明“至少有一个对象满足 \(A\)”，没有说明是哪一个对象
因此临时引入的 \(c\) 只能表示“某个任意选取的见证对象”
如果 \(c\) 已经出现在前提或结论中，就可能把“存在某个对象”误读为“这个指定对象”
例如从 \[ \exists xP(x) \] 不能推出 \[ P(a) \] 因为 \(a\) 可能不是那个满足 \(P\) 的对象。
所以存在消去要求 \(c\) 是新常元，并且最终推出的结论不能依赖 \(c\) 的特殊名字
例 17.7.4 量词推演
证明： \[ \forall x(P(x)\to Q(x)),\ \forall xP(x)\vdash \forall xQ(x) \]
推演：
| 步骤 | 公式 | 理由 |
|---|---|---|
| 1 | \(\forall x(P(x)\to Q(x))\) | 前提 |
| 2 | \(\forall xP(x)\) | 前提 |
| 3 | \(P(a)\to Q(a)\) | 1 全称消去 |
| 4 | \(P(a)\) | 2 全称消去 |
| 5 | \(Q(a)\) | 3,4 蕴含消去 |
| 6 | \(\forall xQ(x)\) | 5 全称引入 |
这里 \(a\) 是任意对象，没有使用关于 \(a\) 的特殊前提，所以最后可以全称引入
例 17.7.5 存在消去示例
证明： \[ \exists x(P(x)\wedge Q(x))\vdash \exists xP(x) \]
推演：
| 步骤 | 公式 | 理由 |
|---|---|---|
| 1 | \(\exists x(P(x)\wedge Q(x))\) | 前提 |
| 2 | \(P(c)\wedge Q(c)\) | 存在消去临时假设，\(c\) 新 |
| 3 | \(P(c)\) | 2 合取消去 |
| 4 | \(\exists xP(x)\) | 3 存在引入 |
| 5 | \(\exists xP(x)\) | 1,2-4 存在消去 |
第 5 步退出关于 \(c\) 的临时假设，因为最终结论 \(\exists xP(x)\) 不含 \(c\)
定义 17.8 等词与相等规则
带等词的一阶逻辑把 \(=\) 作为逻辑符号
等词通常满足：
自同一性： \[ x=x \]
替换性： 若 \[ x=y \] 且公式 \(A(x)\) 成立，则可推出 \[ A(y) \]
也就是说，相等对象在任意性质和关系中可以相互替换
例 17.8.1 等词推理
由 \[ a=b,\quad P(a) \] 可推出 \[ P(b) \]
这是替换性的直接应用。
若有函数符号 \(f\)，由 \[ a=b \] 也可推出 \[ f(a)=f(b) \]
这表示函数对相等对象取相等值。
定理 17.8.2 等词的同余性质
若 \[ a_1=b_1,\dots,a_n=b_n \] 则对任意 \(n\) 元函数符号 \(f\)， \[ f(a_1,\dots,a_n)=f(b_1,\dots,b_n) \]
对任意 \(n\) 元谓词符号 \(R\)， \[ R(a_1,\dots,a_n)\leftrightarrow R(b_1,\dots,b_n) \]
证明： 点击查看证明
这是相等替换性的多次应用
函数情形：从 \(a_1=b_1\) 可把 \(f(a_1,a_2,\dots,a_n)\) 中第一处替换为 \(b_1\)；再用 \(a_2=b_2\) 替换第二处，如此继续，最后得到 \[ f(a_1,\dots,a_n)=f(b_1,\dots,b_n) \]
谓词情形同理。若 \[ R(a_1,\dots,a_n) \] 成立，则逐项用 \(a_i=b_i\) 替换，得 \[ R(b_1,\dots,b_n) \]
反向由 \(b_i=a_i\) 得到。
定义 17.9 Henkin 思想
若有公式 \[ \exists xA(x) \] 则引入一个新的常元 \(c\)，并加入公式 \[ \exists xA(x)\to A(c) \]
这个 \(c\) 称为该存在公式的见证常元。
直观上，如果存在某个对象满足 \(A\)，就给这样一个对象起一个新名字。
定理 17.9.1 Henkin 见证的作用
加入足够多的 Henkin 见证后，极大一致理论可以构造出一个模型
证明： 点击查看证明
这里只写证明思路
设 \(\Delta\) 是带 Henkin 见证的极大一致理论
用语言中的闭项构成模型的对象
若有等词，则把可证明相等的闭项看成同一个对象
谓词解释为： \[ R(t_1,\dots,t_n)\text{ 在模型中为真} \] 当且仅当 \[ R(t_1,\dots,t_n)\in\Delta \]
函数解释按项的构造给出。
关键在于存在量词：若 \[ \exists xA(x)\in\Delta \] 则 Henkin 公理保证某个见证常元 \(c\) 满足 \[ A(c)\in\Delta \]
于是存在命题在构造出的模型中确实有见证
这样就能证明 \(\Delta\) 中每个公式都在该模型中为真，从而得到模型存在
定义 17.10 紧致性
一阶逻辑的紧致性定理说：
若公式集 \(\Gamma\) 的每个有限子集都有模型，则 \(\Gamma\) 有模型
等价地：
若 \[ \Gamma\models A \] 则存在有限子集 \[ \Gamma_0\subseteq\Gamma \] 使得 \[ \Gamma_0\models A \]
紧致性说明：一阶逻辑的语义后承虽然可以有无限多前提，但真正推出某个公式时，只需要有限多个前提
定理 17.10.1 紧致性来自完全性
若一阶逻辑可靠且完全，则可推出紧致性
证明： 点击查看证明
设 \(\Gamma\models A\)
由完全性， \[ \Gamma\vdash A \]
形式证明是有限长的，所以证明中实际用到的前提只可能是 \(\Gamma\) 中有限多个公式。设这些公式组成有限集 \(\Gamma_0\)。
则 \[ \Gamma_0\vdash A \]
由可靠性， \[ \Gamma_0\models A \]
所以只需有限前提即可推出 \(A\)
令 \(A\) 为矛盾式，也得到“若每个有限子集可满足，则整体可满足”的形式
例 17.10.2 紧致性的应用
存在一个一阶理论，它有任意大的有限模型约束，并因此有无限模型
设语言中有无穷多个常元 \[ c_0,c_1,c_2,\dots \]
加入公式： \[ c_i\neq c_j\qquad (i\neq j) \]
任取有限多个这样的公式，只涉及有限多个常元，可以用一个足够大的有限集合解释这些常元，使它们两两不同
所以每个有限子集都有模型
由紧致性，整个公式集有模型
在这个模型中，所有 \(c_i\) 解释为两两不同的对象，因此模型必须是无限的
这个例子说明，一阶逻辑可以通过无限理论“逼出”无限模型，但单个一阶句子通常不能表达“论域无限”
定义 17.11 Löwenheim-Skolem 定理
Löwenheim-Skolem 定理讨论一阶理论模型的大小
若一个可数一阶理论有无限模型，则它有可数无限模型
更一般地，一阶理论如果有足够大的无限模型，往往也有较小基数的模型
这个定理体现了一阶逻辑表达能力的限制：一阶句子通常不能唯一刻画某个无限结构的基数
注记 17.11.1 Skolem 悖论
集合论可以在一阶语言中谈论不可数集合；但 Löwenheim-Skolem 定理又说明，如果这个一阶理论有模型，则在适当条件下它有可数模型
于是出现所谓 Skolem 悖论：可数模型内部也可能“认为”某个集合不可数
关键在于：
- “可数模型”是从模型外部看的大小
- “不可数”是模型内部没有某个双射对象
内外视角不同，所以并不真正矛盾
例 17.11.2 一阶逻辑不能刻画“恰为标准自然数模型”
一阶 Peano 算术有标准模型 \(\mathbb{N}\)
但由 Löwenheim-Skolem 和紧致性相关思想可知，一阶 Peano 算术也有非标准模型
这些模型中除了 \[ 0,1,2,\dots \] 所对应的标准部分，还存在“非标准自然数”
因此，一阶公理可以刻画许多算术性质，却不能把自然数结构唯一固定到只剩标准模型
定义 17.12 可定义性
在一个结构中，若某个集合或关系可以由一阶公式刻画，则称它是可定义的
设结构为 \(\mathcal{M}\)，公式为 \(A(x)\)。若 \[ S=\{a\in M\mid \mathcal{M}\models A(a)\} \] 则称 \(S\) 由公式 \(A(x)\) 定义
如果公式中允许参数，则称为带参数可定义；否则称为无参数可定义
例 17.12.1 在整数结构中的可定义性
在结构 \[ (\mathbb{Z},+,\times,0,1) \] 中，偶数集合可以用公式 \[ \exists y(x=y+y) \] 定义
因为 \(x\) 是偶数，当且仅当存在整数 \(y\) 使 \[ x=2y=y+y \]
定义 17.12.2 显式可定义与隐式可定义
若一个关系可以直接由某个公式定义，称为显式可定义
若一个关系虽然没有给出直接公式，但在结构或理论中被其他符号唯一决定，称为隐式可定义
在经典模型论中有 Beth 可定义性定理：
若一个关系在一阶理论中隐式可定义，则它也显式可定义
直观地说，一阶逻辑中“被唯一决定”和“可用公式写出来”在这种意义下是一致的
定义 17.13 不完全性
不完全性并非对一阶逻辑的完全性定理的否定
一阶逻辑完全性定理说： \[ \Gamma\models A \Rightarrow \Gamma\vdash A \]
Gödel 不完全性定理讨论的是能表达足够算术的形式理论 \(T\)
粗略说，若 \(T\) 满足：
- \(T\) 是一致的
- \(T\) 的公理和证明可有效识别
- \(T\) 足够表达基本算术
则存在算术命题 \(G\)，使得在 \(T\) 中既不能证明 \(G\)，也不能证明 \(\neg G\)
这说明：足够强的一致形式算术理论不可能把所有算术真理都证明出来
定义 17.13.1 算术化
Gödel 不完全性证明的关键技术是算术化
它把符号、公式、证明这些语法对象编码为自然数。
例如可以给每个基本符号分配一个自然数编码，再把有限符号串编码成一个自然数
这样，“\(n\) 是某个公式的编码”“\(m\) 是公式 \(n\) 的证明编码”这类语法命题就可以转化为关于自然数的算术命题
一旦语法可以在算术内部表达，理论就可以谈论自身的证明行为
定义 17.13.2 自指句
不完全性证明构造一个句子 \(G\)，其直观含义是： \[ G \equiv \text{“我不可在 }T\text{ 中证明”} \]
若 \(T\) 证明了 \(G\)，则 \(G\) 所说的“我不可证明”就是假的，从而导致不一致
若 \(T\) 证明了 \(\neg G\)，则相当于证明“\(G\) 可证明”，在适当条件下也会导致问题
因此在一致且足够强的理论中，\(G\) 既不可证也不可反证
注记 17.13.3 第一不完全性与第二不完全性
第一不完全性定理：
足够强且一致的可有效公理化理论是不完全的，即存在既不能证明也不能反证的命题
第二不完全性定理：
足够强且一致的理论不能在自身内部证明自己的相容性
直观地说，形式系统可以非常强，但只要它足够表达算术并保持一致，就无法完全封闭地证明自身没有矛盾