encyclopedia

Categories: Model theory | Logic

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, and 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) \rightarrow \forall x P(x) \qquad \qquad \hbox{(WARNING: This formula is wrong.)}$

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) \rightarrow \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) \rightarrow \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 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 $\vdash P(x)$ 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 $\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) \rightarrow 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 GEN and the axiom together, one deduces that

$\vdash P(x) \ \equiv \ \vdash \forall x P(x)$

which does not mean the same as

$P(x) \leftrightarrow \forall x P(x) \qquad \qquad \hbox{(WARNING: This formula is wrong)}$

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 $\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) \rightarrow Q(x)) \rightarrow (\forall x P(x) \rightarrow \forall x Q(x))$ .

Proof:

Number	Formula	Justification
1	$\forall x (P(x) \rightarrow Q(x))$	Hypothesis
2	$\forall x P(x)$	Hypothesis
3	$(\forall x (P(x) \rightarrow Q(x))) \rightarrow (P(x) \rightarrow Q(x)))$	Axiom PRED-1
4	$P(x) \rightarrow Q(x)$	From (1) and (3) by Modus Ponens
5	$(\forall x P(x)) \rightarrow P(x)$	Axiom PRED-1
6	$P(x) \$	From (2) and (6) by Modus Ponens
7	$Q(x) \$	From (6) and (4) by Modus Ponens
8	$\forall x Q(x)$	From (7) by Generalization
9	$\forall x (P(x) \rightarrow Q(x)), \forall x P(x) \vdash \forall x Q(x)$	Summary of (1) through (8)
10	$\forall x (P(x) \rightarrow Q(x)) \vdash \forall x P(x) \rightarrow \forall x Q(x)$	From (9) by Deduction Theorem
11	$\vdash \forall x (P(x) \rightarrow Q(x)) \rightarrow (\forall x P(x) \rightarrow \forall x Q(x))$	From (10) by Deduction Theorem

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 turnstyle (by DT) did not contain any free variable. DT was also applicable in step (11) for the same reason.

Categories: Model theory | Logic

The contents of this article are licensed from Wikipedia.org under the GNU Free Documentation License.
How to see transparent copy

01-04-2007 01:21:04

| | | |