Showing there does not exist a formal proof of a formula $\phi$.

Question

My problem:

Suppose $R$ is a binary predicate and use the soundness theorem to show that there does not exist a formal proof of $$ \phi =\forall y\exists xR(x,y)\rightarrow \exists x\forall yR(x,y).$$

This is my attempt at a solution.
First, If $\Sigma$ is a set of sentences and $\phi$ is a sentence over $\mathcal{L}$ we say $\Sigma \models \phi$ if and only if for every $\mathcal{L}$ structure $\mathcal{A}$, if $\mathcal{A} \models \Sigma$ then $\mathcal{A} \models \phi$.

The soundness theorem says: If $\Sigma \vdash \phi$ then $\Sigma \models \phi$. Therefore, my idea is to show that $\emptyset \not\models \phi$. Now, $\emptyset \not\models \phi$ if and only if there exists a $\mathcal{L} = \{R\}$ structure $\mathcal{A}$, such that $\mathcal{A} \models \emptyset$, but $\mathcal{A} \not\models \phi$.

Now, let $\mathcal{A} = \{ \emptyset\}$, where $R_{\mathcal{A}} = \emptyset$. We have that $\mathcal{A} \models \emptyset$. Also $\forall x \exists y R(x,y)$ is vacuously true for every substitution of constant symbols from the model $\mathcal{A}$ but $\exists x \forall y R(x,y)$ is false because no such $x$ exists. We conclude $\emptyset \not\models \phi$, and therefore, by the soundness theorem, $\emptyset \not\vdash \phi$ which, by the deduction theorem, says that there is no formal proof of $\exists x\forall y R(x,y)$ from $\forall y \exists x R(x,y)$. My question is: If $\mathcal{L}=\{R\}$ do I need to consider the case where $\mathcal{L}$ has a nonempty $\mathcal{F}_0$ where $\mathcal{F}_0$ denotes the set of functional symbols of $0$-arity?? Or is what I have done thus far enough?

Answer 1

I would not allow the empty structure, so find the "model" $\mathcal{A}$ unsatisfactory. Maybe use instead the structure $\mathcal{A}$, with underlying set $\{a,b\}$, with the interpretation of $R$ holding for the pair $(a,a)$ and the pair $(b,b)$, and nowhere else. Then $\forall x\exists y R(x,y)$ is true in $\mathcal{A}$, but $\exists x\forall yR(x,y)$ is false.

As to the main question of the post, we need not worry about the non-existence of constant symbols in the language.