What is supported in First Order Logics which is not supported in Description Logic?

Question

While studying description logics (DL), it is very common to read that it is a fragment of first order logics (FOL), but it is hard to read something explicitely on what is excluded from DL which is part of FOL, which makes DL (with all its dialects ALC, SHOIN etc...) decidable. Or in another words, could you provide me some examples in FOL which are not expressible through DL (and which are the reason for semi/non-decidability in FOL) ?

Answer 1

The following facts about description logics are closely related to decidability:

1. (a form of) tree-model property — this property is important for tableu methods;
2. embeddability into multimodal systems — which are known to be "robustly decidable";
3. embeddability into the so-called guarded fragments of FOL — see below;
4. embeddability into two-variables FOL fragments — which are decidable;
5. locality — see below.

Some of these facts are syntactical, while some are semantical. Here below are two interesting, decidability-related, and more or less syntactical characteristics of description logics:

Locality (from The Description Logic Handbook, 2nd edition, section 3.6):

One of the main reasons why satisfiability and subsumption in many Description Logics are decidable – although highly complex – is that most of the concept constructors can express only local properties about an element 〈...〉 Intuitively, this implies that a constraint regarding x will not “talk about” elements which are arbitrarily far (w.r.t. role links) from x. This also means that in ALC, and in many Description Logics, an assertion on an individual cannot state properties about a whole structure satisfying it. However, not every Description Logic satisfies locality.

Guarded fragment (from The Description Logic Handbook, 2nd edition, section 4.2.3)

Guarded fragments are obtained from first-order logic by allowing the use of quantified variables only if these variables are guarded by appropriate atoms before they are used in the body of a formula. More precisely, quantifiers are restricted to appear only in the form
     ∃y(P(x,y) ∧ Φ(y))         or      ∀y(P(x,y) ⊃ Φ(y))               (First Guarded Fragment)
     ∃y(P(x,y) ∧ Φ(x,y))      or      ∀y(P(x,y) ⊃ Φ(x,y))            (Guarded Fragment)
for atoms P, vectors of variables x and y and (first) guarded fragment formulae Φ with free variables in y and x (resp. in y).

From these points of view, analyze the examples from @JoshuaTaylor's comments:

• ∀x.(C(X) ↔ ∃y.(likes(x,y) ∧ ∃z.(likes(y,z) ∧ likes(z,x))))
• ∀x.(C(x) ↔ ∃z.(favoriteTeacher(x,z) ∧ firstGradeTeacherOf(x,z)))

---

The reasons why DL is preferred to FOL for knowledge representation are not only decidability or computational complexity related. Look at the slide called "FOL as Semantic Web Language?" in this lecture.

Answer 2

As shown by Turing and Church, FOL is undecidable, because there is no algorithm for deciding if a FOL formula is valid. Many description logics are decidable fragments of first-order logic, however, some description logics have more features than FOL, and many spatial, temporal, and fuzzy description logics are undecidable as well.