# Substitution (logic)

**Substitution** is a fundamental concept in logic. Substitution is a syntactic transformation on strings of symbols of a formal language.

In propositional logic, a **substitution instance** of a propositional formula is a second formula obtained by replacing symbols of the original formula by other formulas. For any formal system that is *closed under substitution*, any substitution of a tautology will also produce a tautology.

## Definition

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

and

is a substitution instance of:

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 by substitution is said to be a substitution instance of . If is a closed propositional formula we count itself as its only substitution instance.

## Tautologies

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.

## See also

- Substitution property in Equality (mathematics)#Some basic logical properties of equality
- First-order logic#Rules of inference
- Rule of universal substitution
- Lambda calculus#Substitution
- Truth-value semantics
- Unification (computer science)
- Mutatis mutandis
- Rule of replacement

## References

- 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