Axiomatic WikiWWikiDDefinitionsSubstitutable (free for) a variable in a formula
Definition·D099
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
, using the notation of D109:
is substitutable (free) for
in a formula
, written
, is characterized by: for
:
for
and
with
:
for
:
for
:
for
and
:
In words
Whether the term is substitutable for the variable in a formula is defined case by case on how the formula is built: any two terms form an equality that the term is always substitutable into, and a relation symbol applied to a matching-arity tuple of terms is always substitutable into as well - atomic formulas have no quantifiers to worry about. Substitutability into a negation is exactly substitutability into the negated formula. Substitutability into a conjunction, a disjunction, an implication, or a biconditional is substitutability into both sides. Substitutability into a universally quantified formula holds exactly when either the variable being replaced does not occur free there at all, or the quantifier's own bound variable does not occur in the replacement term and the replacement is substitutable into the body, and the same characterization holds for an existentially quantified formula.
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 this definition 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.