Description: Rule of (universal) generalization. In our axiomatization, this is the
only postulated (that is, axiomatic) rule of inference of predicate
calculus (together with the rule of modus ponens ax-mp of
propositional calculus). See, e.g., Rule 2 of Hamilton p. 74. This
rule says that if something is unconditionally true, then it is true for
all values of a variable. For example, if we have proved x = x ,
then we can conclude A. x x = x or even A. y x = x . Theorem
altru shows the special case A. x T. . The converse rule of
inference spi (universal instantiation, or universal specialization)
shows that we can also go the other way: in other words, we can add or
remove universal quantifiers from the beginning of any theorem as
required. Note that the closed form ( ph -> A. x ph ) need not hold
(but may hold in special cases, see ax-5 ). (Contributed by NM, 3-Jan-1993)