后件概括和前件存在规则

谓词逻辑中两条推演规则。如果个体变元x在公式A中不出现，而在B中出现，则从推出A→B(_x)可推出A→∀_xB(_x)，这就是后件概括规则。例如，对P∨乛P中的P代以F_x可推出A→∀_xB(_x)，这就是后件概括规则。例如，对P∨乛P中的P代以F(x)，可得P∨乛P→F(λ)∨乛F(x)，从这个蕴涵式出发，根据后件概括规则，可推出P∨乛P→∨_x(F(_x)∨乛F(_x))。如果个体变元x在A中出现，而在B中不出现，则从推出A(x)→B可推出∃_xA(x)→B，这就是前件存在规则。
例如，从推出F(y)→乛∨_x乛属(y)，可推出∃_yF(_y)→乛∨_x乛F(x)。这两条规则的作用在于对没有量词的公式引进量词。使用这两条规则时，必须注意它们所要求的条件，即在使用后件慨括规则时.该个体变元不得在前件出现；在使用前件存在规则时，该个体变元不得在后件出现。否则，就可能从普遍有效式出发推出非普遍有效式。