Proposition 29: 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 universal statement \forall a, b, ..., z \phi .
(b) If \mathtt{v} occurs in \phi then it occurs in \forall a, b, ..., z \phi .
Proof: (a): We argue by structural induction over the definition of iterated universal 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 \forall a \forall b \phi by (a) in [15]. If \mathtt{v} is identical to b then \mathtt{v} occurs in \forall b \phi by the same result, and hence in \forall a \forall b \phi by either (a) or (b) in [15]. 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 \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 \forall a \forall b, c, ..., z \phi by (a) in [15]. In the latter case, \mathtt{v} occurs in \forall b, c, ..., z \phi by the induction hypothesis, and hence in \forall a \forall b, c, ..., z \phi by (b) in [15]. But \forall a, b, c, ..., z \phi is short for precisely the statement \forall a \forall 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 \forall b \phi by (b) in [15]. By the same rule again, it also exists in \forall a \forall b \phi , for which \forall 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 \forall b, c, ..., z \phi . Then, if \mathtt{v} occurs in \phi , it follows from this induction hypothesis and (b) in [15] that \mathtt{v} occurs in \forall a \forall b, c, ..., z \phi , which is the definition of \forall a, b, c, ..., z . \square