Theorem·T41

Substitutability is well-defined

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.

Never needed: F05 · F10 · F13 · A04 · A05 · A09 (computed from the citation graph, not asserted).

Proof

1
By strong induction on : assume the claim for every formula of length (the induction hypothesis, "IH"); show it for of length .
2
By T35 (ii), is exactly one of the five forms of D083.
3
eq, rel. The eq and rel clauses of D099 assert holds unconditionally for these two forms - a specific, determinate verdict, needing no induction.
4
neg, bin. If or ( ): as in the proof of T36. By the IH, whether (and ) holds is already determined; the neg or bin clause of D099 then determines via a fixed Boolean combination.
5
quant. If ( , ): is a determinate fact (T38 gives exists uniquely), as is (T37). If the first holds, the quant clause forces regardless of the second disjunct. Otherwise, by the IH, whether holds is already determined, and the quant clause forces via the remaining disjunct.
6
In every case, mutual exclusivity of the five forms (T35 (ii)) leaves exactly one verdict consistent with D099. T08 concludes: is well-defined for every .

∎

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.

Propose an edit1 published revision