离散数学 一阶逻辑等值演算

A(x,y)?x?yA(x,y) ??y?xA(x,y)二、等值演算规则1、置换规则(等值代换)设Φ(A)是含公式A的公式,若A ? B,则Φ(A) ?Φ(B).一阶逻辑中的置换规则与命题逻辑中的置换规则形式上完全相同,只是在这里A,B是一阶逻辑公式.对于公式中出现有双重身份的变元(即自由又约束)的处理:2、换名规则(约束变元的换名)-目的是使每个变元性质唯一设A为一公式,将A中某量词辖域中某约束变项的所有出现及相应的指导变元,改成该量词辖域中未曾出现过的某个体变项符号,公式中其余部分不变,设所得公式为A’,则A’? A 例:?xA(x) ∨ B(x) 由于公式中的x 即是自由的又是约束的,可利用此规则进行换名为:?t A(t) ∨ B(x) ??xA(x) ∨ B(x) 后可利用量词的扩充得到:?t A(t) ∨ B(x) ??t( A(t)∨ B(x) )例:?xF(x,y,z)→?yG(x,y,z) 其中x,y即是约束又自由??t F(t,y,z) →?yG(x,y,z) (换名规则) 约束的x换名??t F(t,y,z) →?wG(x,w,z) (换名规则)约束的y换名3) 代替规则(自由变元的代替)设A为一公式,将A中某个自由出现的个体变项的所有出现用A中未曾出现过的个体变项符号代替,A中其余部分不变,设所得公式为A’,则A’? A.注:该规则对后面的演算很重要,特别是对于公式中某个变元x,它即是约束的又是自由的情况,必须利用此规则将该变元换为仅具有一种性质才可进行演算。例:?xF(x,y,z)→?yG(x,y,z)??x F(x,t,z) →?yG(x,y,z) (代替规则) 自由的y用t代换??x F(x,t,z) →?yG(w,y,z) (代替规则) 自由的x用w代换