Generalization (logic)

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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

[edit] Generalization with hypotheses

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

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

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

This purports to show that \exists z \exists w ( z \not = w) \vdash \forall x (x \not = x), which is an unsound deduction.

[edit] 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(y) \rightarrow Q(y)))  Axiom PRED-1
4  P(y) \rightarrow Q(y) From (1) and (3) by Modus Ponens
5  (\forall x \, P(x)) \rightarrow P(y) Axiom PRED-1
6  P(y) \ From (2) and (5) by Modus Ponens
7  Q(y) \ 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, the deduction theorem was applicable in steps 10 and 11 because the formulas being moved have no free variables.

[edit] See also

Personal tools
Namespaces
Variants
Actions
Navigation
Interaction
Toolbox
Print/export
Languages