Database: Universal elimination

Theorem 95: Universal elimination/instantiation (inference rule)

Suppose x is a variable and y is a variable such that x is freely substitutable for y in the statement \phi . Given that the universal statement \forall x \phi holds, we may infer that the variable substitution [\phi | x \to y] holds: \cfrac{\vdash \forall x \phi}{\vdash [\phi | x \to y]}.

Proof: Assume the negation \neg [\phi | x \to y] . Observe that this is the same as the statement [ \neg \phi | x \to y] . By existential introduction, we may then infer that the existence statement \exists x \neg \phi holds. Thus \neg [\phi | x \to y] entails \exists x \neg \phi .

However, we had as a premise that \forall x \phi holds, and this is short for \neg \exists x \neg \phi . We thus get using weakening that \neg [\phi | x \to y] entails \neg \exists x \neg \phi . We infer by negation introduction that the double negation \neg \neg [\phi | x \to y] holds; using double negation elimination, we conclude [\phi | x \to y] holds. \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Negation
  3. Definition: Existential quantification
  4. Definition: Universal quantification
  5. Proposition/definition: Variable substitution
  6. Definition: Freely substitutable variable
  7. Terminology: Inference, entailment
  8. Terminology: Inference rule
  9. Theorem: The weakening rule
  10. Inference rule: Negation introduction
  11. Inference rule: Double negation elimination
  12. Inference rule: Existential introduction