# Existence of some syntactic deduction

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.

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$$.