Alphabetic Substitution is Semantically Equivalent

From ProofWiki
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