一阶谓词逻辑命题符号化例子

不是所有——非任意（存在非）

不存在——非存在（任意非）

说明

辖域、指导变元、约束出现

赋值

 ​​​​

代换实例

简而言之——就是将命题变项换为谓词公式

例子

 基本等值式

简而言之——命题逻辑的等值式，谓词逻辑也可以直接用（不改变量词） 

第三行要改变量词 

并且B中不能含有x

有限个体域消去量词

量词辖域的收缩与扩张

前束范式

简而言之——就是将所有的量词放在公式最前面（包括‘非’之前）

求前束范式的例子

用好换名规则

推理规则

化简律，附加律同命题逻辑

注意第一，二条，从左往右可以，从右往左不行（没有分配律）

量词消去规则

全称量词消去规则

存在量词消去规则

量词引入规则

全称量词引入规则

存在量词引入规则

例题

这个证明类似命题逻辑

看看第8步合取引入

由上易知：一般先从“存在量词”入手

看着简单，但实际做的效果就不得而知了

说明

消去规则需要前束范式

这个“3.”由上面公式易知：因为  任意x（F(x)->G(x)）不能直接分配律

归谬法

附加前提法