Axiomatic WikiWWikiDDefinitionsSubstitution into a term
Definition·D097
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 (writing terms via the notation for formulas and terms):
For any other variable
with
:
For a function symbol
and
with
:
In words
This holds for every term of the language: 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.