# Substitution (logic)

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.

## Propositional logic

### Definition

Where *ψ* and *φ* represent

*ψ*is a

*substitution instance*of

*φ*if and only if

*ψ*may be obtained from

*φ*by substituting formulas for propositional variables

*φ*, 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

*substitution instance*for the purpose of introducing certain variables into a derivation.

### Tautologies

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.

## First-order logic

In first-order logic, a *substitution* is a total mapping *σ*: *V* → *T* from variables to terms; many,^{[1]}^{: 73 }^{[2]}^{: 445 } but not all^{[3]}^{: 250 } authors additionally require *σ*(*x*) = *x* for all but finitely many variables *x*. The notation { *x*_{1} ↦ *t*_{1}, …, *x*_{k} ↦ *t*_{k} }^{[note 1]}
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

*t*{

*x*

_{1}↦

*t*

_{1}, ...,

*x*

_{k}↦

*t*

_{k}}; it means to (simultaneously) replace every occurrence of each

*x*

_{i}in

*t*by

*t*

_{i}.

^{[note 2]}

*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

*f*(*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*(*σ*) = { *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 *σ*^{−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, { *x* ↦ 2, *y* ↦ 3+4 } is a ground substitution, { *x* ↦ *x*_{1}, *y* ↦ *y*_{2}+4 } is non-ground and non-flat, but linear,
{ *x* ↦ *y*_{2}, *y* ↦ *y*_{2}+4 } is non-linear and non-flat, { *x* ↦ *y*_{2}, *y* ↦ *y*_{2} } is flat, but non-linear, { *x* ↦ *x*_{1}, *y* ↦ *y*_{2} } is both linear and flat, but not a renaming, since it maps both *y* and *y*_{2} to *y*_{2}; each of these substitutions has the set {*x*,*y*} as its domain. An example for a renaming substitution is { *x* ↦ *x*_{1}, *x*_{1} ↦ *y*, *y* ↦ *y*_{2}, *y*_{2} ↦ *x* }, it has the inverse { *x* ↦ *y*_{2}, *y*_{2} ↦ *y*, *y* ↦ *x*_{1}, *x*_{1} ↦ *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*_{1} ↦ *t*_{1}, …, *x*_{k} ↦ *t*_{k} } and *τ* = { *y*_{1} ↦ *u*_{1}, …, *y*_{l} ↦ u_{l} } is obtained by removing from the substitution { *x*_{1} ↦ *t*_{1}*τ*, …, *x*_{k} ↦ *t*_{k}*τ*, *y*_{1} ↦ *u*_{1}, …, *y*_{l} ↦ *u*_{l} } those pairs *y*_{i} ↦ *u*_{i} for which *y*_{i} ∈ { *x*_{1}, …, *x*_{k} }.
The composition of *σ* and *τ* is denoted by *στ*. Composition is an

*ρσ*)

*τ*=

*ρ*(

*στ*), and (

*tσ*)

*τ*=

*t*(

*στ*), respectively, for every substitutions

*ρ*,

*σ*,

*τ*, and every term

*t*. The

*identity substitution*, which maps every variable to itself, is the

*σ*is called

*idempotent*if

*σσ*=

*σ*, and hence

*tσσ*=

*tσ*for every term

*t*. When

*x*

_{i}≠

*t*

_{i}for all

*i*, the substitution {

*x*

_{1}↦

*t*

_{1}, …,

*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.

^{[1]}

^{: 73–74 }

^{[2]}

^{: 445–446 }

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*,^{[4]} also called *Leibniz's Law*.^{[5]}

Considering mathematics as a

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 , depending on the context, the variable can be free and 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

*a*and

*b*, if

*a*=

*b*, then

*a*≥ 0 implies

*b*≥ 0 (here, is

*x*≥ 0). This is a property which is most often used in

^{[8]}

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).^{[citation needed]}

### Algebra

Substitution is a basic operation in algebra, in particular in computer algebra.^{[9]}^{[10]}

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

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

or

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.

## See also

- Integration by substitution
- Lambda calculus § Substitution
- String interpolation
- Substitution property of Equality
- Trigonometric substitution
- Universal instantiation

## Notes

**^**Some authors use [*t*_{1}/*x*_{1}, …,*t*_{k}/*x*_{k}] to denote that substitution, e.g. M. Wirsing (1990). Jan van Leeuwen (ed.).*Algebraic Specification*. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 675–788., here: p. 682.**^**From a term algebra point of view, the set*T*of terms is the free term algebra over the set*V*of variables, hence for each substitution mapping σ:*V*→*T*there is a unique homomorphism σ:*T*→*T*that agrees with σ on*V*⊆*T*; the above-defined application of*σ*to a term*t*is then viewed as applying the function*σ*to the argument*t*.

## Citations

- ^
^{a}^{b}David A. Duffy (1991).*Principles of Automated Theorem Proving*. Wiley. - ^
^{a}^{b}Franz Baader, Wayne Snyder (2001). Alan Robinson and Andrei Voronkov (ed.).*Unification Theory*(PDF). Elsevier. pp. 439–526. Archived from the original (PDF) on 2015-06-08. Retrieved 2014-09-24. **^**N. Dershowitz; J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.).*Formal Models and Semantics*. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.- ISBN 1402006098.
**^**Deutsch, Harry and Pawel Garbacz, "Relative Identity", The Stanford Encyclopedia of Philosophy (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman (eds.), forthcoming URL: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden- ISBN 1402006098. Retrieved 2024-09-05.
**.****^**Fitting, M.,*First-Order Logic and Automated Theorem Proving*(Berlin/Heidelberg: Springer, 1990), pp. 198–200.- ISBN 978-0-08-048855-4.
**.**substitution.

**
**## References

- Crabbé, M. (2004).
*On the Notion of Substitution*. Logic Journal of the IGPL, 12, 111–124. - Curry, H. B. (1952)
*On the definition of substitution, replacement and allied notions in an abstract formal system*. Revue philosophique de Louvain 50, 251–269. - Hunter, G. (1971).
*Metalogic: An Introduction to the Metatheory of Standard First Order Logic*. University of California Press.ISBN 0-520-01822-2

## External links

- Substitution at the
*n*Lab