Generalization is an inference rule of Predicate Calculus which states that:

If is true (valid) then so is .

"Generalization" can be abbreviated as GEN, and the inference rule can be summarized as the sequent

,

but this gives rise to an important restriction: the Deduction Theorem cannot be applied to it to derive

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):

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

is clearly not true, because from it and

,

"7 is a prime number", can be deduced

,

"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 GEN 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 turnstyle.

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

So the formula is just a more explicit way of stating what was already implicitly meant by .

There is also an axiom of Pred.Calc. which states that

which transforms by the converse of the Deduction Theorem into

,

meaning that from can be deduced . Putting GEN and the axiom together, one deduces that

which does not mean the same as

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 turnstyle symbol 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 really does mean more than , because the 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: .

Proof:

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