Theorem·T42
The substitution lemma for terms
Evaluating a substituted term matches evaluating the original term after moving the replacement's own value into the assignment.
For an L-structure
, assignment
,
,
, and
:
In words
For any term: substituting into it, then evaluating, gives the same result as evaluating it directly under an assignment updated to send the substituted variable to the replacement term's own value.
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 . Write .
- 2By T32 (ii), is either for a unique , or for a unique .
- 3Variable case, . (match clause, D097), so the left side is . The right side is (var clause, D089), and by the defining property of the updated assignment . The two sides agree.
- 4Variable case, . (other clause, D097), so the left side is . The right side is , and since agrees with everywhere except at , and . The two sides agree.
- 5Function case. (func clause, D097), so by the func clause of D089: . By the IH applied to each ( , each of length by the same bookkeeping as in the proof of T31): for every , i.e. as functions (Extensionality). By associativity of : . So the left side is , which is exactly (func clause of D089) - the right side.
- 6T08 concludes: the claim holds for every .
∎
Remarks
The technical heart of why universal instantiation and substitutivity of equals are sound: this lemma is what lets soundness relate a substituted formula's truth to the original formula's truth under a shifted assignment. Its formula-level counterpart, needed for the same purpose whenever the substituted variable occurs inside a quantifier-free part of a formula, is T46.