Skip to content
Axiomatic Wiki
Theorem·T46

The substitution lemma for formulas

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 :
In words
For any formula the term is substitutable into: given that substitutability, satisfying the substituted formula matches satisfying the original under an assignment updated to send the substituted variable to the replacement term's own value.
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, 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, D099), so the IH applies to . (neg clause, D098), so by the neg clause of D091: iff iff (IH) iff .
  5. 5
    bin. If ( ): (bin clause, D099), so the IH applies to both 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 ( , bound variable 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 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 . 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.
Wikipedia ↗FirstOrder.Language.BoundedFormula.realize_subst ↗

Used by

T48T49
Propose an edit1 published revision