Skip to content
Axiomatic Wiki

WTThe substitution lemma for formulas

Theorem·T46

Satisfying a substituted formula matches satisfying the original after moving the replacement's own value into the assignment, provided the substitution was safe.

For an L-structure , assignment , , , and with , writing :
In words
For an L-structure and assignment, a variable, and a term, and any formula of the language, given that the term is substitutable for the variable in it, writing s' for the assignment updated to send the variable to the value the term has there: satisfying the substituted formula under the assignment matches satisfying the original formula under s'.
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 formula of length (the induction hypothesis, "IH"); show it for of length with . Write .
  2. 2
    By T35 (ii), is exactly one of the five forms of D083.
  3. 3
    eq, rel. If (eq clause, D083, via D109): (eq clause, D098). By the eq clause of D091 and T42 applied to and : iff iff iff (eq clause again, at ). The rel case is identical, using T42 pointwise on the argument tuple, as in the proof of T44.
  4. 4
    neg. If (neg clause, D083): (neg clause, D099), so the IH applies to . (neg clause, D098), so by the neg clause of D091: iff iff (IH) iff .
  5. 5
    bin. If is ( ), ( ), ( ), or ( ) (bin clause, D083): (bin clause, D099), so the IH applies to both and . is the same connective applied to and (bin clause, D098), so by the matching clause of D091 and the IH applied to both sides: iff the same Boolean combination of and iff .
  6. 6
    quant, same variable. If is ( ) or ( ) (quant clause, D083), i.e. the bound variable is exactly : the same clause of D098 forces , so the left side is . Since is the bound variable here, (D093, quant clause: ). By T44 applied with : , i.e. - the claim.
  7. 7
    quant, different variable. If is ( ) or ( ) with : by the quant clause of D099, means , or and . In either branch holds - directly in the second, and in the first because (quant clause, D093) with gives , so T45 applies. So the IH applies to either way, and the diff clause of D098 gives as the same quantifier applied to and . It suffices to show, for every : - then the forall/exists clause of D091 gives iff (for all/some) , the left side, iff (for all/some) , the right side, iff .
  8. 8
    Sub-case . By the IH at : . Since , T43 gives , and since , updates at different coordinates commute (both add the independent pairs , to with the old entries at removed, in either order, Extensionality): . So the right side of the IH becomes , giving the sub-case.
  9. 9
    Sub-case (hence , shown above). By T44 applied to at the base assignment , with reassigned first to and separately to (neither choice matters, as ): and . Combining, and using the IH (at ) on the left: (the last equality by commutativity of updates at different coordinates, as above). This gives the sub-case without needing to relate to at all.
  10. 10
    T08 concludes: the claim holds for every with .
∎

Remarks

The Substitution Lemma, the central technical fact soundness needs to verify universal instantiation and substitutivity of equals are valid: both axioms compare a formula to its substituted form, and this lemma is what says that comparison tracks a single, well-understood change of assignment rather than something satisfaction cannot see through. The substitutability hypothesis is used only in the quantifier, different-variable case, exactly where a naive substitution risks capturing 's own variables. Throughout the proof, compound formulas are named using the ordinary connective and quantifier symbols of D109 rather than spelled out via the raw construction those symbols abbreviate.
Wikipedia ↗FirstOrder.Language.BoundedFormula.realize_subst ↗

Used by

T48T49
Propose an edit1 published revision