Definition·D098
Substitution into a formula
Replace every occurrence of one variable throughout a formula, except once a quantifier on that same variable is reached: from there down, nothing is left free to replace.
For a language
,
, and
, the result of substituting
for
in a formula
, written
, is characterized by:
In words
An equality of two terms substitutes into each term and so does a relation applied to a tuple of terms. A negation substitutes into the negated formula, and a connective substitutes into both sides. A quantifier over the very variable being replaced is left untouched entirely - nothing under it is free in that variable to begin with - but a quantifier over any other variable substitutes into its 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
Existence and uniqueness of
, for every formula, is T40. Named
, distinct from "subst", exactly as "FV" is kept distinct from "vars". This substitution is *total* - defined for every
- but says nothing about whether the result is *faithful* to the original meaning: if
contains a variable that a quantifier inside
binds, substituting naively can let that variable be captured, changing what the formula says. The axiom schema that uses this operation will restrict to terms
that are free for
in
- a side condition ruling out capture, not built into
itself.