基本概念

1. 个体词
   1. 表示研究对象的词
   2. 可分为：个体常元、个体变元
   3. 使用字母表靠前的小写字母表示个体变元，靠前的表示个体常元
2. 谓词
   1. 表示研究对象的性质或者研究对象之间关系的词
   2. 用大写字母表示
   3. $n$元谓词：含有$n$个个体变元的谓词
3. 论域（个体域）
   1. 个体变元的取值范围
4. 函词：藐视一个个体域到另一个个体域的映射
5. 量词
   1. 限制个体词的数量
   2. 分为存在量词$\exist$和全称量词$\forall$
6. 项：个体变元、个体常元、$n$元函词以及以上三者的有限次复合
7. 约束变元：受量词约束的个体变元
8. 自由变元：不受量词约束的个体变元
9. 辖域：量词的约束范围
10. 易名规则：将量词辖域中出现的某个约束变元改成另一个在该辖域中从未出现的个体变元，公式的其他部分保持不变；改名后的公式称为改名式
11. 可代入：设$v$是谓词公式$A$中的自由变元，且项$t$中不含$A$的约束变元符（如果有可易名），则称$t$对$v$是可代入的
12. 代入：对公式$A$中的自由变元的所有自由变元的所有自由出现都换为$t$（必须是可代入的）记为$A^v_t$（$A^原_现$）；如果$A$中没有$v$则为$A_t^v=A$

自然语言形式化

1. 谓词：$X是xxxx。$
2. 函词：$X的xxxx。$

一阶谓词形式系统

1. 闭公式+解释=命题
2. 含有自由变元的公式+解释=命题函数