Database: Universal introduction

Theorem 97: Universal introduction/generalization (inference rule)

Suppose x and y are variables such that y does not occur in the statement \phi nor in any assumption in the current context. Given the variable substitution [\phi | x \to y] holds, we may infer the universal statement \forall x \phi holds: \cfrac{\vdash [\phi | x \to y] }{\vdash \forall x \phi}.

Proof: First, using double negation introduction, we infer that the double negation \neg \neg [\phi | x \to y] holds. By negation elimination, we then infer that the negation \neg [|\phi | x \to y] entails the negated existence statement \neg \exists x \neg \phi .

Assume now \exists x \neg \phi . Noting that y does not occur in this assumption, we infer by existential elimination that \neg \exists x \neg \phi holds. In other words, \exists x \neg \phi entails its own negation. By [57], we thus conclude \neg \exists x \neg \phi holds. But \forall x \phi is short for precisely this statement. \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Negation
  3. Definition: Existential quantification
  4. Definition: Universal quantification
  5. Definition: Occurrence of a variable
  6. Proposition/definition: Variable substitution
  7. Terminology: Inference, entailment
  8. Terminology: Inference rule
  9. Proposition: Statements entailing their own negation
  10. Proposition: Double negation introduction
  11. Theorem: Negation elimination
  12. Inference rule: Existential elimination