First-order sentence involving only a symmetric binary relation with only infinite models

Question

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?

Answer 1

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.

Answer 2

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

Answer 3

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.