# Definition:Alphabetic Substitution

## Definition

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.

## Caution

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.

## Note

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.

## Example

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} }$