Alphabetic Substitution is Semantically Equivalent
Jump to navigation
Jump to search
Theorem
Let $\map \phi x$ be a WFF of predicate logic.
Let $z$ be free for $x$ in $\phi$.
Let $z$ not occur freely in $\phi$.
Let $\map \phi z$ be the result of the alphabetic substitution of $z$ for $x$.
Universal Quantifier
- $\forall x: \map \phi x$ and $\forall z: \map \phi z$ are semantically equivalent
Existential Quantifier
- $\exists x: \map \phi x$ and $\exists z: \map \phi z$ are semantically equivalent