# A technique for deciding satisfiability in fragments of first-order logic

By Goedels completeness theorem satisfiability in first-order logic is $\Pi_1$. So to obtain decidability in some fragment, it is enough to show that satisfiability is $\Sigma_1$ in this fragment. I wonder if the following technique can work.

Let $\cal F$ be a set of first-order formulas and $\cal M$ a countable set of structures. Assume we can prove that if a sentence $\phi \in \cal F$ is satisfiable, than it has a model $M \in \cal M$. Assume further that $M \models \phi$ is decidable (or at least semi-decidable). Then the satisfiability for $\cal F$ will be $\Sigma_1$ and hence decidable.

Does anybody know results along these lines?

-

In particular, the Effective Completeness Theorem (see page 18 of the Harizanov book to which I linked) is the assertion of the converse of your observation. That is, if a theory $T$ is decidable in the sense that we have an effective procedure to determine $T\vdash \varphi$, then $T$ has a decidable model, a model $M$ built on $\mathbb{N}$, in which the satisfaction relation $M\models\varphi[\vec n]$ is decidable. In particular, by applying a uniform version of that argument, if $T$ is decidable then for each $\varphi$ for which $T+\varphi$ is consistent, we may build a decidable model $M_\varphi\models T+\varphi$. These models therefore function exactly as in your argument.