In predicate logic, generalization (also universal generalization, universal introduction, GEN, UG) is a valid inference rule. It states that if <math>\vdash \!P(x)</math> has been derived, then <math>\vdash \!\forall x \, P(x)</math> can be derived.

Generalization with hypotheses

The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume <math>\Gamma</math> is a set of formulas, <math>\varphi</math> a formula, and <math>\Gamma \vdash \varphi(y)</math> has been derived. The generalization rule states that <math>\Gamma \vdash \forall x \, \varphi(x)</math> can be derived if <math>y</math> is not mentioned in <math>\Gamma</math> and <math>x</math> does not occur in <math>\varphi</math>.

These restrictions are necessary for soundness. Without the first restriction, one could conclude <math>\forall x P(x)</math> from the hypothesis <math>P(y)</math>. Without the second restriction, one could make the following deduction:

  1. <math>\exists z \, \exists w \, ( z \not = w) </math> (Hypothesis)
  2. <math>\exists w \, (y \not = w) </math> (Existential instantiation)
  3. <math>y \not = x</math> (Existential instantiation)
  4. <math>\forall x \, (x \not = x)</math> (Faulty universal generalization)

This purports to show that <math>\exists z \, \exists w \, ( z \not = w) \vdash \forall x \, (x \not = x),</math> which is an unsound deduction. Note that <math>\Gamma \vdash \forall y \, \varphi(y)</math> is permissible if <math>y</math> is not mentioned in <math>\Gamma</math> (the second restriction need not apply, as the semantic structure of <math>\varphi(y)</math> is not being changed by the substitution of any variables).

Example of a proof

Prove: <math> \forall x \, (P(x) \rightarrow Q(x)) \rightarrow (\forall x \, P(x) \rightarrow \forall x \, Q(x)) </math> is derivable from <math> \forall x \, (P(x) \rightarrow Q(x)) </math> and <math> \forall x \, P(x) </math>.

Proof:

{| class="wikitable"

! Step

! Formula

! Justification

|-

| 1

| <math> \forall x \, (P(x) \rightarrow Q(x)) </math>

| Hypothesis

|-

| 2

| <math> \forall x \, P(x) </math>

| Hypothesis

|-

| 3

| <math> (\forall x \, (P(x) \rightarrow Q(x))) \rightarrow (P(y) \rightarrow Q(y)) </math>

| From (1) by Universal instantiation

|-

| 4

| <math> P(y) \rightarrow Q(y) </math>

| From (1) and (3) by Modus ponens

|-

| 5

| <math> (\forall x \, P(x)) \rightarrow P(y) </math>

| From (2) by Universal instantiation

|-

| 6

| <math> P(y) \ </math>

| From (2) and (5) by Modus ponens

|-

| 7

| <math> Q(y) \ </math>

| From (6) and (4) by Modus ponens

|-

| 8

| <math> \forall x \, Q(x) </math>

| From (7) by Generalization

|-

| 9

| <math> \forall x \, (P(x) \rightarrow Q(x)), \forall x \, P(x) \vdash \forall x \, Q(x) </math>

| Summary of (1) through (8)

|-

| 10

| <math> \forall x \, (P(x) \rightarrow Q(x)) \vdash \forall x \, P(x) \rightarrow \forall x \, Q(x) </math>

| From (9) by Deduction theorem

|-

| 11

| <math> \vdash \forall x \, (P(x) \rightarrow Q(x)) \rightarrow (\forall x \, P(x) \rightarrow \forall x \, Q(x)) </math>

| From (10) by Deduction theorem

|}

In this proof, universal generalization was used in step 8. The deduction theorem was applicable in steps 10 and 11 because the formulas being moved have no free variables.

See also

  • First-order logic
  • Hasty generalization
  • Universal instantiation
  • Existential generalization

References