Database: Variable occurrence in generalized universal statements

Proposition 20: Let x be a variable, and \phi a statement.
(a) If x is among the variables a, b, ..., z , then x occurs in the generalized universal statement \forall a, b, ..., z \phi .
(b) If x occurs in \phi then it occurs in \forall ab, b, ..., z \phi .

Proof: (a): We will argue by structural induction over the recursive definition of generalized universal statements.

Base cases:
If x is among the variables a and b , then x is identical to at least one of these variables. If x is identical to a , then x occurs in \forall a \forall b \phi by (a) in [19]. If x is identical to b then x occurs in \forall b \phi by the same result, and hence in \forall a \forall b \phi by either (a) or (b) in [19]. But \forall a, b \phi is short for \forall a \forall b \phi .

Inductive step: We take as the induction hypothesis that the desired result is evident for variables b, c, ..., z , and want to show from this that it is evident for a, b, c, ..., z . If x is among a, b, ..., y, z , then either x is identical to a or it is among b, c, ..., z . In the former case, x occurs in \forall a \forall b, c, ..., z \phi by (a) in [19]. In the latter case, x occurs in \forall b, c, ..., z \phi by the induction hypothesis, and hence in \forall a \forall b, c, ..., z \phi by (b) in [19]. But \forall a, b, c, ..., z \phi is short for precisely the statement \forall a \forall b, c, ..., z \phi . \square

This database entry builds on the following:

  1. Terminology: Class, membership
  2. Terminology: Statement
  3. Definition: Occurrence of a variable
  4. Definition: Universal quantification
  5. Proposition: Variable occurrence in universal statements
  6. Terminology: Recursion, structural induction