Hubbry Logo
Substitution (logic)Substitution (logic)Main
Open search
Substitution (logic)
Community hub
Substitution (logic)
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Substitution (logic)
Substitution (logic)
Substitution (logic)
View on Wikipedia
from Wikipedia

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.[citation needed]

The resulting expression is called a substitution instance, or instance for short, of the original expression.

Propositional logic

[edit]

Definition

[edit]

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

That is, ψ can be obtained by replacing P and Q in φ with (R → S) and (T → S) respectively. Similarly:

ψ: (A ↔ A) ↔ (A ↔ A)

is a substitution instance of:

φ: (A ↔ A)

since ψ can be obtained by replacing each A in φ with (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.[1][failed verification] 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.

Tautologies

[edit]

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

[edit]

In first-order logic, a substitution is a total mapping σ: V → T from variables to terms; many,[2]: 73 [3]: 445  but not all[4]: 250  authors additionally require σ(x) = x for all but finitely many variables x. The notation { x1 ↦ t1, …, xk ↦ tk }[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. Most authors additionally require each term ti to be syntactically different from xi, to avoid infinitely many distinct notations for the same substitution. Applying that substitution to a term t is written in postfix notation as t { x1 ↦ t1, ..., xk ↦ tk }; 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 { 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 ↦ x1, y ↦ y2+4 } is non-ground and non-flat, but linear, { x ↦ y2, y ↦ y2+4 } is non-linear and non-flat, { x ↦ y2, y ↦ y2 } is flat, but non-linear, { x ↦ x1, y ↦ y2 } 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 {x,y} as its domain. An example for a renaming substitution is { x ↦ x1, x1 ↦ y, y ↦ y2, y2 ↦ x }, it has the inverse { x ↦ y2, y2 ↦ y, y ↦ x1, x1 ↦ 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 σ = { x1 ↦ t1, …, xk ↦ tk } and τ = { y1 ↦ u1, …, yl ↦ ul } is obtained by removing from the substitution { x1 ↦ t1τ, …, xk ↦ tkτ, y1 ↦ u1, …, yl ↦ ul } those pairs yi ↦ ui 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. When xi≠ti for all i, the substitution { x1 ↦ t1, …, xk ↦ tk } 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.[2]: 73–74 [3]: 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

[edit]

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,[5] also called Leibniz's Law.[6]

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.[7] If a variable is free in a given expression or formula, then it can be replaced with any of the values in its range.[8] 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 , 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 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:For every and , and any well-formed formula (with a free variable x). For example: For all real numbers 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 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.[9]

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

[edit]

Substitution is a basic operation in algebra, in particular in computer algebra.[10][11]

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.

Proof of substitution in ZFC

[edit]

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.[12]

Theorem—if , then, for any well-formed formula , .

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—

Axiom—

Base formulas

Let , be metavariables for any variables or sets, such that

Case 1:

Assume , then, by the definition of equality, , thus

Case 2:

Assume , then by the axiom of extensionality, , thus

Recursive formulas

Let be meta variables for any formulas with the property that . Let , be metavariables for any variables or sets, such that , and let be a metavariable for any variable.

Case 1:

Since , then by symmetry of equality, therefore , by the induction hypothesis, therefore by contraposition, thus

Case 2:

Since , then and , which implies , thus

Case 3:

Since , assume by way of contradiction that the result is false, that is is true but is false. By existential instantiation, let denote the value such that is true. Then is false by asumption, and therefore is false, which contradicts our induction hypothesis, and the result follows.

See also

[edit]

Notes

[edit]

Citations

[edit]
  1. ^ Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic. University of California Press (published 1973). p. 118. ISBN 9780520023567. OCLC 36312727. (accessible to patrons with print disabilities)
  2. ^ a b David A. Duffy (1991). Principles of Automated Theorem Proving. Wiley.
  3. ^ 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.
  4. ^ 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.
  5. ^ Sobolev, S. K. (2001) [1994], "Equality axioms", Encyclopedia of Mathematics, EMS Press
  6. ^ 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
  7. ^ Sobolev, S. K. (2001) [1994], "Individual variable", Encyclopedia of Mathematics, EMS Press
  8. ^ Sobolev, S. K. (2001) [1994], "Free variable", Encyclopedia of Mathematics, EMS Press
  9. ^ Fitting, M., First-Order Logic and Automated Theorem Proving (Berlin/Heidelberg: Springer, 1990), pp. 198–200.
  10. ^ Margret H. Hoft; Hartmut F.W. Hoft (6 November 2002). Computing with Mathematica. Elsevier. ISBN 978-0-08-048855-4.
  11. ^ Andre Heck (6 December 2012). Introduction to Maple. Springer Science & Business Media. ISBN 978-1-4684-0484-5. substitution.
  12. ^ Takeuti, Gaisi; Zaring, Wilson M. (1982). "Introduction to Axiomatic Set Theory". Graduate Texts in Mathematics: 6–9. doi:10.1007/978-1-4613-8168-6. ISSN 0072-5285. Archived from the original on 2014-08-06.

References

[edit]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Substitution (logic)

View on Grokipedia
from Grokipedia
In , substitution is the operation of replacing free occurrences of a variable in a term or with another term or , defined recursively to preserve the of the expression. This process is fundamental to formal reasoning, enabling the derivation of new logical statements from axioms and theorems while maintaining semantic validity. In propositional logic, substitution operates on Boolean formulas by replacing a propositional variable p uniformly with any proposition Q throughout a tautology, resulting in another tautology; this is known as the first substitution law. For instance, substituting p → q for p in the double negation law ¬(¬p) ≡ p yields ¬(¬(p → q)) ≡ p → q, which remains logically true. The second substitution law extends this by allowing replacement of one or more occurrences of a subformula P with an equivalent Q in a compound proposition, preserving equivalence; for example, in q → (¬(¬p)), replacing *¬(¬p) *with p simplifies to q → p. These laws facilitate algebraic manipulation of propositions without altering their truth values. In (also called predicate logic), substitution is extended to terms and formulas involving quantifiers, functions, and predicates, but requires caution to avoid variable capture, where a substituted term introduces a variable that becomes bound by an existing quantifier. Formally, for a term s and variable x, the substitution s[t/x] replaces all occurrences of x in s with term t, applied recursively: constants and unrelated variables remain unchanged, while x becomes t, and function applications substitute into their arguments. For formulas, φ[t/x] substitutes t for free occurrences of x in φ only if t is free for x in φ, meaning no free x in φ lies in the scope of a quantifier binding a variable from t; this prevents invalid binding, as in avoiding the capture in ∀y (x < y)[y/x] becoming the false ∀y (y < y). Simultaneous substitutions use a mapping σ: variables to terms, applied as φ[σ], with updates like σ[x := t] to handle multiple replacements while ensuring freshness of variables. Beyond syntax, substitution underpins key logical principles, such as the substitution quantifier , which ensures that if a holds universally, its substituted instance does too, provided side conditions on free variables are met. It plays a central role in proof systems like resolution and , unification in , and semantic interpretations in . In higher-order logics and type theories, substitution extends to binding forms like abstractions, influencing in programming languages.

Propositional Logic

Definition

In propositional logic, substitution is a syntactic operation that replaces occurrences of propositional variables in a (wff) with other wffs, while preserving the overall connective structure of the original formula. This process allows for the uniform transformation of formulas, enabling the derivation of new expressions from existing ones without altering their . A substitution is formally defined as a function σ\sigma that maps a set of propositional variables to wffs, and the application σ(ϕ)\sigma(\phi) to a formula ϕ\phi is defined recursively: if ϕ\phi is an atomic variable pp, then σ(p)\sigma(p) is the wff assigned by σ\sigma to pp; for compound formulas, σ(¬ϕ)=¬σ(ϕ)\sigma(\neg \phi) = \neg \sigma(\phi), σ(ϕ∧ψ)=σ(ϕ)∧σ(ψ)\sigma(\phi \wedge \psi) = \sigma(\phi) \wedge \sigma(\psi), and similarly for other connectives like ∨\vee, →\to, and ↔\leftrightarrow. For example, applying the substitution σ={p↦(q∨r)}\sigma = \{p \mapsto (q \vee r)\} to the (p→p)(p \to p) yields ((q∨r)→(q∨r))((q \vee r) \to (q \vee r)). This resulting remains a tautology, as can be verified by a simple : regardless of the truth values assigned to qq and rr, the antecedent and consequent are identical, making the implication always true. The concept of substitution was early formalized by and in their 1928 work on theoretical logic, where it served as a foundational tool in axiomatic proof systems for propositional calculus. Such substitutions play a key role in axiomatic proof systems by allowing the uniform replacement of variables in axioms and theorems, preserving their validity.

Properties and Tautologies

In propositional logic, substitution preserves semantic properties such as truth values under any valuation. A key theorem states that if a ϕ\phi is a tautology—true under every possible assignment of truth values to its propositional variables—then the result of applying any substitution σ\sigma to ϕ\phi, denoted σ(ϕ)\sigma(\phi), is also a tautology. This preservation holds because substitution commutes with the semantic evaluation of . The proof proceeds by induction on the structure of the , leveraging truth tables or valuations. For atomic propositions, substitution directly replaces the variable, preserving its under the assignment. For compound formulas, assume the property holds for subformulas; then, for a connective like disjunction, the valuation v(σ(ϕ∨ψ))=v(σ(ϕ))∨v(σ(ψ))v(\sigma(\phi \lor \psi)) = v(\sigma(\phi)) \lor v(\sigma(\psi)), and since ϕ∨ψ\phi \lor \psi is tautologous, its value is always true, so the substituted version inherits this under any extended valuation. Similar reasoning applies to other connectives (conjunction, , implication), ensuring the overall evaluates to true universally. For instance, consider the tautology p∨¬pp \lor \neg p. Substituting q∧rq \land r for pp yields (q∧r)∨¬(q∧r)(q \land r) \lor \neg (q \land r), which remains true for all assignments to qq and rr, as verified by exhaustive evaluation: the disjunction covers both cases where q∧rq \land r is true or false. Substitutions in propositional logic require uniformity: all occurrences of a given propositional variable must be replaced by the identical formula throughout the expression. This uniformity maintains the formula's logical structure and prevents inconsistencies that could arise from non-uniform replacements, even in the absence of quantifiers. Although substitutions preserve tautology, they may introduce redundancy by expanding the formula's complexity without altering its validity; however, no substitution can invalidate a tautology.

First-Order Logic

Definition and Notation

In first-order logic, substitution extends the propositional notion by applying to terms and formulas, where variables in terms are replaced by other terms, and this replacement propagates through predicates and quantifiers to maintain structural integrity. A substitution σ\sigma is formally defined as a finite mapping from variables to terms, denoted σ={x1/t1,…,xn/tn}\sigma = \{x_1 / t_1, \dots, x_n / t_n\}, where the xix_i are distinct variables and the tit_i are terms; it is extended to all variables by leaving others unchanged. The application of σ\sigma to a term tt, written σ(t)\sigma(t), is defined recursively: if tt is a variable xx, then σ(x)=ti\sigma(x) = t_i if x=xix = x_i for some ii, else σ(x)=x\sigma(x) = x; if t=f(s1,…,sk)t = f(s_1, \dots, s_k), then σ(t)=f(σ(s1),…,σ(sk))\sigma(t) = f(\sigma(s_1), \dots, \sigma(s_k)). For atomic formulas, if ϕ=P(t1,…,tk)\phi = P(t_1, \dots, t_k) where PP is an kk-ary predicate symbol, then σ(ϕ)=P(σ(t1),…,σ(tk))\sigma(\phi) = P(\sigma(t_1), \dots, \sigma(t_k)). The extension to compound formulas is recursive: for Boolean connectives, σ(¬ϕ)=¬σ(ϕ)\sigma(\neg \phi) = \neg \sigma(\phi), σ(ϕ∧ψ)=σ(ϕ)∧σ(ψ)\sigma(\phi \land \psi) = \sigma(\phi) \land \sigma(\psi), and similarly for ∨\lor, →\to, and ↔\leftrightarrow; for quantifiers, σ(∀x ϕ)=∀x σ(ϕ)\sigma(\forall x \, \phi) = \forall x \, \sigma(\phi) provided xx does not occur free in the terms of σ\sigma, with adjustments for potential variable capture addressed separately, and analogously for ∃x ϕ\exists x \, \phi. For example, applying the substitution σ={x/f(y)}\sigma = \{x / f(y)\} to the formula ∀x P(x)\forall x \, P(x) yields ∀x P(f(y))\forall x \, P(f(y)) under conditions avoiding capture, whereas a simple atomic substitution like σ={x/c}\sigma = \{x / c\} in P(x,y)P(x, y) produces P(c,y)P(c, y). This framework for substitution was initially formalized in the ramified type theory of by and during the 1910s, using notations like the for propositional functions to handle substitutions in quantified contexts. It was refined in modern treatments, such as Herbert B. Enderton's A Mathematical Introduction to Logic (1972), which provides the recursive definitions and notations standard in contemporary .

Variable Binding and Safety

In , variables are classified as free or bound depending on their occurrence within the scope of quantifiers. A variable is free in a if it is not within the scope of a universal quantifier ∀\forall or existential quantifier ∃\exists that binds it; such free variables can be substituted without restriction, as they act like placeholders for arbitrary terms. In contrast, bound variables are those captured by a quantifier in whose scope they appear, requiring caution during substitution to preserve the intended meaning, since altering bound variables could change the 's semantics. The variable capture problem arises when a substitution inadvertently binds a variable from the substituting term due to a quantifier in the target , leading to an incorrect alteration of scope. For instance, consider the ∀x P(x)\forall x \, P(x) and a substitution σ\sigma that replaces some free variable yy with a term tt containing xx freely; if applied naively to a larger context where yy is bound elsewhere, it may result in σ(∀x P(x))\sigma(\forall x \, P(x)) binding the xx in tt unexpectedly, such as transforming ∀x (Q(y)→P(x))\forall x \, (Q(y) \to P(x)) under σ={y↦x}\sigma = \{y \mapsto x\} into ∀x (Q(x)→P(x))\forall x \, (Q(x) \to P(x)), which equates yy to the bound xx rather than a free occurrence. This issue, known as capture, violates the preservation of and satisfaction. To ensure correctness, a substitution σ\sigma is safe for a formula ϕ\phi if it avoids capture, meaning no variable in the domain of σ\sigma becomes unexpectedly bound in σ(ϕ)\sigma(\phi). Formally, for each variable xx in \dom(σ)\dom(\sigma), either xx is not free in ϕ\phi, or the term σ(x)\sigma(x) contains no variables that are bound in ϕ\phi; this condition, often called the freshness requirement, guarantees that σ(ϕ)\sigma(\phi) preserves the free variables and satisfaction under interpretations. Safe substitutions are crucial for maintaining semantic properties, as captured in the Translation Lemma: if no variable in term tt is bound in formula FF, then an interpretation satisfies F[t/x]F[t/x] if and only if the modified assignment does for FF. Alpha-renaming addresses capture by renaming bound variables to fresh ones before applying substitution, preserving logical equivalence since formulas differing only in bound variable names are equivalent. For example, to substitute term tt for yy in ∀y Q(y)\forall y \, Q(y), first rename to ∀z Q(z)\forall z \, Q(z) where zz is fresh (not free in Q(y)Q(y) or tt), yielding ∀z Q(z)[y↦t]=∀z Q(t)\forall z \, Q(z)[y \mapsto t] = \forall z \, Q(t) if yy does not appear bound in QQ; this ensures tt's variables remain free. The equivalence is formalized as: ∀x ϕ≡∀y ϕ[y/x]\forall x \, \phi \equiv \forall y \, \phi[y/x] if yy is not free in ϕ\phi. In , safe substitutions underpin rules for quantifier instantiation, such as universal elimination (∀\forall-E), which substitutes a closed term tt for the bound variable xx in ∀x ϕ(x)\forall x \, \phi(x) to derive ϕ(t)\phi(t), provided tt avoids capture via freshness. Similarly, existential introduction (∃\exists-I) applies substitution to introduce ∃x ϕ(x)\exists x \, \phi(x) from ϕ(t)\phi(t), while the eigenvariable condition in universal introduction (∀\forall-I) and existential elimination (∃\exists-E) enforces safety by restricting constants to those not occurring freely in assumptions or conclusions, preventing invalid bindings. These rules rely on alpha-renaming to handle variable clashes during proofs. A key result is the simultaneous substitution theorem, which ensures that composing safe substitutions yields correct results: for a term tt and assignment β\beta, β(tσ)=(β∘σ)(t)\beta(t\sigma) = (\beta \circ \sigma)(t), and for a FF, β(Fσ)=(β∘σ)(F)\beta(F\sigma) = (\beta \circ \sigma)(F), proven by and preserving semantic evaluation. This theorem validates multi-variable substitutions in derivations, such as in Skolemization or resolution, by confirming syntactic operations align with interpretations.

Mathematical Applications

Algebra

In universal algebra, substitution refers to the operation of replacing variables in terms—formal expressions constructed from a of operation symbols and variables—with other terms or elements, thereby generating new terms while preserving the . Terms are defined recursively over a set of variables XX and a type FF, starting with variables and constants, and extending via function applications such as f(p1,…,pn)f(p_1, \dots, p_n) where pip_i are terms and f∈Fnf \in F_n. This replacement ensures that algebraic identities, which are equations holding universally in a class of algebras (a variety), remain valid after substitution; for instance, if p≈qp \approx q is an identity in a variety VV, then for any substitution σ\sigma, pσ≈qσp^\sigma \approx q^\sigma holds in all algebras of VV. Such substitutions extend to term functions pA:An→Ap^A: A^n \to A in an AA, where commutes with homomorphisms and preserves congruences, facilitating the study of free algebras and equational theories. A concrete example arises in group theory, where the identity x⋅x−1=ex \cdot x^{-1} = e (with ee the ) holds universally. Substituting xx with the term g⋅yg \cdot y (where gg is a constant and yy a variable) yields (g⋅y)⋅(g⋅y)−1=e(g \cdot y) \cdot (g \cdot y)^{-1} = e, which simplifies to g⋅y⋅y−1⋅g−1=eg \cdot y \cdot y^{-1} \cdot g^{-1} = e using group axioms, demonstrating how substitution preserves the identity and illustrates the preservation of homomorphisms between group structures. In term rewriting systems, central to equational logic, substitution is a core mechanism for applying reduction rules: given a rule l→rl \to r (where ll and rr are terms with variables from a set, and free variables of rr are contained in those of ll), a substitution σ\sigma transforms it to σ(l)→σ(r)\sigma(l) \to \sigma(r), enabling the rewriting of terms in contexts C[σ(l)]→C[σ(r)]C[\sigma(l)] \to C[\sigma(r)]. This process supports and completion algorithms, ensuring decidability of word problems in certain varieties. Substitutions act as endomorphisms on the term algebra Term(Σ)\mathrm{Term}(\Sigma), the absolutely free over a Σ\Sigma on countably many variables, mapping terms to terms while preserving operations; they are fully determined by their action on variables and compose naturally as σ∘τ\sigma \circ \tau. Ground substitutions, which map variables to constant (variable-free) terms, exhibit : σ∘σ=σ\sigma \circ \sigma = \sigma, as their domain and are disjoint, a crucial for unification and normalization in . These endomorphisms generate the clone of a variety, linking substitutions to fully invariant congruences that define equational theories. The development of substitution in this context gained prominence in the through the Knuth-Bendix completion algorithm, which uses substitutions to overlap and reduce rules for solving word problems in groups and other algebras, transforming incomplete sets of identities into confluent systems. Propositional substitutions, which replace atomic propositions in formulas while avoiding capture, extend to algebraic varieties through Herbrand interpretations, where ground term instances (via substitutions) reduce first-order equational reasoning to propositional satisfiability over the Herbrand universe of terms. Herbrand's theorem underpins this by showing that an existential equational formula is provable in a variety if and only if a finite disjunction of its ground instances (obtained by substitutions) is propositionally valid, bridging logical deduction with algebraic equation solving in varieties.

Set Theory

In Zermelo-Fraenkel set theory with choice (ZFC), the plays a central role in enabling functional substitution, allowing the construction of new sets from existing ones by applying a definable function to each element of a given set. Specifically, if a ϕ(x,y)\phi(x, y) defines a functional relationship—meaning for every xx there exists a unique yy such that ϕ(x,y)\phi(x, y) holds—then for any set aa, the collection {y∣∃x∈a ϕ(x,y)}\{ y \mid \exists x \in a \, \phi(x, y) \} is itself a set. This schema ensures that substitution preserves set existence, providing the axiomatic foundation for replacing terms in set definitions and formalizing mathematical constructions like transfinite recursions and large cardinalities. Without it, ZFC would be limited to , unable to generate sets such as the first uncountable ordinal ω1\omega_1 or the von Neumann hierarchy beyond finite ranks. The admissibility of substitution in ZFC follows from the interplay of the with the . Formally, for any formula ϕ(x,y,p)\phi(x, y, \mathbf{p}) with free variables xx and yy (and parameters p\mathbf{p}), the schema states: ∀a∀p(∀x∈a ∃!y ϕ(x,y,p)→∃b ∀y(y∈b↔∃x∈a ϕ(x,y,p)))\forall a \forall \mathbf{p} \bigl( \forall x \in a \, \exists! y \, \phi(x, y, \mathbf{p}) \to \exists b \, \forall y \bigl( y \in b \leftrightarrow \exists x \in a \, \phi(x, y, \mathbf{p}) \bigr) \bigr). The , ∀x∀y(∀z(z∈x↔z∈y)→x=y)\forall x \forall y \bigl( \forall z (z \in x \leftrightarrow z \in y) \to x = y \bigr), guarantees that the resulting set bb is uniquely determined by its elements, ensuring that substitutions yield well-defined sets without ambiguity in membership. This combination admits term replacement: if ϕ(a,z)\phi(a, z) defines a function on elements of aa, then {z∣∃x∈a ϕ(x,z)}\{ z \mid \exists x \in a \, \phi(x, z) \} exists as a set, allowing systematic substitution in set-theoretic expressions while maintaining extensional equality. A representative example of substitution via replacement arises in comprehending subsets of power sets. Consider the power set P(a)\mathcal{P}(a) of a set aa, which exists by the power set axiom. To form the set of all singletons {{x}∣x∈a}\{ \{x\} \mid x \in a \}, apply replacement with ϕ(x,y)\phi(x, y) defined as y={x}y = \{x\} (using the pairing axiom for singletons); the schema ensures this image is a set, enabling further substitutions like mapping to subsets without violating the axiom of foundation, which prevents infinite descending membership chains. Such substitutions in comprehension allow constructing Cartesian products, for instance, ∏ι∈IAι={f∈IP(A)∣∀ι∈I f(ι)∈Aι}\prod_{\iota \in I} A_\iota = \{ f \in I^{\mathcal{P}(A)} \mid \forall \iota \in I \, f(\iota) \in A_\iota \}, where replacement collects the functional images into a set. Challenges in substitution within ZFC include avoiding paradoxes like Russell's, which arises from unrestricted comprehension. The replacement schema addresses this by restricting formulas ϕ(x,y)\phi(x, y) to those with properly bound variables—quantifiers bind variables within the scope, preventing self-referential free variables that could define paradoxical sets like the Russell class R={x∣x∉x}R = \{ x \mid x \notin x \}. Combined with the axiom schema of , which bounds comprehension to subsets of existing sets, replacement ensures substitutions operate on bounded domains, eliminating global self-reference and maintaining consistency. In von Neumann–Bernays–Gödel (NBG) , substitution is supported by both the class comprehension and a replacement for classes, contrasting with the set-specific replacement in ZFC. Formally, for any ϕ(x)\phi(x) without class quantifiers, there exists a class AA such that x∈A↔ϕ(x)x \in A \leftrightarrow \phi(x); this allows replacement over classes, potentially yielding proper classes, and contrasts with ZFC by incorporating classes as primitive objects while remaining a conservative extension—proving the same theorems about sets. Historically, Abraham Fraenkel's 1922 addition of the replacement axiom formalized substitution to accommodate infinite constructions, building on Zermelo's 1908 system and addressing limitations in handling transfinite sequences. Fraenkel proposed it to ensure the existence of images under definable mappings, resolving issues in earlier theories and enabling the full iterative hierarchy essential for modern mathematics.

References

  1. https://builds.openlogicproject.org/content/first-order-logic/syntax-and-semantics/substitution.pdf
  2. https://eng.libretexts.org/Bookshelves/Computer_Science/Programming_and_Computation_Fundamentals/Delftse_Foundations_of_Computation/01%3A_Logic/1.02%3A_Boolean_Algebra/1.2.02%3A_Substitution_Laws
  3. https://liacs.leidenuniv.nl/~basoldh/education/itl20/substitution.pdf
  4. https://theory.stanford.edu/~arbrad/slides/cs156/lec2-4.pdf
  5. https://ncatlab.org/nlab/show/substitution
  6. https://plato.stanford.edu/entries/logic-propositional/
  7. https://iep.utm.edu/propositional-logic-sentential-logic/
  8. https://lara.epfl.ch/w/sav08:substitution_theorems_for_propositional_logic
  9. https://builds.openlogicproject.org/courses/enderton/open-logic-enderton.pdf
  10. https://users.cecs.anu.edu.au/~jks/LogicNotes/glossary/g_substitution.html
  11. http://www.linguist.univ-paris-diderot.fr/~amsili/Ens20/pdf/Formal_Tools_ho_PropLogic.pdf
  12. https://plato.stanford.edu/entries/pm-notation/
  13. https://www.cs.yale.edu/homes/piskac/teaching/decpro-729/fol.pdf
  14. https://www.cs.ox.ac.uk/people/james.worrell/lecture10.pdf
  15. https://builds.openlogicproject.org/content/first-order-logic/natural-deduction/natural-deduction.pdf
  16. https://math.hawaii.edu/~ralph/Classes/619/univ-algebra.pdf
  17. http://voutsadakis.com/TEACH/LECTURES/UNVALG/Chapter2b.pdf
  18. https://www2.math.uu.se/~palmgren/tillog/equlogic07.pdf
  19. https://www.karlin.mff.cuni.cz/~barto/Articles/clonesuniv.pdf
  20. https://www.cs.tufts.edu/~nr/cs257/archive/don-knuth/knuth-bendix.pdf
  21. https://www.researchgate.net/publication/2734763_Herbrand%27s_Theorem_and_Equational_Reasoning_Problems_and_Solutions
  22. https://math.bu.edu/people/aki/20.pdf
  23. https://people.math.ethz.ch/~halorenz/4students/LogikGT/Ch13.pdf
  24. https://ncatlab.org/nlab/show/axiom+of+replacement
  25. https://www.britannica.com/science/set-theory/The-Neumann-Bernays-Godel-axioms
  26. http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=GDZPPN002268760
Add your contribution
Related Hubs
User Avatar
No comments yet.