On the relative expressiveness of description logics and predicate logics

It is natural to view concept and role definitions in description logics as expressing monadic and dyadic predicates in predicate calculus. We show that the descriptions built using the constructors usually considered in the DL literature are characterized exactly as the predicates definable by formulas in L double over dot(3), the subset of first-order predicate calculus with monadic and dyadic predicates which allows only three variable symbols, In order to handle ''number bounds'', we allow numeric quantifiers, and for transitive closure of roles we use infinitary disjunction. Using previous results in the literature concerning languages with limited numbers of variables, we get as corollaries the existence of formulas of FOPC which cannot be expressed as descriptions. We also show that by omitting role composition, descriptions express exactly the formulas in L double over dot(2), which is known to be decidable.