Quantifier laws

There are a couple of equivalences involving first-order quantifiers. They are useful for establishing normal forms.

Simple equivalences

There are three simple equivalences involving first-order quantifiers, which somehow draw on the fact that existential quantification is a generalized form of disjunction and universal quantification is a generalized form of conjunction.

Duality (DUAL). For all first-order formulas $\varphi$ and $i \in \mathbf N$, \begin{align*} \neg \exists x_i \varphi & \SemEquiv \forall x_i \neg \varphi \enspace,\\ \neg \forall x_i \varphi & \SemEquiv \exists x_i \neg \varphi \enspace. \end{align*} Commutativity (COMM). For all first-order formulas $\varphi$ and $i,j \in \mathbf N$, \begin{align*} \exists x_i \exists x_j \varphi & \SemEquiv \exists x_j \exists x_i \varphi \enspace,\\ \forall x_i \forall x_j \varphi & \SemEquiv \forall x_j \forall x_i \varphi \enspace. \end{align*} Distributivity (DIST). For all first-order formulas $\varphi_0, \varphi_1$ and $i \in \mathbf N$, \begin{align*} \exists x_i (\varphi_0 \vee \varphi_1) & \SemEquiv \exists x_i \varphi_0 \vee \exists x_i \varphi_1 \enspace,\\ \forall x_i (\varphi_0 \wedge \varphi_1) & \SemEquiv \forall x_i \varphi_0 \wedge \forall x_i \varphi_1 \enspace. \end{align*}

Exercise

1. Show that, in general, an existential quantification does not commute with a universal quantification.
2. Show that, in general, universal quantification does not distribute over disjunction (or, dually, that existential quantification does not distribute over conjunction).

Equivalences with side conditions on the quantified variables

Some of the rules for quantifiers are more complex in the sense that the respective quantifier can only be 'moved' when the quantified variable meets certain conditions.

Elimination (ELIM). For every $i \in \mathbf N$ and every first-order formulas $\varphi$ with $x_i \notin \text{fvars}(\varphi)$, \begin{align*} \exists x_i \varphi & \SemEquiv \varphi \enspace, \\ \forall x_i \varphi & \SemEquiv \varphi \enspace. \end{align*} Shift (SHFT). For $\ast \in \{\vee, \wedge\}$, $Q \in \{\forall, \exists\}$, every $i \in \mathbf N$ and first-order formulas $\varphi_0, \varphi_1$ with $x_i \notin \text{fvars}(\varphi_0)$, \begin{align*} \varphi_0 \ast Q x_i \varphi_1 & \SemEquiv Q x_i (\varphi_0 \ast \varphi_1) \enspace. \end{align*}

Exercise Show that the above side conditions on free variables are necessary.

Renaming of bound variable

The coincidence lemma states that for the interpretation of a formula only the values of the free variables are important. The quantified variables can even be renamed.

Lemma (renaming of bound variable) For every first-order formula $\varphi$, numbers $i, j \in \mathbf N$, and quantifier $Q \in \{\exists, \forall\}$, \begin{align} Q x_i \varphi & \SemEquiv Q x_j (\varphi\{x_i \mapsto x_j\}) && \text{if $x_j \notin \text{fvars}(\varphi)$ and $x_i \notin \text{scope}(x_j, \varphi)$.}\tag{BREN} \end{align}

Proof For the proof, first note that the case $i = j$ is trivial. Next, note that by symmetry it is enough to show $Q x_i \varphi \models Qx_j (\varphi\{x_i \mapsto x_j\})$. Note also that by duality it is enough to show this for one of the quantifiers, say $Q = {\exists}$.

Assume $\mathcal A, \beta \mymodels \exists x_i \varphi$ and the side condition is satisfied. Then there exists $a \in A$ such that $\mathcal A, \beta\left[\frac{x_i}{a}\right] \mymodels \varphi$. Consider the assignment $\beta'$ defined by $\beta' = \beta\left[\frac{x_j}{a}\right]$. We have $\mathcal A, \beta'\left[\frac{x_i}{a}\right] \mymodels \varphi$ because of the coincidence lemma ($x_j \notin \text{fvars}(\varphi)$). Moreover, $\beta'^{ \{x_i \mapsto x_j\} } = \beta'\left[\frac{x_i}{a}\right]$, such that $\mathcal{A},\beta'^{ \{x_i \mapsto x_j\} }\mymodels \varphi$. Note, that there is no name clash in $\varphi$ for $\{x_i \mapsto x_j\}$ because $x_i\not\in\operatorname{scope}(x_j,\varphi)$. From the substitution lemma, we conclude $\mathcal A, \beta' \mymodels \varphi\{x_i \mapsto x_j\}$. Since $\beta' = \beta\left[\frac{x_j}{a}\right]$, this implies $\mathcal A, \beta \mymodels Q x_j (\varphi\{x_i \mapsto x_j\})$.

This concludes the proof of the lemma.

Exercise In the above proof, you find "Note also that by duality [...] quantifiers." Explain this in detail.