Satisfaction does not depend on variables not free in the formula

Proof

1. 1
   Setup, generalizing over assignments. By strong induction on : assume, for every formula of length with not free in it, the claim holds for every assignment (the induction hypothesis, "IH"); show it for of length with , for an arbitrary assignment .
2. 2
   By T35 (ii), is exactly one of the five forms of D083.
3. 3
   eq, rel. If : (eq clause, D093), so and . By T43 applied to each: , likewise . By the eq clause of D091 on both sides: iff iff iff . The rel case is identical, using T43 pointwise on the argument tuple, as in the proof of T42.
4. 4
   neg, bin. If : (neg clause, D093), so ; by the IH, , and the neg clause of D091 transports this to . Likewise if ( ): (bin clause), so is free in neither nor ; the IH applies to both, and the matching clause of D091 transports the equivalence to .
5. 5
   quant, same variable. If ( , bound variable exactly ): for any , updating twice at the same variable leaves only the second update - , since both remove the same pair at from and add back (D087, Extensionality). So by the forall/exists clause of D091 (according to ): iff (for all/some) , iff (for all/some) , iff - the identical condition, with no dependence on at all.
6. 6
   quant, different variable. If with : (quant clause, D093), so and together give . For any , updates at different coordinates commute: , since each just adds the independent pairs , to with the old entries at removed, in either order (Extensionality). By the IH applied to (with ) at the assignment : iff iff . So by the forall/exists clause of D091: iff (for all/some) , iff (for all/some) , iff .
7. 7
   T08 concludes: the claim holds for every with not free in it, for every assignment.

Used by