On fragments of higher order logics that on finite structures collapse to second order

Abstract

We define new fragments of higher-order logics of order three and above, and investigate their expressive power over finite models. The key unifying property of these fragments is that they all admit inexpensive algorithmic translations of their formulae to equivalent second-order logic formulae. That is, within these fragments we can make use of third-and higher-order quantification without paying the extremely high complexity price associated with them. Although theoretical in nature, the results reported here are more significant from a practical perspective. It turns out that there are many examples of properties of finite models (queries from the perspective of relational databases) which can be simply and elegantly defined by formulae of the higher-order fragments studied in this work. For many of those properties, the equivalent second-order formulae can be very complicated and unintuitive. In particular when they concern properties of complex objects, such as hyper-graphs, and the equivalent second-order expressions require the encoding of those objects into plain relations.