Definition:Alphabetic Substitution

From ProofWiki
Jump to navigation Jump to search


Let $\mathbf C$ be a WFF of the language of predicate logic $\LL_1$.

Consider the (abbreviated) WFF $Q x: \mathbf C$ where $Q$ is a quantifier.

Let $y$ be another variable such that:

$y$ is freely substitutable for $x$ in $\mathbf C$
$y$ does not occur freely in $\mathbf C$.

Let $\mathbf C'$ be the WFF resulting from substituting $y$ for all free occurrences of $x$ in $\mathbf C$.

The change from $Q x: \mathbf C$ to $Q y: \mathbf C'$ is called alphabetic substitution.

Also known as

Some sources refer to this process as alphabetic replacement.


As a consequence of the formal grammar of $\LL_1$, it is essential that only the free occurrences of $x$ are replaced.

If this is not adhered to, the statement of the WFF may change, in much the same way as demonstrated on Confusion of Bound Variables.


In practice, the method of alphabetic substitution will be employed mainly to avoid dealing with expressions like:

$\paren {\exists x: \paren {\forall y: x = y \lor \paren {\exists x: x > y} } }$

where the variable $x$ is bound twice.

It is a formal way of ensuring that such erratic (although well-defined by the parentheses) statements have to be dealt with in practical situations.


Take the WFF:

$\map P {x, y} \implies \forall x: \paren {\exists y: \map R {x, y} \implies \map Q {x, y} }$

The first occurrence of $x$ is free.

The other three occurrences of $x$ are bound.

The first and last occurrences of $y$ are free.

The second and third occurrences of $y$ are bound.

The scope of the quantifier $\forall$ is:

$\forall x: \paren {\exists y: \map R {x, y} \implies \map Q {x, y} }$

The scope of the quantifier $\exists$ is:

$\exists y: \map R {x, y}$

By making the alphabetic changes of the bound occurrences of $x$ with $u$, and of $y$ with $v$, we get:

$\map P {x, y} \implies \forall u: \paren {\exists v: \map R {u, v} \implies \map Q {u, y} }$

Also see