12
$\begingroup$

I know that the question "does a first order formula $\phi$ have a model" is undecidable in general.

Could anyone give me a link or a book which give the answer for finite models. If I have a first order formula $\phi$, is it decidable whether $\phi$ has a finite model? I am pretty sure that the question is well known, but I do not even know where to begin the search for an answer. (For example, I would have expected it to be in Libkin's "Elements of finite model theory", but it seems that I can not find it.)

The second part of my question is: Are there known restrictions such that the problem is decidable?

For example, the problem may become decidable for first-order formula with only monadic predicates. Or when we have monadic predicate plus a successor relation. But I cannot imagine an algorithm to decide if there exists a (finite) model over those restrictions.

Improve this question
$\endgroup$
6
  • $\begingroup$ Have you read any books on Finite Model Theory? $\endgroup$
    – Dave Clarke
    Apr 13, 2011 at 16:11
  • $\begingroup$ @Dave Clarke: Libkin's book "Element of finite model theory" and Immerman's "Descriptive complexity" $\endgroup$
    – Arthur MILCHIOR
    Apr 13, 2011 at 16:17
  • $\begingroup$ Are you searching for Trakhtenbrot's theorem? For the second part, one simple example is that MSO over words, denoting regular languages, can be checked for satisfiability, as the word structure is itself something one can describe in MSO. $\endgroup$
    – Michaël Cadilhac
    Apr 13, 2011 at 16:25
  • $\begingroup$ Merci Michaël. It seems that it indeed answers the first part of my question. But I'm still searching what is known about restrictions. $\endgroup$
    – Arthur MILCHIOR
    Apr 13, 2011 at 17:11
  • 1
    $\begingroup$ @Michaël Cadilhac - Why not post an answer? Trakhtenbrot's theorem is covered in Libkin's book in Chapter 9. $\endgroup$
    – Marc Hamann
    Apr 13, 2011 at 17:14

4 Answers 4

Reset to default
15
$\begingroup$

The first part of your question is answered by Trakhtenbrot's Theorem. The second part is quite a large question indeed. Depending on the relational structure you're working on, multiple solutions can be given. For instance, if you're interested in formal languages, MSO over word structures corresponds to regular languages, and the matching logic (see this) corresponds to CFL, and thus have their satisfiability problem decidable.

You should have a look at Chapter 14 of Libkin, where nice segments of FO are proven to have a decidable satisfiability problem, according to the amount of quantifier alternations allowed.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ As Michaël says, a large part of computational logic seems devoted to finding and studying fragments where the associated problems are decidable (or tractable). Just to mention one nice survey: Gottlob, Kolaitis, Schwentick, Existential second-order logic over graphs: Charting the tractability frontier, JACM 2004, dx.doi.org/10.1145/972639.972646 $\endgroup$
    – András Salamon
    Apr 13, 2011 at 20:59
  • $\begingroup$ Thank you for your answer. For the question I was thinking about, it is known to be equal to MSO but over nested words. Hence, if the proof of the decidability of MSO over words use the proof of decidability of emtpyness of CFL it doesn't really help me. And thanks for the "matching logic" I didn't know this, but it looks a lot like nested words, hence may interest me. $\endgroup$
    – Arthur MILCHIOR
    Apr 15, 2011 at 22:36
5
$\begingroup$

I do not know the answer for arbitrary FO fragments. Classical modal logic and its extensions have several decidability properties. By the standard translations, you get fragments of classical logic that share these properties.

  1. Modal Logic and the bisimulation invariant fragment of two-variable FOL.
  2. CTL* and the bisimulation invariant fragment of monadic path logic.
  3. The mu-calculus and the bisimulation invariant fragment of Monadic Second Order logic.

All the modal logics above are decidable and have the finite model property. Other logics with robust decidability properties are the guarded fragment of FO, the loosely guarded fragment and guarded fixed point logics. These logics were designed to transfer the essence of well behaved properties of modal logics to a classical logic setting. Guarded fixed point logic is decidable but does not have the finite model property.

Improve this answer
$\endgroup$
2
$\begingroup$

What follows should not be taken as any magisterial textbook truth but merely suggestions for your own further research. Editors are welcome to make corrections as they see fit.

First, your question is apparently of interest to the Automated Deduction community. William McCune has a program called Mace4 which searches for finite models. You might want to read the documentation that describes how it's done.

As for specific decidable restrictions, you may want to look at the following:

  1. Cases where the Herbrand Universe is finite. One mechanical way of checking for a subset of these cases is to check whether the formula has any function symbols. If it doesn't, the Herbrand Universe is finite.

  2. Cases where Quantifier Elimination is possible: theory.stanford.edu/~tingz/talks/qe.ps

Improve this answer
$\endgroup$
1
$\begingroup$

In addition to the answers which were already given: a very good reference about the (un)decidability of fragments of first-order logic is the book The classical decision problem by Börger, Grädel, and Gurevich

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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