Skip to content
Axiomatic Wiki

WTA term's value does not depend on variables not occurring in it

Theorem·T43

Reassigning a variable that never appears in a term cannot change the term's value.

For an L-structure , assignment , , , and with :
In words
For a structure, an assignment, a variable, and an element of the domain to reassign it to, and for any term of the language: provided the given variable does not occur in the term, the term's value is unchanged whether it is computed under the original assignment or under the assignment with that variable reassigned to the given element.
Rests onF02F03F04F06F08F09F11F12F14A01A02A06A07A08
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    By strong induction on : assume the claim for every term of length (the induction hypothesis, "IH"); show it for of length .
  2. 2
    By T32 (ii), is either the variable for a unique , or for a unique and , using the notation of D109.
  3. 3
    Variable case. (var clause, D092), so means . Then and , since agrees with everywhere except at , and (D087). Equal.
  4. 4
    Function case. (func clause, D092), so means for every (else would lie in the union). By the IH applied to each (length , by the same bookkeeping as in the proof of T31): for every , i.e. as functions (Extensionality). By the func clause of D089 applied on both sides: .
  5. 5
    T08 concludes: the claim holds for every .
∎

Remarks

The term-level half of the fact that satisfaction only ever depends on an assignment through its values at the finitely many variables actually occurring free; the formula-level half is T44, needed for the quantifier case of the substitution lemma when the substituted variable is the one just quantified.
Wikipedia ↗FirstOrder.Language.Term.realize_relabel ↗

Used by

T44T46
Propose an edit1 published revision