type
status
date
slug
summary
tags
category
icon
password
本章已整理
概念
也称谓词逻辑
个体词
- 个体常项：具体
- 个体变项：抽象
- 个体域： 个体变项的取值范围
谓词
- 谓词常项： 具体性质or关系
- 谓词变项： 抽象性质or关系
- 一元谓词： 个体性质
- 多元谓词： 多元性质
量词
- 全称量词 (A(ll)倒置) 通常
- 存在量词 (E(xist)倒置) 通常
- 1元谓词与多元谓词的区分
- 无特别要求，用全总个体域
- 量词顺序一般不要随便颠倒
否定式的使用
例：没有不吃饭的人：
字母表
项
个体常项、变项是项，由它们构成的n元函数和复合函数还是项
原子公式
由项组成的n元谓词
例如，等均为原子公式
合式公式
具体定义
原子公式的“线性组合”
个体变项的自由出现与约束出现
指导变元，辖域
在公式和中，称为指导变元，为辖域
出现
的所有出现都称为约束出现，中不是约束出现的其他变项均称为是自由出现的。
闭式
不含自由出现的个体变项的公式
例
这是一个闭式，因为变项 x 被全称量化符 ∀ 绑定。
例子
在公式中
为的辖域，为指导变元, 中的两次出现均为约束出现，与均为自由出现.
换名规则
将量词辖域中出现的某个约束出现的个体变项及对应的指导变项，改成公式中未曾出现过的个体变项符号，公式中其余部分不变．
代替规则
对某自由出现的个体变项用与原公式中所有个体变项符号不同的变项符号去代替，且处处代替。
规则 | 作用对象 | 操作 | 目标 |
换名规则 | 绑定变量 | 更换变量名，保持语义不变 | 避免变量冲突或混淆 |
代替规则 | 自由变量 | 用项替换自由变量 | 应用公式或实例化逻辑陈述 |
关于量词的公式
量词否定等值式
量词辖域收缩与扩张等值式
蕴含前的量词要变号
“指向别人需要代价”
可以将不属于量词辖域范围的部分去掉，即“提纯”
量词分配等值式
对无分配律，对无分配律
举例
（1）任意对析取无分配律举例：对任意的x, x是奇数或x是偶数。
（2）存在对合取无分配律举例: 存在x，x是奇数且x是偶数
- 能换的换，看着清晰
- 存在和任意的顺序不变
- 非和其他运算符能不变就不变
同一层级，xy先后无影响
前束范式
将量词提到最前面，后面的公式不含量词。
如
- 前束范式一定存在但不唯一
求法：换名规则，代替规则，等值演算。
尤其注意改变辖域时蕴含前面的符号要变。
