Axiomatic WikiWWikiDDefinitionsSubstitution into a formula
Definition·D098
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 (using the notation for formulas and terms): for
:
for
and
with
:
for
:
for
:
for
, substituting into a quantifier over
itself changes nothing:
for
with
and
:
In words
For any formula being substituted into, an equality of two terms substitutes into each term, and a relation symbol applied to a tuple of terms substitutes into every entry of that tuple. A negation substitutes into the negated formula; a conjunction substitutes into both conjuncts, a disjunction substitutes into both disjuncts, an implication substitutes into both its hypothesis and its conclusion, and a biconditional substitutes into both sides. A universal quantifier over the very variable being replaced is left untouched entirely, since nothing under it is free in that variable to begin with, and likewise for an existential quantifier over that variable. A universal quantifier over any other variable keeps that same quantifier and substitutes into its body, and likewise for an existential quantifier over that other variable.
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.