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?


You are searching for the subject known as computable model theory, which is model theory, but with a view to the computability of the models and theories that arise. Many arguments in computable model theory have the nature and flavor of the observation in your question.

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.

  • $\begingroup$ Thanks for the comprehensive answer. $\endgroup$ – Levon Haykazyan Jul 5 '11 at 9:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.