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. 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 obtained from an open propositional formula φ by substitution is said to be a substitution instance of φ. If φ is a closed propositional formula we count φ 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, but not all authors additionally require σ(x) = x for all but finitely many variables x. The notation { x1 ↦ t1, ..., xk ↦ tk } refers to a substitution mapping each variable xi to the corresponding term ti, for i=1,...