Just curious: This monday, I had an exam in Knowledge Processing. They asked what's the problem with FOL (compared to propositional), and I gave the textbook answer that iterating functions gives infinitely many ground terms and makes it undecidable. And since I'm a bigmouth, lavedida, I added that I strongly suspect throwing just that feature out won't suffice. (Cf. e.g. planners like STRIPS, which are far weaker than FOL.)
We simply let that one go since it was irrelevant for the exam (and neither of us had the math knowledge) but I still want to know: Can you restrict FOL so that you still have quantors (which are the whole point) but the resulting axiom system is decidable?


closed as off-topic by Andrej Bauer, Pace Nielsen, YCor, Piotr Hajlasz, Joseph Van Name Feb 25 at 13:14

  • This question does not appear to be about research level mathematics within the scope defined in the help center.
If this question can be reworded to fit the rules in the help center, please edit the question.

  • 5
    $\begingroup$ Various restrictions on the signature and/or on the quantifier prefix that guarantee decidability are mentioned in the question mathoverflow.net/questions/83399/… and in my answer there. $\endgroup$ – Emil Jeřábek Feb 20 at 11:59
  • 3
    $\begingroup$ I'm voting to close this question as it was previously answered. $\endgroup$ – Pace Nielsen Feb 20 at 16:19
  • 1
    $\begingroup$ As the answer and Emil's link show, the fact that there are infinitely many ground terms has nothing to do with undecidability. Indeed, first-order logic is undecidable in a signature with a single binary relation and no function symbols (so there are no terms other than the variables). While on the other hand, first-order logic is decidable in a signature with a single unary function symbol and a single constant symbol (where there are infinitely many ground terms: $c$, $f(c)$, $f(f(c))$, $\dots$). $\endgroup$ – Alex Kruckman Feb 20 at 19:51
  • $\begingroup$ Ha. I knew there was something fishy with the "standard" answer...(And feel free to close, I have my answer.) $\endgroup$ – Hauke Reddmann Feb 21 at 11:12

There are various decidable fragments of FOL. Beyond prefix classes which Emil Jeřábek mentioned, other common fragments are:

  • Two variable logics. The fragment of FOL in which only two variables x and y are allowed is decidable. There are extensions of this logic which are decidable, e.g. with counting quantifiers $\exists ^{\leq 5} x$. Note that allowing even three variables leads to undecidability.

  • Guarded logics. Here all quantification is guarded by a predicate from the signature, e.g. $\forall x,y,z\, (R(x,y,z) \to S(z,z,y,x))$. This remains true with various extensions including that go beyond FOL such as fixed point logic.

If you want to know more, have a look at: Decidable Fragments of First-Order and Fixed-Point Logic - From prefix vocabulary classes to guarded logics (2003) by Erich Grädel. I believe it is unpublished, but you can google a manuscript and slides.


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