Existence of some syntactic deduction

Question

Given an $\mathcal{L}-$language, prove if it exists or not a deduction for: $$\exists x_1 \exists x_2 \neg \varphi \vdash \neg \exists x_1 \exists x_2 \varphi $$

My idea is that if it exists a syntactic deduction, by the Soundness Theorem it follows the semantic implication, so a set composed of the first formula and the negative of the second is not satisfiable. I have tried this but I am not getting the fact, possible ideas would be appreciated.

Answer 1

First of all, you should recognize that the statement is not true in general. So, we are trying to disprove it.

Therefore, we want to find a model which satisfies both the affirmative of the left-hand side and the negative of the right-hand side. That's actually fairly easy, since we just want two elements such that $\varphi$ is true for them and two elements such that $\varphi$ is false for them. For example, let $\mathcal{M}$ be a model with $\lvert \mathcal{M} \rvert = \{a, b, c, d\}$ and $\varphi^{\mathcal{M}} = \{(a, b)\}$. Then $a, b$ make $\varphi$ true and $c, d$ make $\varphi$ false. Done.

Here I assumed, though, that $\varphi$ was a relational symbol — you haven't specified what it was. If the problem asks if this is true for all formulas $\varphi$ of $\mathcal{L}$, then the above is enough, as we have found a formula for which it is not true. There do exist, though, some formulas for which the statement is true; for example, take $\varphi = \top$.