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, 2013 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, 2013 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, 2013 at 11:38
  • $\begingroup$ I still don't understand the setup, but apparently that's only me. $\endgroup$
    – Raphael
    Mar 14, 2013 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, 2018 at 21:23