T admits elimination of quantifiers

[mathmari]

Hey!

Say that we work in a language $L$.
A theory $T$ (i.e. a subject of the set of formulas) of $L$ admits elimination of quantifiers if any $L$-formula $\phi (x)$ is equivalent in $T$ to an existential formula.
Let $T$ be an $L$-theory.
Assume that any formula of the form $\exists x \ \ \psi (x, y)$, where $x$ is one variable, $y$ is a tuple of variables and $\psi$ is quantifier-free, is equivalent in $T$ to a quantifier-free formula.
Prove that $T$ admits elimination of quantifiers. I have done the following:

Any formula of $T$ is of the form $$Q_1 x_1 \dots Q_n x_n \ \ \phi (\overline{x}, \overline{y})$$ where $Q_i \in \{\forall, \exists \}$.

We change the order of the $Q_i$'s so that first we have all the $\forall$ and then all the $\exists$.

So we have $$\forall x_1 \dots \forall x_i \exists x_{i+1} \dots \exists x_n \ \ \phi (\overline{x}, \overline{y})$$

We know that $\exists x_n \ \ \phi (\overline{x}, \overline{y}) \leftrightarrow \phi_0 (\overline{x}, \overline{y})$.

So
$$\forall x_1 \dots \forall x_i \exists x_{i+1} \dots \exists x_{n-1} \ \ \phi (\overline{x}, \overline{y})$$

We do the same till we get $$\forall x_1 \dots \forall x_i \ \ \tilde{\phi}_0 (\overline{x}, \overline{y})$$

Since $$\neg \exists x \ \ \psi (x)\equiv \forall x \ \ \neg \psi (x) \\ \neg \forall x \ \ \psi (x)\equiv \exists x \ \ \neg \psi (x)$$ to prove that $\forall x_j \ \ \phi (\overline{x}, \overline{y})$ is quantifier-free, it suffices to prove that its negation is quantifier-free

So $$\neg \forall x_1 \dots \neg \forall x_i \ \ \tilde{\phi}_0 (\overline{x}, \overline{y})\leftrightarrow \exists x_1 \dots \exists x_i \ \ \neg \tilde{\phi}_0 (\overline{x}, \overline{y})$$

Now we do the same as before, $$\exists x_1 \dots \exists x_i \ \ \neg \tilde{\phi}_0 (\overline{x}, \overline{y})\leftrightarrow \exists x_1 \dots \exists x_{i-1} \ \ \neg \tilde{\phi}_0' (\overline{x}, \overline{y})$$

$$\exists x_1 \dots \exists x_{i-1} \ \ \neg \tilde{\phi}_0' (\overline{x}, \overline{y})\leftrightarrow \exists x_1 \dots \exists x_{i-2} \ \ \neg \tilde{\phi}_0'' (\overline{x}, \overline{y})$$

Until we get a quantifier-free formula.

So, we have that any formula of $T$ is equivalent to a quantifier-free formula.

Therefore, $T$ admits elimination of quantifiers.

Is everything correct? Could I improve something? (Wondering)

 

[mmwave]

Hi there! Your proof looks good, but there are a few things that could be improved:

1. In the beginning, it would be helpful to define what you mean by "equivalent" in $T$. Do you mean logically equivalent? Or do you mean equivalent under some interpretation of the language $L$?

2. When changing the order of the quantifiers, it might be helpful to explain why this is possible. For example, you can mention that this is possible because $T$ is an $L$-theory, and thus the quantifiers in a formula can be rearranged without changing its meaning.

3. When doing the steps to eliminate the quantifiers, it might be helpful to explain why each step is valid. For example, when you say "$\exists x_n \ \ \phi (\overline{x}, \overline{y}) \leftrightarrow \phi_0 (\overline{x}, \overline{y})$", you could mention that this is true because of the assumption given in the forum post.

Overall, your proof is correct and well-written. Keep up the good work!