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?
 A: 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.
A: To formalise Stephen A. Meigs's suggestion, define:
$$\sigma (x,y) = \forall z (Rxz \leftrightarrow Ryz) \\
\kappa (x) = \forall y_{1} \forall y_{2} \forall y_{3} ((Rxy_{1} \wedge Rxy_{2} \wedge Rxy_{3}) \to (\sigma (y_{1},y_{2}) \vee \sigma (y_{2},y_{3}) \vee \sigma (y_{1},y_{3})))  \\
\lambda(x) = \exists y(Rxy \wedge \forall z(Rxz \to \sigma(y,z)))
$$
Then let $\psi$ be the conjunction of:
$$
\forall x \kappa (x) \\
\exists x (\lambda (x) \wedge \forall y (\lambda (y) \to \sigma(y,x))) \\
\forall x \forall y \neg (\sigma(x,y) \wedge Rxy)
$$
A: Here's a way to do it that also constructs a transitive irreflexive relation like bof's answer, but does so in a different way.
Define a relation $aSb$ as follows:
     x
   / |
  /  |
a----+----b    for some x and y is the definition of aSb
  \  |   / 
   \ | /
     y

In other words, let $aSb$ abbreviate $\exists xy ( \lnot xRb \land aRb \land xRy \land yRb \land aRy \land aRx)$.
With this relation, we get strange behavior if self-edges are allowed. It holds that $aSb$ whenever $aRa$ and $aRb$ and $\lnot bRb$. This isn't actually a problem because we insist on the existence of a larger element for each element later, but ruling it out is more intuitive. So let's insist on $\forall a \mathop. \lnot aRa$.
Given the definition of $aSb$ above, it is a theorem that $\forall a \mathop. \lnot aSa$ holds because $aRx$ must be either true or false.
Transitivity is not free, we need to insist that $\forall x y z (xSy \land xSy \to xSz)$.
Antisymmetry is also not free, we must insist that $\forall a b (aSb \to \lnot bSa)$.
Totality is also not free, we must insist that $\forall a \exists b \mathop. aSb$.
If we put this all together we conceptually get a sprawling grid of incomplete $K_4$s expanding out in all directions.
$$ \forall a \mathop ( \lnot aRa) \land \forall x y z (xSy \land ySz \to xSz) \land \forall a b (aSb \to \lnot bSa) \land \forall a \exists b (aSb) $$
Our train of almost-$K_4$s can loop back on itself in weird ways, but insisting on transitivity, irreflexivity, and totality forces us to keep visiting new vertices at a conceptual level.
