804
Derivation Rules for Propositional and Predicate Logic
infEREncE RulEs (continued)
from
can Derive
name/abbreviation for Rule Restrictions on use
(4x)P(x)
P(t), where t
is a variable
or constant
symbol
Universal instantiation—ui
If t is a variable, it
must not fall within
the scope of a
quantifier for t.
( E x)P(x)
P(a) where a
is a constant
symbol not
previously
used in proof
sequence
Existential instantiation—ei
Must be the first rule
used that introduces
a.
P(x)
(4x)P(x)
Universal generalization—ug
P(x) has not been
deduced from any
hypotheses in which
x is a free variable
nor has P(x) been
deduced by ei from
any wff in which x is
a free variable.
P(x) or P(a)
where a is
a constant
symbol
( E x)P(x)
Existential generalization—eg To go from P(a) to
( E x)P(x), x must not
appear in P(a).