Generalization (logic)

Generalization is an inference rule of predicate calculus which states that::"If $vdash\; P(x)$ is true (valid) then so is $vdash\; forall\; x\; ,\; P(x)$."Generalization" can be abbreviated as GEN. The inference rule can be summarized as the sequent: $P(x)\; vdash\; forall\; x\; ,\; P(x)$,but this gives rise to an important restriction: the Deduction Theorem cannot be applied to it to derive:

$vdash\; P(x)\; ightarrow\; forall\; x\; ,\; P(x)$

This formula is wrong because "x" has an unbound instance in its antecedent and a bound occurrence in its consequent, so that if the formula were instead correct, then its free instance of "x" could be replaced by any constant (element of the domain):: $vdash\; P(t)\; ightarrow\; forall\; x\; ,\; P(x)$but this is incorrect. E.g. if P(x) means "x" is a prime number" and the domain is the set of natural numbers, then:$vdash\; P(7)\; ightarrow\; forall\; x\; ,\; P(x)$is clearly not true, because from it and:$vdash\; P(7)$,"7 is a prime number", can be deduced:$vdash\; forall\; x\; ,\; P(x)$,"all natural numbers are prime numbers", a contradiction, by means of modus ponens, so the wrong formula is reduced to the absurd.

This restriction applies to proofs: if generalization is applied to a formula in a proof, thereby binding its free variable "x", then DT cannot be applied to the proof to move this formula to the right side of the turnstile.

Note that "P(x)" symbolizes an open statement with free variable "x", whose truth is contingent on "x", but $vdash\; P(x)$ symbolizes a statement which is valid (for all values of "x"), even though its variable "x" is free. Generalization applies to such valid statement, binding its free variable and yielding $vdash\; forall\; x\; ,\; P(x)$.

So the formula $vdash\; forall\; x\; ,\; P(x)$ is just a more explicit way of stating what was already implicitly meant by $vdash\; P(x)$.

There is also an axiom of Pred.Calc. which states that:$vdash\; forall\; x\; ,\; P(x)\; ightarrow\; P(x)$which transforms by the converse of the Deduction Theorem into:$forall\; x\; ,\; P(x)\; vdash\; P(x)$,meaning that from $vdash\; forall\; x\; ,\; P(x)$ can be deduced $vdash\; P(x)$. Putting generalization and the axiom together, one deduces that:$vdash\; P(x)\; Leftrightarrow\; vdash\; forall\; x\; ,\; P(x)$which does not mean the same as:

$P(x)\; Leftrightarrow\; forall\; x\; ,\; P(x)$

which is wrong because here "P(x)" could be any contingent, invalid, open formula. In order to prevent such wrong formula from being at all provable, the restriction is added to DT in Pred.Calc.

The turnstile symbol $vdash$ is not a part of a well-formed formula: strictly speaking it belongs neither to Prop.Calc. or Pred.Calc., but might be thought of as a "metasymbol". Therefore, ultimately $vdash\; forall\; x\; ,\; P(x)$ really does mean more than $vdash\; P(x)$, because the $vdash$ symbol is not really a part of the formula "P(x)"; it is just a "handle" used to "grab" the formula, figuratively speaking.

Example of a proof

Prove: $forall\; x\; ,\; (P(x)\; ightarrow\; Q(x))\; ightarrow\; (forall\; x\; ,\; P(x)\; ightarrow\; forall\; x\; ,\; Q(x))$.

Proof:

In this proof, DT was applicable in step (10) because the formula $forall\; x\; ,\; P(x)$ which was to be moved to the right of the turnstile (by DT) did not contain any free variable. DT was also applicable in step (11) for the same reason.

ee also

*First-order logic
*Universal instantiation