Skip to content
Axiomatic Wiki

WTSubstitutability is well-defined

Theorem·T41

def-free-for's clauses never leave a formula undetermined and never force two conflicting verdicts on it.

For a language , , , and : (D099) is a well-defined proposition - D099's clauses determine, uniquely, whether it holds.
In words
For any formula, whether the term is substitutable for the variable in it is settled outright, never left open or contradictorily double-determined.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    placeholder
∎

Remarks

Confirms substitutability is a well-posed notion for every formula, by the same strong-induction-plus-unique-readability pattern used for free variables and substitution - no generalization over assignments needed, since this too is purely syntactic. The proof writes the five shapes of admissible formulas via the usual not/and/or/->/<->/forall/exists notation, rather than spelling out the raw construction.
Wikipedia ↗FirstOrder.Language.BoundedFormula.Subformula ↗
Propose an edit1 published revision