后件概括和前件存在规则

谓词逻辑中两条推演规则。如果个体变元x在公式A中不出现，而在B中出现，则从推出A→B(

x

)可推出A→

x

B(

x

)，这就是后件概括规则。例如，对P∨?P中的P代以F

x

可推出A→

x

B(

x

)，这就是后件概括规则。例如，对P∨?P中的P代以F(x)，可得P∨?P→F(λ)∨?F(x)，从这个蕴涵式出发，根据后件概括规则，可推出P∨?P→∨

x

(F(

x

)∨?F(

x

))。如果个体变元x在A中出现，而在B中不出现，则从推出A(x)→B可推出

x

A(x)→B，这就是前件存在规则。

例如，从推出F(y)→?∨

x

?属(y)，可推出

y

F(

y

)→?∨

x

?F(x)。这两条规则的作用在于对没有量词的公式引进量词。使用这两条规则时，必须注意它们所要求的条件，即在使用后件慨括规则时.该个体变元不得在前件出现;在使用前件存在规则时，该个体变元不得在后件出现。否则，就可能从普遍有效式出发推出非普遍有效式。