First-order sentence involving only a symmetric binary relation with only infinite models It's known that there are sentences of first-order logic which only have infinite models, even if our language consists only of a binary relation $R$. An example of such a sentence is 
$$\forall x \exists y Rxy \wedge \forall x \forall y \forall z ((Rxy \wedge Ryz ) \to Rxz) \wedge \neg \exists x Rxx$$
What I'm curious about is whether there are still sentences with only infinite models when we mandate that our binary relation be symmetric?
To phrase the question formally, consider a first-order language $\mathcal{L} = \{R^{2}\}$ (without equality). Let $\phi$ denote the formula
$$\forall x \forall y (Rxy \to Ryx)$$
Is there a sentence $\psi$ of $\mathcal{L}$ such that $\phi \wedge \psi$ has an infinite model, but no finite models?

Let us define the formulas:
$$\kappa_3(x)=\exists u\exists v(Rxu\land Rxv\land Ruv)$$
$$\kappa_4(x)=\exists u\exists v\exists w(Rxu\land Rxv\land Rxw\land Ruv\land Ruw\land Rvw)$$
$$\alpha(x)=\neg\kappa_3(x)$$
$$\beta(x)=\kappa_3(x)\land\neg\kappa_4(x)$$
$$\gamma(x)=\kappa_4(x)$$
$$\sigma(x,y)=\alpha(x)\land\alpha(y)\land\exists u\exists v(Rxu\land Ruv\land Rvy\land\beta(u)\land\gamma(v))$$
Let $\psi$ be the conjunction of the sentences:
$$\forall x\forall y\forall z(\sigma(x,y)\land\sigma(y,z)\to\sigma(x,z))$$
$$\forall x\neg\sigma(x,x)$$
$$\exists x\alpha(x)$$
$$\forall x\exists y(\alpha(x)\to\sigma(x,y))$$
Plainly, $\psi$ has no finite model. On the other hand, it is a straightforward exercise to construct an infinite model of $\phi\land\psi.$
Intuition behind this example. The (irreflexive) models of $\phi$ are just (undirected) graphs. The problem is to construct an asymmetric relation on an undirected graph. Given a vertex $x$ let $f(x)$ denote the maximum number of vertices in a clique containing $x$. For vertices $x$ and $y$, define $x\lt y$ to mean that $f(x),f(y)\le2$ and there is a path $x,u,v,y$ with $f(u)=3$ and $f(v)\ge4$. Then we can write a first order sentence in the language of graph theory which says that the relation $\lt$ restricted to the set $\{x:f(x)\le2\}$ is an irreflexive transitive relation with no greatest element.
