| 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 5
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 𝑥 = 𝑥,
then we can conclude ∀𝑥𝑥 = 𝑥 or even ∀𝑦𝑥 = 𝑥. Theorem
altru 1839 shows the special case ∀𝑥⊤. The converse rule of
inference spi 2220 (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 (𝜑 → ∀𝑥𝜑) need not hold
(but may hold in special cases, see ax-5 1942). (Contributed by NM,
3-Jan-1993.) |
