Definition·D099
Substitutable (free for) a variable in a formula
A term is safe to substitute for a variable exactly when doing so cannot let any of its own variables be swept under a quantifier it passes through.
For a language
,
, and
:
is substitutable (free) for
in a formula
, written
, is characterized by:
In words
Any term is substitutable into an equality and into a relation applied to a tuple of terms - atomic formulas have no quantifiers to worry about. Substitutability into a negation is substitutability into the negated formula, and into a connective, substitutability into both sides. Substitutability into a quantified formula holds when either the variable being replaced is not free there at all, or the quantifier's own variable does not occur in the replacement term and the replacement is substitutable into the body.
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).
Remarks
The side condition naive substitution needs to stay faithful: if
fails, some free occurrence of
in
sits inside a quantifier binding a variable that also occurs in
, so
would let
's own variable get captured - accidentally bound by that quantifier instead of standing for whatever value it names. For instance, with
:
becomes, after a naive substitution of
for
,
- always true, though the original said "
equals every value of
", a claim that need not hold. This is exactly the case D099 rules out:
and
is free in the body, so
fails. Existence and uniqueness of whether
holds, for every formula, is T41. The only axiom that will need this guard is
: without it, that schema is unsound.