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?
$\begingroup$
$\endgroup$
4
asked Feb 20, 2019 at 10:15
-
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řábekCommented Feb 20, 2019 at 11:59
-
3$\begingroup$ I'm voting to close this question as it was previously answered. $\endgroup$– Pace NielsenCommented Feb 20, 2019 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 KruckmanCommented Feb 20, 2019 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 ReddmannCommented Feb 21, 2019 at 11:12
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
