THE LOGIC NOTES

Substitution Glossary

Definition

In propositional logic, one formula is a substitution instance of another if it results by substituting formulae for atoms. Substitution must be uniform, the same formula replacing all occurrences of the same atom throughout the original.

A different notion of substitution is important in first order logic: that of substituting a term for another term or for a variable, or conversely substituting a variable for a term. This is simply a matter of replacing all occurrences of one expression by occurrences of the other. In general, where e and e' are any two expressions (not necessarily names), and A any larger expression (not necessarily a formula), Ae'e is just like A except that every occurrence of e in it has been replaced by e'. Analogously, where e1, ..., en is a list of n different expressions, and e'1, ..., e'n is a list of n expressions, we may write

Ae'1, ..., e'ne1, ..., en

for the result of simultaneously replacing e1 by e'1 and e2 by e'2 and so on.

Comments

We may extend the idea of substitution to cover not only substitution in a single formula, but substitution throughout an entire sequent. If a sequent is provable (or valid), so are all of its substitution instances.

There is a concept of a substitution instance applying to full first order logic, based on the idea of substituting formulae expressing predicates for predicate symbols, but it is rather intricate and we do not detail it here.

Examples

  1. NOT(q OR r) IMP p is a substitution instance of p IMP q, resulting from it by substituting NOT(q OR r) for p, and substituting p for q.
  2. If A is the formula Fa OR Fb then  Af(x)b is  Fa OR F(f(x)).  Note that this is not a formula because of the free variable x, but it could be part of a formula such as  ALLx(Fa OR F(f(x)))  where the variable is bound by a quantifier.

Links