Suppose $\sigma$ is a vocabulary of First Order logic consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence (FO formula with no free variables). Is it decidable whether there is a finite directed graph $G$, with all in- and out-degrees $0$ or $1$, such that $G\models \phi$ ?

  • $\begingroup$ Welcome to Computer Science! Your question is underspecified: what does "vocabulary" mean here? What kind of logic are you considering, and how are graphs models for formulae in this logic? I'm closing this for now so you can improve it; please flag for reopening once you added or referenced the necessary detail. $\endgroup$ – Raphael Mar 13 '13 at 14:43
  • $\begingroup$ What have you tried? Have you tried to show whether or not it admits quantifier elimination? $\endgroup$ – Pål GD Mar 14 '13 at 10:54
  • $\begingroup$ @Pal GD: I have no idea how to start, are you talking about the quantifier elimination of $\sigma$ ? How does that help ? $\endgroup$ – pritam Mar 14 '13 at 11:38
  • $\begingroup$ I still don't understand the setup, but apparently that's only me. $\endgroup$ – Raphael Mar 14 '13 at 15:23
  • 1
    $\begingroup$ I disagree with the closed status of the question and with the reason given. In the context of finite model theory (which is one of the tags), the question is perfectly clear. I can understand that somebody not familiar with the concepts of finite model theory might have difficulty making sense of it, but that can be said about any non-beginner question from any specialized field. If the question is reopened, I will be happy to provide an answer. $\endgroup$ – kne Apr 29 '18 at 21:23