1.8谓词演算的推理规则

《1.8谓词演算的推理规则》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、离散数学DiscreteMathematics数理逻辑张晓西北工业大学计算机学院zhangxiao@nwpu.edu.cn2011-1-101.8.1“A(x)对y是自由的”可以这样吧考察以下谓词公式:x替换为y吗？∀yP(y)∨Q(x)∨R(x)∀yP(y)∨Q(y)∨R(x)∃yP(x,y)∨Q(x,y)∃yP(y,y)∨Q(y,y)∀yP(y)∨Q(x,y)∀yP(y)∨Q(y,y)2011-1-10离散数学2术语“A(x)对y是自由的”:如果公式A(x)中,x不出现在量词∀y或∃y的辖域之内,则称A(x)对y是自由的。上面的例子中，第二个式子

2、中的x是对y不自由的。不自由变量，不能进行代入。想替换x为y时，可以替换与y没有关系（自由）的x，否则不能替换2011-1-10离散数学3(2)式如果有必要代入y,则应先将式中的约束变元y改名,例如,把(2)式改名为:∃zP(x,z)∨Q(x,y)然后代入得∃zP(y,z)∨Q(y,y)2011-1-10离散数学41.8.2谓词演算中的推理规则-命题演算中所有推理规则都是谓词演算中的推理规则;-谓词演算中的所有永真蕴含式,恒等式和代入规则也都可作为推理规则。2011-1-10离散数学5(1)全称指定规则(全称特定化规则/全称量词消去规则)(Unive

3、rsalSpecification)简记为US∀xA(x)∴A(y)应用US规则的条件是:A(x)对于y必须是自由的。设则A(x)=∃y(x>y)∀xA(x)=∀x∃y(x>y),x,y的个体域为R，是一真命题.若应用US得∃y(y>y)，则是错误的。正确的做法是换成∃y(z>y)(z∈R)这一规则也可写为:∀xA(x)推得A(x)或∀xA(x)⇒A(x).它的意义是,全称量词可以删除。2011-1-10离散数学7(2)存在指定规则(存在特定规则/存在量词消去规则)(ExistentialSpecification)简记为ES。∃xA(x)∴A(y)

4、含义:如果已证明∃xA(x),那么我们可以假设某一确定的个体y使A(y)是真,这里y只是一个表面的自由变元。应用ES规则的条件应用ES规则的条件:(1)y(说c更好些)是使A为真的特定的个体常项。(2)y不在A(x)中出现。（3）y不是前提和居先推导步骤中的（表面）自由变元(3)若A(x)中还有其它自由出现的个体变项，此规则不能使用。2011-1-10离散数学9(3)存在推广规则（存在一般化规则/存在量词引入规则）(ExistentialGeneralization)简记为EG。A(y)∴∃xA(x)应用这一规则的条件是:A(y)对x是自由的（x最好

5、在A(y)中没有出现过）。这一规则可写成:A(y)⇒∃xA(x)(4)全称推广规则（全称一般化规则/全称量词引入规则）(UniversalGeneralization)简记为UG。A(y)∴∀xA(x)（1）无论A(y)中自由出现的个体变项y取何值，A(y)应该均为真。(1)y在A(y)中自由出现，且y取任何值时A均为真。（2）y不能是居先推导步骤中使用ES引入的。（3(2)x）取代自由出现的不在A(y)中约束出现y的x也不能在A(y)中约束出现。观察下述推理过程:(1)∀x∃yP(x,y)P,前提(2)∃yP(c,y)T,(1),US(3)P(c,

6、d)T,(2),ES(4)∀xP(x,d)T,(3),UG(5)∃y∀xP(x,y)T,(4),EG第(4)步是错误的：-P(c,d)无论c取何值，P(c,d)都为真？不是均为真!-P(c,d)中的d是使用ES引入的新变元，且自由出现!2011-1-10离散数学12∀x∃yP(x,y)⇒∃y∀xP(x,y)而这一式前面已指明它是不成立的。特别要注意,使用ES而产生的自由变元不能保留在结论中,因它是暂时的假设,在推导结束之前必须使用EG使之成为约束变元。2011-1-10离散数学13推理规则的正确使用(1)例设实数集中，语句“不存在最大的实数”可符号化

7、为：(∀x)(∃y)G(x,y)。其中：G(x,y)：y>x。推导1：（1）(∀x)(∃y)G(x,y)P（2）(∃y)G(y,y)US,(1)分析注意：：推导使用1是错误的。正确的推导如下：US规则来消去量词时，若选用变元（y取代1）(x∀，则要求x)(∃y)G(x,y)在原公式中x不能出现P在量词（2(）∀y)(∃或y)G(z,y)(∃y)的辖域之内。US,(1)2011-1-10离散数学14推理规则的正确使用（2）推导2：（1）(∀x)(∃y)G(x,y)P（2）(∃y)G(z,y)US,(1)（3）G(z,c)ES,(2)分析：推导2是错误的

8、。正确的推导如下：注意：使用ES规则来消去量词时，若还（1）(∀x)(∃y)G(x,y)P有其它自由变元时，