Database: Variable occurrence in universal statements

Proposition 19: Let x and y be variables, and \phi a statement.
(a) x occurs in the universal statement \forall x \phi .
(b) If x occurs in \phi then it occurs in \forall y \phi .

Proof: (a): By (c) in the the definition, x occurs in \exists x \neg \phi , where \neg denotes negation. Next, by (e) in the definition, x occurs in the existence statement \neg \exists x \neg \phi . But \forall x \phi is short for just this statement.

(b): Using (e) and (f) in the definition, x occurs in \neg \phi and hence in \exists y \neg \phi , and therefore in \neg \exists y \neg \phi , for which \forall y \phi is short. \square

This database entry builds on the following:

  1. Terminology: Class, membership
  2. Terminology: Statement
  3. Definition: Negation
  4. Definition: Existential quantification
  5. Definition: Occurrence of a variable
  6. Definition: Universal quantification