World Library  
Flag as Inappropriate
Email this Article

Substitution (logic)

Article Id: WHEBN0005438948
Reproduction Date:

Title: Substitution (logic)  
Author: World Heritage Encyclopedia
Language: English
Subject: Logic, Contradiction, Resolution inference, Salva congruitate, Substitution (logic)
Collection: Automated Theorem Proving, Concepts in Logic, Logic Programming, Logical Truth, Propositional Calculus, Substitution (Logic)
Publisher: World Heritage Encyclopedia

Substitution (logic)

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 result expression is called a substitution instance of the original expression.


  • Propositional logic 1
    • Definition 1.1
    • Tautologies 1.2
  • First-order logic 2
  • See also 3
  • Notes 4
  • References 5

Propositional logic


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 Φ, always replacing an 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


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

First-order logic

In first-order logic, a substitution is a total mapping σ: VT from variables to terms; the notation { x1t1, ..., xktk } [note 1] 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 { x1t1, ..., xktk }; it means to (simultaneously) replace every occurrence of each xi in t by ti. [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 { xz, zh(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(σ) = { xV | 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) term t containing just 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, { xx1, yy2+4 } is non-ground and non-flat, but linear, { xy2, yy2+4 } is non-linear and non-flat, { xy2, yy2 } is flat, but non-linear, { xx1, yy2 } is both linear and flat, but not a renaming, since is maps both y and y2 to y2; each of these substitutions has the set {x,y} as its domain. An example for a renaming substitution is { xx1, x1y, yy2, y2x }, it has the inverse { xy2, y2y, yx1, x1x }. The flat substitution { xz, yz } cannot have an inverse, since e.g. (x+y) { xz, yz } = 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 xV. The composition of two substitutions σ = { x1t1, ..., xktk } and τ = { y1u1, ..., yl ↦ ul } is obtained by removing from the substitution { x1t1τ, ..., xktkτ, y1u1, ..., ylul } those pairs yiui for which yi ∈ { x1, ..., xk }. 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 { x1t1, ..., xktk } is idempotent if and only if none of the variables xi occurs in any ti. Substitution composition is not commutative, that is, στ may be different from τσ, even if σ and τ are idempotent.[1][2]

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

See also


  1. ^ some authors use [ t1/x1, ..., tk/xk ] 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;
  2. ^ 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 σ: VT there is a unique homomorphism σ: TT that agrees with σ on VT; the above-defined application of σ to a term t is then viewed as applying the function σ to the argument t.


  • 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
  1. ^ David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley. ; here: p.73-74
  2. ^  ; here: p.445-446
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from World eBook Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.