Universal generalization

Universal generalization or universal introduction (∀I, sometimes GEN) is a basic rule of inference in first-order logic by which a universal statement is introduced to a proof. The universal generalization rule holds that if you can prove that something is true for any arbitrary constant, it must be true for all things. This allows you to move from a particular statement about an arbitrary object to a general statement using a quantified variable.

The universal introduction rule may be formally presented as follows:

If Γ φ(c), then Γ ∀xφ(x)

… where Γ is a set of formulae and c is an arbitrary constant that is new to the proof or argument being presented. That is, the constant c cannot be present in Γ.

(If the object c is already being discussed, then it is not arbitrary and we would then be wrongly moving to a general statement from a particular. The only reason that we can move from an arbitrary c to a statement about all objects is because we are proving that for anything, a certain statement (φ, in this case) logically applies (and can't not apply), which forces us to conclude that the statement applies to all objects.

Introducing a Universal

When constructing a proof of some formula, one may need to introduce a universal statement by means of universal generalization. To do this, we create a sub-proof in which we prove that some statement, φ, is true for any arbitrary constant. In this example, we introduce a constant a. The constant we introduce must be completely new to the proof.

At the beginning of the proof, we make a note that we are required to prove φ(a) in order to form the universal, and then, using other rules of inference, derive φ(a) from previous premises and deductions. Once we establish φ(a), we can proceed with our generalization and introduce a universal, stating that ∀xφ(x).