<p>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. </p>

<ol>
<li>Modal Logic and the bisimulation invariant fragment of two-variable FOL.</li>
<li>CTL* and the bisimulation invariant fragment of monadic path logic.</li>
<li>The mu-calculus and the bisimulation invariant fragment of Monadic Second Order logic. </li>
</ol>

<p>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. </p>

CC BY-SA 3.0
2011-04-13T16:42:04.443Z
2011-04-13T16:42:04.443Z
Vijay D
<p>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.</p>

<p>First, your question is apparently of interest to the Automated Deduction community. William McCune has a program called <a href="http://www.cs.unm.edu/~mccune/prover9/" rel="nofollow">Mace4</a> which searches for finite models. You might want to read the documentation that describes how it's done.</p>

<p>As for specific decidable restrictions, you may want to look at the following:</p>

<ol>
<li><p>Cases where the <a href="http://mathworld.wolfram.com/HerbrandUniverse.html" rel="nofollow">Herbrand Universe</a> 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.</p></li>
<li><p>Cases where <a href="http://mathworld.wolfram.com/QuantifierElimination.html" rel="nofollow">Quantifier Elimination</a> is possible: theory.stanford.edu/~tingz/talks/qe.ps</p></li>
</ol>

CC BY-SA 3.0
2011-05-17T21:09:31.800Z
2011-05-17T21:09:31.800Z
ShyPerson
<p>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 <a href="http://www.springer.com/us/book/9783540423249" rel="nofollow">The classical decision problem</a> by Börger, Grädel, and Gurevich</p>

CC BY-SA 3.0
2016-07-01T05:51:45.320Z
2016-07-01T06:28:17.113Z
2016-07-01T06:28:17.113Z
f-h
<p>The first part of your question is answered by <a href="http://en.wikipedia.org/wiki/Trakhtenbrot%27s_theorem">Trakhtenbrot's Theorem</a>.
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 (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.376">see this</a>) corresponds to CFL, and thus have their satisfiability problem decidable.</p>

<p>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.</p>

CC BY-SA 3.0
2011-04-13T20:59:24.887Z
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, http://dx.doi.org/10.1145/972639.972646
András Salamon
CC BY-SA 3.0
2011-04-15T22:36:47.783Z
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.
Arthur MILCHIOR
CC BY-SA 3.0
2011-04-13T17:47:47.210Z
2011-04-14T04:09:35.580Z
2011-04-14T04:09:35.580Z
Michaël Cadilhac
<p>I know that the question "does a first order formula $\phi$ have a model" is undecidable in general. </p>

<p>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.)</p>

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

<p>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.</p>

CC BY-SA 3.0
2011-04-13T16:11:51.990Z
Have you read any books on Finite Model Theory?
Dave Clarke
CC BY-SA 3.0
2011-04-13T16:17:40.377Z
@Dave Clarke: Libkin's book "Element of finite model theory" and Immerman's "Descriptive complexity"
Arthur MILCHIOR
CC BY-SA 3.0
2011-04-13T16:25:40.213Z
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.
Michaël Cadilhac
CC BY-SA 3.0
2011-04-13T17:11:58.567Z
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.
Arthur MILCHIOR
CC BY-SA 3.0
2011-04-13T17:14:18.293Z
@Michaël Cadilhac - Why not post an answer?  Trakhtenbrot's theorem is covered in Libkin's book in Chapter 9.
Marc Hamann
CC BY-SA 3.0
2011-04-13T17:48:55.663Z
@Marc Hamann: Well, I didn't have quite a satisfying answer for part 2.  I posted something nontheless. :)
Michaël Cadilhac
<reference-request><lo.logic><computability><finite-model-theory>
Finding a finite model
Arthur MILCHIOR
# Finding a finite model

(Asked by: username_0 on 2011-04-13)

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.

**Tags:** reference-request, lo.logic, computability, finite-model-theory

> **Comments:**
> **username_1**: Have you read any books on Finite Model Theory?  
> **username_0**: @username_1: Libkin's book "Element of finite model theory" and Immerman's "Descriptive complexity"  
> **username_2**: 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.  
> **username_0**: 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.  
> **username_3**: @username_2 - Why not post an answer?  Trakhtenbrot's theorem is covered in Libkin's book in Chapter 9.  
> **username_2**: @username_3: Well, I didn't have quite a satisfying answer for part 2.  I posted something nontheless. :)  

---

## 4 answers

### Answer by username_2 on 2011-04-13. Score: 15 | Accepted answer

The first part of your question is answered by [Trakhtenbrot's Theorem](http://en.wikipedia.org/wiki/Trakhtenbrot%27s_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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.376)) 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.

> **Comments:**
> **username_7**: 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, http://dx.doi.org/10.1145/972639.972646  
> **username_0**: 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.  

---

### Answer by username_4 on 2011-04-13. Score: 5

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.


---

### Answer by username_5 on 2011-05-17. Score: 2

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](http://www.cs.unm.edu/~mccune/prover9/) 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](http://mathworld.wolfram.com/HerbrandUniverse.html) 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](http://mathworld.wolfram.com/QuantifierElimination.html) is possible: theory.stanford.edu/~tingz/talks/qe.ps


---

### Answer by username_6 on 2016-07-01. Score: 1

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](http://www.springer.com/us/book/9783540423249) by Börger, Grädel, and Gurevich


---

