谓词逻辑
00:00
量词、谓词公式、等值演算、前束范式、推理理论、一阶逻辑形式化。
1. 量词与谓词
1.1 谓词
谓词表示个体的性质或个体间的关系。
- 一元谓词 ： 具有性质
- 二元谓词 ： 和 具有关系
- 元谓词
论域（个体域）：个体变元的取值范围。
1.2 量词
全称量词 ： 表示”对所有 ， 成立”。
存在量词 ： 表示”存在 ，使得 成立”。
1.3 量词与联结词的关系
在有限论域 上：
1.4 量词的否定
例：
2. 谓词公式
2.1 项与公式
项的递归定义：
- 个体常量和个体变元是项
- 若 是 元函数符号， 是项，则 是项
原子公式：，其中 是谓词符号， 是项。
合式公式：由原子公式通过联结词和量词递归构造。
2.2 自由变元与约束变元
- 约束变元：出现在量词作用范围内的变元，如 中的
- 自由变元：不受量词约束的变元，如 中的
闭公式：不含自由变元的公式。
2.3 量词的辖域
中 的辖域仅为 ， 中的 是自由的。
2.4 约束变元换名
可将约束变元换名为不出现在公式中的其他变元：
3. 等值演算
3.1 基本等值式
量词德摩根律：
量词分配律：
注意：，
量词与蕴含：
3.2 量词的顺序
不同量词不可交换：
例： 为真（对每个 ，取 ），但 为假（不存在一个 对所有 满足 ）。
4. 前束范式
4.1 定义
前束范式：所有量词都在公式最前面的等值形式，形如
其中 ， 为不含量词的公式（称为母式）。
4.2 求前束范式的步骤
- 消去 和
- 将 内移至原子公式前
- 约束变元换名（使不同量词使用不同变元名）
- 将量词前移
例：求 的前束范式。
- 换名：
- 量词前移：
4.3 Skolem 范式
将前束范式中的存在量词用 Skolem 函数消去：
- 前面有 ：用 替换
- 前面无全称量词：用常量 替换
例： 的 Skolem 化：用 替换 ，得 。
5. 推理理论
5.1 推理规则
全称量词消去（UI）：（ 为论域中任意个体）
全称量词引入（UG）：（ 为任意个体）
存在量词消去（EI）：（ 为特定个体，不能是已有常量）
存在量词引入（EG）：
5.2 推理注意事项
- EI 必须在 UI 之前使用
- EI 引入的常量不能在其他前提中出现
- UG 要求变元是任意的
例：前提 ，。结论 。
- （前提）
- （EI，1）
- （前提）
- （UI，3）
- （MP，2, 4）
- （EG，5）
6. 一阶逻辑形式化
6.1 形式化步骤
- 确定论域
- 定义谓词
- 将自然语言翻译为谓词公式
例：将”所有实数都大于或等于某个整数”形式化。
论域：实数集 谓词： 表示 ， 表示 是整数
例：将”存在唯一的 使得 成立”形式化。
也可记为 。
6.2 常见形式化模式
| 自然语言 | 形式化 |
|---|---|
| 所有 都是 | |
| 有些 是 | |
| 没有 是 | |
| 并非所有 都是 |
注意：“所有 都是 ” 形式化为 ，而非 。后者要求论域中所有元素都是 且都是 。
6.3 嵌套量词的理解
“每个人都爱某个人”——对每个人，都存在一个人被他爱。
“有一个人被所有人爱”——存在一个人，所有人都爱他。
两者的逻辑强度不同，后者更强。