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} }$
Also see
Sources
- 1972: A.G. Howson: A Handbook of Terms used in Algebra and Analysis ... (previous) ... (next): $\S 1$: Some mathematical language: Variables and quantifiers
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.3$
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.8$ Further Semantic Notions: Exercise $\text{II}.8.25$