Axiomatic WikiWWikiTTheoremsSatisfaction does not depend on variables not free in the formula
Theorem·T44
Reassigning a variable that is not free in a formula cannot change whether the formula is satisfied.
For an L-structure
,
,
, and
with
: for every assignment
into
:
In words
For any formula that does not have a given variable free in it: whether it is satisfied is unchanged by reassigning that variable to anything, no matter the assignment it is checked under.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1Setup, 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
- 3eq, rel. If is for terms : (eq clause, D093), so and . By T43 applied to each: , likewise for . By the eq clause of D091 on both sides: iff iff iff . The rel case is identical: if is for a relation symbol and a matching-arity tuple of terms , apply T43 pointwise to each entry of , as in the proof of T42.
- 4neg, bin. If is : (neg clause, D093), so ; by the IH, , and the neg clause of D091 transports this to . Likewise if is , , , or (any of the four binary connectives): (bin clause), so is free in neither nor ; the IH applies to both, and the matching clause of D091 transports the equivalence to , whichever connective it is.
- 5quant, same variable. If is or (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 (matching whichever quantifier uses): iff (for all/some) , iff (for all/some) , iff - the identical condition, with no dependence on at all.
- 6quant, different variable. If is or 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 (matching whichever quantifier uses): iff (for all/some) , iff (for all/some) , iff .
- 7T08 concludes: the claim holds for every with not free in it, for every assignment.
∎
Remarks
Confirms satisfaction genuinely only depends on an assignment through its values at the (finitely many) free variables of a formula - the intuition behind isolating sentences in the first place. Needed for the quantifier-same-variable case of the substitution lemma, and again directly inside soundness when checking the second quantifier axiom is valid. The proof below writes each of the five formation cases using the clean notation of D109 (negation, the four binary connectives, and the two quantifiers) rather than the raw underlying construction; only unique readability, invoked to split into these five cases, needs that raw construction itself, to distinguish a formula's leading symbol.