# Suppose that $\Sigma \vdash \exists x \theta$. Do we then have that $\Sigma \vdash \theta$?

This is a problem from A Friendly Introduction to Mathematical Logic by Christopher Leary and Lars Kristiansen which is in Page number 65.

Here's my attempt:

Consider a structure $$\mathfrak{U}$$ and suppose that its universe is $$A=\{ 1,2 \}$$. Consider $$\Sigma$$ be the singleton consisting of the formula $$\exists x(x=y)$$. Then $$\Sigma \vdash \exists x(x=y)$$ and suppose that we had $$\Sigma \vdash x=y$$. Then by Soundness Theorem, $$\Sigma\models x=y$$.

Consider the variable assignment function $$s$$ into $$\mathfrak{U}$$ which sends $$x$$ to $$1$$ and $$y$$ to $$2$$. Then clearly, $$\mathfrak{U}$$ satisfies $$\exists x (x=y)$$ with the assignment $$s$$ as $$\mathfrak{U}$$ satisfies $$x=y$$ with the substituition $$s[x|2]$$. But on the other hand, $$\mathfrak{U}$$ does not satisfy $$x=y$$ with the substituition $$s$$. This would contradict that $$\Sigma\models x=y$$. Hence, it cannot be that $$\Sigma \vdash x=y$$.

Is this counterexample correct? Is there a way to do without appealing to the Soundness Theorem?

As to avoiding soundness: it's difficult, although of course not impossible, to avoid the soundness theorem when proving non-instances of $$\vdash$$. This is because the definition of $$\vdash$$ is a "positive inductive" one - it's set up to be very easy to prove instances of $$\vdash$$, but that has a cost. To see the issue, think about proving $$\top\not\vdash\perp$$; although blindingly obvious, this isn't actually easy (depending on what definition of "$$\vdash$$" you're using anyways).
Broadly speaking, in order to prove $$\Phi\not\vdash\psi$$ you need to produce a set of formulas $$\Theta$$ which is closed under $$\vdash$$, contains $$\Phi$$, and does not contain $$\psi$$ (and verify that of course). The soundness theorem is really just a way of repackaging this task: every structure $$\mathfrak{M}$$ has its associated theory $$Th(\mathfrak{M})$$, which is closed under $$\vdash$$ by soundness, and so we can think about structures instead of theories. However, we can totally "cut out the middleman:" you can produce an entirely syntactic description of $$Th(\mathfrak{A})$$, and prove the relevant properties of this, without ever actually referring to structures.
Can you give a "structure-free" description of $$Th(\mathfrak{A})$$?