Substitution (logic)

First-order logic

In first-order logic, a substitution is a total mapping σ: V → T from variables to terms; many, but not all authors additionally require σ(x) = x for all but finitely many variables x. The notation { x₁ ↦ t₁, …, x_k ↦ t_k } refers to a substitution mapping each variable x_i to the corresponding term t_i, for i=1,…,k, and every other variable to itself; the x_i must be pairwise distinct. Most authors additionally require each term t_i to be syntactically different from x_i, to avoid infinitely many distinct notations for the same substitution. Applying that substitution to a term t is written in postfix notation as t { x₁ ↦ t₁, ..., x_k ↦ t_k }; it means to (simultaneously) replace every occurrence of each x_i in t by t_i. The result tσ of applying a substitution σ to a term t is called an instance of that term t. For example, applying the substitution { x ↦ z, z ↦ h(a,y) } to the term

The domain dom(σ) of a substitution σ is commonly defined as the set of variables actually replaced, i.e. dom(σ) = { x ∈ V | xσ ≠ x }. A substitution is called a ground substitution if it maps all variables of its domain to ground, i.e. variable-free, terms. The substitution instance tσ of a ground substitution is a ground term if all of t's variables are in σ's domain, i.e. if vars(t) ⊆ dom(σ). A substitution σ is called a linear substitution if tσ is a linear term for some (and hence every) linear term t containing precisely the variables of σ's domain, i.e. with vars(t) = dom(σ). A substitution σ is called a flat substitution if xσ is a variable for every variable x. A substitution σ is called a renaming substitution if it is a permutation on the set of all variables. Like every permutation, a renaming substitution σ always has an inverse substitution σ⁻¹, such that tσσ⁻¹ = t = tσ⁻¹σ for every term t. However, it is not possible to define an inverse for an arbitrary substitution.

For example, { x ↦ 2, y ↦ 3+4 } is a ground substitution, { x ↦ x₁, y ↦ y₂+4 } is non-ground and non-flat, but linear, { x ↦ y₂, y ↦ y₂+4 } is non-linear and non-flat, { x ↦ y₂, y ↦ y₂ } is flat, but non-linear, { x ↦ x₁, y ↦ y₂ } is both linear and flat, but not a renaming, since it maps both y and y₂ to y₂; each of these substitutions has the set {x,y} as its domain. An example for a renaming substitution is { x ↦ x₁, x₁ ↦ y, y ↦ y₂, y₂ ↦ x }, it has the inverse { x ↦ y₂, y₂ ↦ y, y ↦ x₁, x₁ ↦ x }. The flat substitution { x ↦ z, y ↦ z } cannot have an inverse, since e.g. (x+y) { x ↦ z, y ↦ z } = z+z, and the latter term cannot be transformed back to x+y, as the information about the origin a z stems from is lost. The ground substitution { x ↦ 2 } cannot have an inverse due to a similar loss of origin information e.g. in (x+2) { x ↦ 2 } = 2+2, even if replacing constants by variables was allowed by some fictitious kind of "generalized substitutions".

Two substitutions are considered equal if they map each variable to syntactically equal result terms, formally: σ = τ if xσ = xτ for each variable x ∈ V. The composition of two substitutions σ = { x₁ ↦ t₁, …, x_k ↦ t_k } and τ = { y₁ ↦ u₁, …, y_l ↦ u_l } is obtained by removing from the substitution { x₁ ↦ t₁τ, …, x_k ↦ t_kτ, y₁ ↦ u₁, …, y_l ↦ u_l } those pairs y_i ↦ u_i for which y_i ∈ { x₁, …, x_k }. The composition of σ and τ is denoted by στ. Composition is an associative operation, and is compatible with substitution application, i.e. (ρσ)τ = ρ(στ), and (tσ)τ = t(στ), respectively, for every substitutions ρ, σ, τ, and every term t. The identity substitution, which maps every variable to itself, is the neutral element of substitution composition. A substitution σ is called idempotent if σσ = σ, and hence tσσ = tσ for every term t. When x_i≠t_i for all i, the substitution { x₁ ↦ t₁, …, x_k ↦ t_k } is idempotent if and only if none of the variables x_i occurs in any t_j. Substitution composition is not commutative, that is, στ may be different from τσ, even if σ and τ are idempotent.

For example, { x ↦ 2, y ↦ 3+4 } is equal to { y ↦ 3+4, x ↦ 2 }, but different from { x ↦ 2, y ↦ 7 }. The substitution { x ↦ y+y } is idempotent, e.g. ((x+y) {x↦y+y}) {x↦y+y} = ((y+y)+y) {x↦y+y} = (y+y)+y, while the substitution { x ↦ x+y } is non-idempotent, e.g. ((x+y) {x↦x+y}) {x↦x+y} = ((x+y)+y) {x↦x+y} = ((x+y)+y)+y. An example for non-commuting substitutions is { x ↦ y } { y ↦ z } = { x ↦ z, y ↦ z }, but { y ↦ z} { x ↦ y} = { x ↦ y, y ↦ z }.

Mathematics

In mathematics, there are two common uses of substitution: substitution of variables for constants (also called assignment for that variable), and the substitution property of equality, also called Leibniz's Law.

Considering mathematics as a formal language, a variable is a symbol from an alphabet, usually a letter like x, y, and z, which denotes a range of possible values. If a variable is free in a given expression or formula, then it can be replaced with any of the values in its range. Certain kinds of bound variables can be substituted too. For instance, parameters of an expression (like the coefficients of a polynomial), or the argument of a function. Moreover, variables being universally quantified can be replaced with any of the values in its range, and the result will a true statement. (This is called Universal instantiation)

For a non-formalized language, that is, in most mathematical texts outside of mathematical logic, for an individual expression it is not always possible to identify which variables are free and bound. For example, in $\sum _{i<k}{a}_{ik}$, depending on the context, the variable $i$ can be free and $k$ bound, or vice-versa, but they cannot both be free. Determining which value is assumed to be free depends on context and semantics.

The substitution property of equality, or Leibniz's Law (though the latter term is usually reserved for philosophical contexts), generally states that, if two things are equal, then any property of one, must be a property of the other. It can be formally stated in logical notation as:$${\displaystyle (a=b)⟹[\varphi (a)\Rightarrow \varphi (b)]}$$For every $a$ and $b$, and any well-formed formula $\varphi (x)$ (with a free variable x). For example: For all real numbers a and b, if a = b, then a ≥ 0 implies b ≥ 0 (here, ${\displaystyle \varphi (x)}$ is x ≥ 0). This is a property which is most often used in algebra, especially in solving systems of equations, but is applied in nearly every area of math that uses equality. This, taken together with the reflexive property of equality, forms the axioms of equality in first-order logic.

Substitution is related to, but not identical to, function composition; it is closely related to β-reduction in lambda calculus. In contrast to these notions, however, the accent in algebra is on the preservation of algebraic structure by the substitution operation, the fact that substitution gives a homomorphism for the structure at hand (in the case of polynomials, the ring structure).

Algebra

Substitution is a basic operation in algebra, in particular in computer algebra.

A common case of substitution involves polynomials, where substitution of a numerical value (or another expression) for the indeterminate of a univariate polynomial amounts to evaluating the polynomial at that value. Indeed, this operation occurs so frequently that the notation for polynomials is often adapted to it; instead of designating a polynomial by a name like P, as one would do for other mathematical objects, one could define

${\displaystyle P(X)=X^5-3X^2+5X-17}$

so that substitution for X can be designated by replacement inside "P(X)", say

${\displaystyle P(2)=13}$

or

${\displaystyle P(X+1)=X^5+5X^4+10X^3+7X^2+4X-14.}$

Substitution can also be applied to other kinds of formal objects built from symbols, for instance elements of free groups. In order for substitution to be defined, one needs an algebraic structure with an appropriate universal property, that asserts the existence of unique homomorphisms that send indeterminates to specific values; the substitution then amounts to finding the image of an element under such a homomorphism.

Proof of substitution in ZFC

The following is a proof of the substitution property of equality in ZFC (as defined in first-order logic without equality), which is adapted from Introduction to Axiomatic Set Theory (1982) by Gaisi Takeuti and Wilson M. Zaring.

Theorem—if ${\displaystyle a=b}$, then, for any well-formed formula ${\displaystyle \varphi }$, ${\displaystyle \varphi (a)\Rightarrow \varphi (b)}$.

See Zermelo–Fraenkel set theory § Formal language for the definition of formulas in ZFC. The definition is recursive, so a proof by induction is used. In ZFC in first-order logic without equality, "set equality" is defined to mean that two sets have the same elements, written symbolically as "for all z, z is in x if and only if z is in y". Then, the Axiom of Extensionality asserts that if two sets have the same elements, then they belong to the same sets:

Definition—$${\displaystyle (x=y):=\mathrm{\forall }z[z\in x\iff z\in y]}$$

Axiom—$${\displaystyle (x=y)\Rightarrow \mathrm{\forall }z(x\in z\iff y\in z)}$$

Base formulas

Let ${\displaystyle X,Y,Z}$, be metavariables for any variables or sets, such that ${\displaystyle X=Y}$

Case 1: ${\displaystyle \varphi (X):(Z\in X)}$

Assume ${\displaystyle Z\in X}$, then, by the definition of equality, ${\displaystyle Z\in Y}$, thus ${\displaystyle (X=Y)⟹[Z\in X\Rightarrow Z\in Y]}$

Case 2: ${\displaystyle \varphi (X):(X\in Z)}$

Assume ${\displaystyle X\in Z}$, then by the axiom of extensionality, ${\displaystyle Y\in Z}$, thus ${\displaystyle (X=Y)⟹[X\in Z\Rightarrow Y\in Z]}$

Recursive formulas

Let ${\displaystyle \psi ,\phi }$ be meta variables for any formulas with the property that ${\displaystyle (a=b)⟹[\varphi (a)\Rightarrow \varphi (b)]}$. Let ${\displaystyle X,Y}$, be metavariables for any variables or sets, such that ${\displaystyle X=Y}$, and let ${\displaystyle z}$ be a metavariable for any variable.

Case 1: ${\displaystyle \mathrm{\neg }(\psi )}$

Since ${\displaystyle X=Y}$, then ${\displaystyle Y=X}$ by symmetry of equality, therefore ${\displaystyle [\psi (Y)\Rightarrow \psi (X)]}$, by the induction hypothesis, therefore ${\displaystyle [\mathrm{\neg }\psi (X)\Rightarrow \mathrm{\neg }\psi (Y)]}$ by contraposition, thus ${\displaystyle (X=Y)⟹[\mathrm{\neg }\psi (X)\Rightarrow \mathrm{\neg }\psi (Y)]}$

Case 2: ${\displaystyle \psi \wedge \phi }$

Since ${\displaystyle X=Y}$, then ${\displaystyle [\psi (X)\Rightarrow \psi (Y)]}$ and ${\displaystyle [\phi (X)\Rightarrow \phi (Y)]}$, which implies ${\displaystyle [(\psi (X)\wedge \phi (X))\Rightarrow \psi (Y)\wedge \phi (Y))]}$, thus ${\displaystyle (X=Y)⟹[(\psi (X)\wedge \phi (X))\Rightarrow \psi (Y)\wedge \phi (Y))]}$

Case 3: ${\displaystyle \mathrm{\exists }z(\psi )}$

Since ${\displaystyle X=Y}$, ${\displaystyle \psi (X,z)\Rightarrow \psi (Y,z)}$ assume by way of contradiction that the result is false, that is ${\displaystyle \mathrm{\exists }z(\psi (X,z))}$ is true but ${\displaystyle \mathrm{\exists }z(\psi (Y,z))}$ is false. By existential instantiation, let ${\displaystyle z_0}$ denote the value such that ${\displaystyle \psi (X,z_0)}$ is true. Then ${\displaystyle \psi (Y,z_0)}$ is false by asumption, and therefore ${\displaystyle \psi (X,z_0)\Rightarrow \psi (Y,z_0)}$ is false, which contradicts our induction hypothesis, and the result follows.