Database: Variable occurrence in iterated existence statements

Proposition 28: Let \mathtt{v} be a variable, and \phi a statement.
(a) If \mathtt{v} is among the variables a, b, ..., z , then \mathtt{v} occurs in the iterated existence statement \exists a, b, ..., z \phi .
(b) If \mathtt{v} occurs in \phi then it occurs in \exists a, b, ..., z \phi .

Proof: (a): We argue by structural induction over the definition of iterated existence statements.

Base cases:
If \mathtt{v} is among the variables a and b , then \mathtt{v} is identical to at least one of these variables. If \mathtt{v} is identical to a , then \mathtt{v} occurs in \exists a \exists b \phi by (c) in the definition of occurrence. If \mathtt{v} is identical to b then \mathtt{v} occurs in \exists b \phi by (c) again, and hence in \exists a \exists b \phi by either (c) or (f) in the definition of occurrence. But \exists a, b \phi is precisely an abbreviation for \exists a \exists 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 \mathtt{v} is among a, b, ..., y, z , then either \mathtt{v} is identical to a or it is among b, c, ..., z . In the former case, \mathtt{v} occurs in \exists a \exists b, c, ..., z \phi by (c) in the definition of occurrence. In the latter case, \mathtt{v} occurs in \exists b, c, ..., z \phi by the induction hypothesis, and hence in \exists a \exists b, c, ..., z \phi by (f) in the definition of occurrence. But \exists a, b, c, ..., z \phi is short for \exists a \exists b, c, ..., z \phi .

(b): We again use structural induction, over the same definition as above.

Base cases: If \mathtt{v} occurs in \phi , then it occurs in \exists b \phi by (f) in the definition of occurrence. By the same rule again, it also exists in \exists a \exists b \phi , for which \exists a, b \phi is shorthand.

Inductive step: Suppose we know that for variables b, c, ..., z that if \mathtt{v} occurs in \phi then it occurs in \exists b, c, ..., z \phi . If \mathtt{v} occurs in \phi , it then follows from this induction hypothesis and (f) in the definition of occurrence that \mathtt{v} occurs in \exists a \exists b, c, ..., z \phi , for which \exists a, b, c, ..., z is short. \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Existential quantification
  3. Definition: Occurrence of a variable
  4. Terminology: Structural induction