Proposition 44: Let a, b, ..., z as well as \mathtt{u} and \mathtt{v} be variables, and \phi a statement. Recall the usual notation for iterated universal statements.
(a) If \mathtt{u} is among a, b, ..., z , the variable substitution [\forall a, b, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \forall a, b, ..., z \phi .
(b) If \mathtt{u} is not among a, b, ..., z , then [\forall a, b, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \forall a, b, ..., z [\phi | \mathtt{u} \to \mathtt{v}].
Proof: (a): We will use structural induction over the definition of iterated universal statements.
Base cases: Suppose \mathtt{u} is among the variables a and b . By definition, we know that \forall a, b is shorthand for \forall a \forall b \phi . There are at most two possibilities: \mathtt{v} is identical to a , or \mathtt{v} is identical to b (these coincide if a is identical to b ). Supposing the former, (a) in [43] tells us [\forall a \forall b | \mathtt{u} \to \mathtt{v}] is defined as \forall a \forall b \phi , i.e. as \forall a, b \phi . Thus, we are done in this case.
Suppose now that \mathtt{v} is identical to b but distinct from a . Then, by (b) in [43], [\forall a \forall b \phi | \mathtt{u} \to \mathtt{v}] is given by \forall a [ \forall b \phi | \mathtt{u} \to \mathtt{v}]. But [ \forall b \phi | \mathtt{u} \to \mathtt{v}] is now given by \forall b \phi , using (e) in the definition of variable substitution. Therefore, [\forall a \forall b \phi | \mathtt{u} \to \mathtt{v}] is again given by \forall a \forall b \phi , i.e. \forall a, b \phi .
Inductive step: We take as the induction hypothesis that for the variables b, c, ..., z , we know that [\forall b, c, ..., z | \mathtt{u} \to \mathtt{v}] is given by \forall b, c, ..., z \phi whenever \mathtt{u} is among b, c, ..., z . Suppose now that \mathtt{u} is among the variables a, b, c, ..., z . If \mathtt{u} is identical to a , then we get by (a) in [43] that [\forall a, b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \forall a, b, c, ..., z \phi , as \forall a, b, c, ..., z is shorthand for \forall a \forall b, c, ..., z \phi .
On the other hand, if \mathtt{u} is not identical to a , then it must instead be among the variables b, c, ..., z . By (b) in [43] we then know [\forall a, b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}] is \forall a [\forall b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}]. By the induction hypothesis, we know that this is the same as \forall a \forall b, c, ..., z \phi , which is the defnition of \forall a, b, c, ..., z \phi .
(b): We again use structural induction, over the same definition as above.
Base cases: Suppose \mathtt{u} is distinct from both a and b . Since \forall a, b \phi is short for \forall a \forall b \phi , (b) in [43] [\forall a, b \phi | \mathtt{u} \to \mathtt{v}] is \forall a [\forall b \phi | \mathtt{u} \to \mathtt{v}]. Using the same part of the definition again, this is the same as \forall a \forall b [\phi | \mathtt{u} \to \mathtt{v}]. Inductive step: We take as the induction hypothesis that for the variables b, c, ..., z , we have that [\forall b, c, ..., z | \mathtt{u} \to \mathtt{v}] is given by \forall b, c, ..., z [\phi | \mathtt{u} \to \mathtt{v}] whenever \mathtt{u} is not among b, c, ..., z . Suppose now that \mathtt{u} is not among the variables a, b, c, ..., z . As \forall a, b, c, ..., z \phi is short for \forall a \forall b, c, ..., z \phi , we get using (b) in [43] that [\forall a, b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}] is \forall a [\forall b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}], which by the induction hypothesis is the same as \forall a \forall b, c, ..., z [\phi | \mathtt{u} \to \mathtt{v}], i.e. the same as \forall a, b, c, ..., z [\phi | \mathtt{u} \to \mathtt{v}] . \square