Logic and Proof MT24, Quantifier elimination

For any formula of the form $\exists x F$ where $F$ is quantifier-free, there exists a quantifier-free formula $G$ with the same free variables and $\pmb T \models \exists x F \leftrightarrow G$.

(Check the specifics! It is equivalent, not equisatisfiable, and $F$ and $G$ are both quantifier-free).

• You also need a procedure for determining whether or not $F \in \pmb T$ for a variable-free atomic formula $F$ (and hence you can decide whether an arbitrary variable-free formula is in $F$ by applying the procedure to all atoms of the formula).
• Then to decide membership:
  • Convert formula to prenex normal form.
  • Eliminate all quantifiers.
  • Check whether $F’ \in \pmb T$ using procedure

• It suffices just to consider existential quantifiers since $\forall x F \leftrightarrow \lnot \exists x \lnot F$.
• It suffices just to consider conjunctions of literals since any formula $F$ can be put in DNF, and existential quantifiers distribute over disjunctions: $\exists x \bigvee^n _ {i = 1} \bigwedge^m _ {j = 1} L _ {i, j} \leftrightarrow \bigwedge^n _ {i = 1} \exists x \bigvee^m _ {j = 1} L _ {i, j}$.
• If any of the literals don’t mention $x$, we may move these outside the scope of the existential quantifiers.

It suffices to consider formulas $G$ where an existential quantifier $\exists x$ is applied to a conjunction of literals, all of which mention $x$.

Then we may write

\[G = \exists x \left( \bigwedge_{i \in I} x = y_i \land \bigwedge_{j \in J} \lnot (x = y_j) \land \bigwedge_{h \in H} x \sim y_h \land \bigwedge_{k \in K} \lnot (x \sim y_k) \right)\]

If $I \ne \emptyset$, then just replace all occurrences of $x$ by some $y _ i$ and remove the existential quantifier.

If $I = \emptyset$, consider the following formula:

\[G' = \bigwedge_{h, h' \in H} y_h \sim y_{h'} \land \bigwedge_{h \in H, k\in K} \lnot (y_h \sim y_k)\]

We aim to show that $\mathcal T \models G \leftrightarrow G’$. Let $[m]$ denote the equivalence class of $m$ for any $m \in M$, and let $y^\mathcal A$ denote the interpretation of the literal $y$ in model $\mathcal A$.

$\mathcal A \models G$ implies $\mathcal A \models G’$:

Suppose that $\mathcal A \models G$ for some structure $\mathcal A$. Then there is some $m \in M$ to which $x$ is assigned such that

\[\lbrace \mathcal y^\mathcal A_h \mid h\in H\rbrace \subseteq [m]\]

and thus in particular $y^\mathcal A _ h \sim y^\mathcal A _ {h’}$ for all $h, h’ \in H$ by the transitivity of $\sim$. Moreover, $y^\mathcal A _ k \notin [m]$ for all $k \in K$, and hence $y^\mathcal A _ h \not\sim y^\mathcal A _ k$ for all $h \in H$ and $k \in K$.

$\mathcal A \models G’$ implies $\mathcal A \models G$:

Suppose $\mathcal A \models G’$, i.e. $y^\mathcal A _ h \sim y^\mathcal A _ {h’}$ for all $h, h’ \in H$, and $y^\mathcal A _ h \not\sim \mathcal y^\mathcal A _ k$ for all $h \in H$ and $k \in K$. Then it is always possible to pick some $m \in M$ such that ${ y _ h^\mathcal A \mid h \in H }$ and $m \neq y _ h^\mathcal A$ for any $h$, since the equivalence class that all $y _ h^\mathcal A$ lie in is infinite.

Furthermore, since $y _ h^\mathcal A \not\sim y _ k^\mathcal A$ for all $h \in H$ and $k \in K$ by assumption, it follows that $m \sim y^\mathcal A _ h \not\sim y _ k^\mathcal A$ for some $h \in H$ and all $k \in K$. Hence we may take $m$ as the desired $x$.

@example~ @exam~