An exercise from Boolos' Computability and Logic asks the reader to give an example of a theory which is decidable but not complete. I am wondering if the following suffices.
Let $T$ be a theory with the following axioms: $$\begin{align} \forall x(x\equiv x)\wedge\forall x\forall y(x\equiv y\rightarrow y\equiv x)\wedge\forall x\forall y\forall z((x\equiv y\wedge y\equiv z)\rightarrow x\equiv z)\qquad(1)\\ \forall x\exists y(xRy)\land\forall x\forall y(\neg(xRy\land yRx))\land \forall x\forall y\forall z((xRy\land yRz)\rightarrow xRz)\qquad(2)\\ \forall x\forall y(x\equiv y)\lor\forall x\forall y(x\equiv y\leftrightarrow x=y)\qquad(3)\\ \end{align}$$ (1) defines the equivalence relation, (2) defines an ordering relation $R$ and ensures that all models of $T$ are infinite, and (3) ensures that there are only two isomporphism types of denumerable models.
In particular, the two types of models of (3) are either one of the following:
- ($\mathcal M_1$) models in which all elements are in the same equivalence class, or
- ($\mathcal M_2$) models in which each element is in its own equivalence class.
Such a theory $T$, having no finite models, and having exactly two isomorphism types of denumerable models, is decidable, as discussed here. To show that $T$ is incomplete, is it enough to observe that $$\forall x\forall y (x\equiv y)\qquad(A)$$ is satisfied by $\mathcal M_1$ but not $\mathcal M_2$, and hence that neither $A$ nor $\neg A$ is a consequence of $T$?
If so, are there far simpler ways to construct decidable but incomplete models?