Skip to content
Axiomatic Wiki

WTSubstitution into a formula exists and is unique

Theorem·T40

The recursive substitution characterization genuinely determines exactly one formula, for every formula substituted into.

For a language , , , and : (D098) exists and is unique.
In words
For any formula substituted into, its substitution result exists and is unique.
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 every formula of length has existing uniquely (the induction hypothesis, "IH"); show the same for of length .
  2. 2
    By T35 (ii), is exactly one of the five forms of D083.
  3. 3
    eq, rel. If is ( ): T39 gives and exist uniquely - unconditionally, independent of this induction - so is a specific formula (D109); the eq clause of D098 forces to equal it. Similarly if is : is a genuine function (by T39 applied to each entry), so is a specific formula (D109); the rel clause forces to equal it.
  4. 4
    neg, bin. If is ( , as in the proof of T36): by the IH, exists uniquely, so the neg clause forces . Likewise if is for ( , ): by the IH applied to and to , both and exist uniquely, and the bin clause forces .
  5. 5
    quant. If is for ( , , ): exactly one of or holds. If , the same clause of D098 forces outright - no induction needed. If , the diff clause applies instead: by the IH, exists uniquely, so the clause forces . The same and diff clauses never both apply (their hypotheses , are exclusive).
  6. 6
    In every case, mutual exclusivity of the five forms (T35 (ii)), and (in the quant case) of versus , leave exactly one formula consistent with D098. T08 concludes: exists and is unique for every .
∎

Remarks

Confirms the notation is well posed for every formula. As in the free-variable case, no generalization over assignments is needed - substitution is purely syntactic - but unlike that case, the quantifier clause genuinely splits in two (same variable versus a different one), each pinning down the value by a different route. The proof writes each case using the ordinary notation for formulas and terms (negation, the binary connectives, the quantifiers, equality, and relation application) rather than spelling out the underlying construction directly.
Wikipedia ↗FirstOrder.Language.BoundedFormula.subst ↗
Propose an edit1 published revision