A substitution is a syntactic transformation on formal expressions.To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols with other expressions.
The resulting expression is called a substitution instance, or instance for short, of the original expression.
Where ψ and φ represent formulas of propositional logic, ψ is a substitution instance of φ if and only if ψ may be obtained from φ by substituting formulas for propositional variables in φ, replacing each occurrence of the same variable by an occurrence of the same formula. For example:
(R → S) & (T → S)is a substitution instance of:
P & Q
and
(A ↔ A) ↔ (A ↔ A)is a substitution instance of:
(A ↔ A)
In some deduction systems for propositional logic, a new expression (a proposition) may be entered on a line of a derivation if it is a substitution instance of a previous line of the derivation (Hunter 1971, p. 118). This is how new lines are introduced in some axiomatic systems. In systems that use rules of transformation, a rule may include the use of a substitution instance for the purpose of introducing certain variables into a derivation.
A propositional formula is a tautology if it is true under every valuation (or interpretation) of its predicate symbols. If Φ is a tautology, and Θ is a substitution instance of Φ, then Θ is again a tautology. This fact implies the soundness of the deduction rule described in the previous section.
In first-order logic, a substitution is a total mapping from variables to terms; many, but not all[1] authors additionally require σ(x) = x for all but finitely many variables x. The notation [2] refers to a substitution mapping each variable xi to the corresponding term ti, for i=1,…,k, and every other variable to itself; the xi must be pairwise distinct. Applying that substitution to a term t is written in postfix notation as t ; it means to (simultaneously) replace every occurrence of each xi in t by ti.[3] The result tσ of applying a substitution σ to a term t is called an instance of that term t.For example, applying the substitution to the term
| f( | ALIGN=CENTER | z | , a, g( | x | ), y) | yields |
| f( | h(a,y) | , a, g( | z | ), y) | . |
The domain dom(σ) of a substitution σ is commonly defined as the set of variables actually replaced, i.e. dom(σ) = .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 ts 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 σ−1, such that tσσ−1 = t = tσ−1σ for every term t. However, it is not possible to define an inverse for an arbitrary substitution.
For example, is a ground substitution, is non-ground and non-flat, but linear, is non-linear and non-flat, is flat, but non-linear, is both linear and flat, but not a renaming, since it maps both y and y2 to y2; each of these substitutions has the set as its domain. An example for a renaming substitution is, it has the inverse . The flat substitution cannot have an inverse, since e.g. (x+y) = 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 cannot have an inverse due to a similar loss of origin information e.g. in (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 σ = and τ = is obtained by removing from the substitution those pairs yi ↦ ui for which yi ∈ .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 xi≠ti for all i, the substitution is idempotent if and only if none of the variables xi occurs in any tj. Substitution composition is not commutative, that is, στ may be different from τσ, even if σ and τ are idempotent.[4] [5]
For example, is equal to, but different from . The substitution is idempotent, e.g. ((x+y)) = ((y+y)+y) = (y+y)+y, while the substitution is non-idempotent, e.g. ((x+y)) = ((x+y)+y) = ((x+y)+y)+y. An example for non-commuting substitutions is =, but = .
Substitution is a basic operation in algebra, in particular in computer algebra.[6] [7]
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
P(X)=X5-3X2+5X-17
P(2)=13
P(X+1)=X5+5X4+10X3+7X2+4X-14.
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).