Similarly: is a substitution instance of: since ψ can be obtained by replacing each A in φ with (A ↔ A).
A propositional formula is a tautology if it is true under every valuation (or interpretation) of its predicate symbols.
This fact implies the soundness of the deduction rule described in the previous section.
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.
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.
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.
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 }.
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.
[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.
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 a property which is most often used in algebra, especially in solving systems of equations, but is apllied in nearly every area of math that uses equality.
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.