Definition·D097
Substitution into a term
Replace every occurrence of one variable in a term by another term; everything else is left untouched, recursing into each function argument.
For a language
,
, and
, the result of substituting
for
in a term
, written
, is characterized by:
In words
The variable being replaced becomes the replacement term itself, any other bare variable is left alone, and a function symbol applied to a tuple of terms substitutes into every argument and reassembles the same function application.
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
Existence and uniqueness of
, for every term, is T39.
(D018) is the tuple of substitution results
. Since a term has no quantifiers to bind a variable, this substitution is total and unconditional - unlike substitution into a formula, which must stop recursing once its target variable is quantified away.