Jump to navigation
Jump to search
## Contents

## Propositional logic[edit]

### Definition[edit]

### Tautologies[edit]

## First-order logic[edit]

## See also[edit]

## Notes[edit]

## References[edit]

## External links[edit]

**Substitution** is a fundamental concept in 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 by other expressions.
The resulting expression is called a **substitution instance**, or short **instance**, 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 symbols in *φ*, replacing each occurrence of the same symbol 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.

In first-order logic, every closed propositional formula that can be derived from an open propositional formula *a* by substitution is said to be a substitution instance of *a*. If *a* is a closed propositional formula we count *a* itself as its only substitution instance.

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 σ: *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. **Applying** that substitution to a term *t* is written in postfix notation as *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]} 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

*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 is 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 structurally 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 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*. 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*_{i}. 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* }.

- Substitution property in Equality (mathematics)#Some basic logical properties of equality
- First-order logic#Rules of inference
- Universal instantiation
- Lambda calculus#Substitution
- Truth-value semantics
- Unification (computer science)
- Metavariable
- Mutatis mutandis
- Rule of replacement
- Substitution (algebra) — about applying substitutions to polynoms and other algebraic expressions

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

- 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 - Kleene, S. C. (1967).
*Mathematical Logic*. Reprinted 2002, Dover. ISBN 0-486-42533-9

- ^
^{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. **^**N. Dershowitz; J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen.*Formal Models and Semantics*. Handbook of Theoretical Computer Science.**B**. Elsevier. pp. 243—320.

- Substitution in
*nLab*

None of the audio/visual content is hosted on this site. All media is embedded from other sites such as GoogleVideo, Wikipedia, YouTube etc. Therefore, this site has no control over the copyright issues of the streaming media.

All issues concerning copyright violations should be aimed at the sites hosting the material. This site does not host any of the streaming media and the owner has not uploaded any of the material to the video hosting servers. Anyone can find the same content on Google Video or YouTube by themselves.

The owner of this site cannot know which documentaries are in public domain, which has been uploaded to e.g. YouTube by the owner and which has been uploaded without permission. The copyright owner must contact the source if he wants his material off the Internet completely.

Wikipedia content is licensed under the GFDL and (CC) license