Theorem·T43
A term's value does not depend on variables not occurring in it
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 any term with no occurrence of a given variable: its value is unchanged by reassigning that variable to anything.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1By strong induction on : assume the claim for every term of length (the induction hypothesis, "IH"); show it for of length .
- 2By T32 (ii), is either for a unique , or for a unique .
- 3
- 4Function 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: .
- 5T08 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.