1
$\begingroup$

So I am studying the theory of quantifer elimination and have come across the following equivalence. I am defining quantifier elimination as: a theory $T$ admits quantifier-elimination (QE) if every formula $\phi$ is equivalent to a quantifier-free one.

I then want to prove that $T$ admits QE if and only if for any quantifier-free formula $\phi(x,y_1,y_2,...,y_n)$ of $L$, there exists a quantifier-free formula $\psi(y_1,...,y_n)$ such that $$T \models (\forall y_1,...,y_n)(\psi \iff(\exists x)\phi)$$.

I have proved the forward direction I think:

Suppose $T$ admits QE, and suppose $\phi(x,y_1,y_2,...,y_n)$ is a quantifier-free formula. Consider $\exists x\phi(x,y_1,y_2,...,y_n)$. Then as $T$ admits QE, $T \models (\forall y_1,...,y_n)(\psi \iff(\exists x)\phi)$, where $\psi$ is quantifier free formula. I think this is simply by definitions. However, I do not know how to prove the converse, so any help would be hugely appreciated. Thank you.

$\endgroup$

1 Answer 1

1
$\begingroup$

First note that for any formula $\phi(x)$ we have that $\forall x \phi(x)$ and $\neg \exists x \neg \phi(x)$ are equivalent.

Let $\zeta(y_1, \ldots, y_n)$ be any formula. We prove by induction on the structure of $\zeta$ that it is equivalent to a quantifier-free formula (modulo $T$). By the above we may assume that the only quantifiers that appear in $\zeta$ are existential quantifiers. The base case, where $\zeta$ is atomic, is trivial. The induction step for the logical connectives ($\wedge$, $\vee$, $\neg$, $\to$, $\bot$) is also trivial. So we are left with the case where $\zeta$ is of the form $\exists x \phi(x, y_1, \ldots, y_n)$. By the induction hypothesis we may assume that $\phi(x, y_1, \ldots, y_n)$ is equivalent (modulo $T$) to a quantifier-free $\phi'(x, y_1, \ldots, y_n)$. Then by assumption there is quantifier-free $\psi(y_1, \ldots, y_n)$ that is equivalent (modulo $T$) to $\exists x \phi'(x, y_1, \ldots, y_n)$. Putting things together we get $$ T \models \forall y_1 \ldots y_n(\psi(y_1, \ldots, y_n) \leftrightarrow \zeta(y_1, \ldots, y_n)), $$ and so we conclude that $\zeta$ is indeed equivalent to a quantifier-free formula (modulo $T$). This completes the induction and thus the proof.

$\endgroup$
1
  • $\begingroup$ Thank you, this is great! $\endgroup$
    – ta1234
    Nov 17, 2020 at 11:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.