Theorem·T45
A term is always substitutable for a variable not free in the formula
If a variable never occurs free in a formula to begin with, no term can ever capture it there - substitutability is automatic.
For a language
,
, and
with
: for every
:
In words
For any formula where a given variable is not free, true regardless of which term, any term at all is automatically substitutable for that variable there.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1By strong induction on : assume the claim for every formula of length (the induction hypothesis, "IH"); show it for of length with , for an arbitrary .
- 2
- 3eq, rel. The eq and rel clauses of D099 assert unconditionally for these two forms, regardless of or .
- 4
- 5bin. If ( ): (bin clause), so is free in neither nor ; by the IH applied to both, and , and the bin clause of D099 gives .
- 6quant. If ( ): the hypothesis is exactly the first disjunct of the quant clause of D099, so holds immediately - no need for the IH in this case.
- 7T08 concludes: the claim holds for every with not free in it, for every .
∎
Remarks
A quick structural fact, nearly immediate from D099's own clauses (the quantifier case is literally the hypothesis restated), used to simplify the quantifier, different-variable case of the substitution lemma: whenever
turns out not to be free in the outer quantified formula, it is automatically not free in the body either (the bound variable there is a different one), so this theorem hands back substitutability for the body for free, without needing to track which disjunct of substitutability's definition was the reason.