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

F. Ferrarotti, S. González Cornejo, J. Turull-Torres. On fragments of higher order logics that on finite structures collapse to second order. volume 10388, pages 125-139, DOI 10.1007/978-3-662-55386-2_9, 7, 2017.

  • Flavio Ferrarotti
  • Senén André González Cornejo
  • José María Turull-Torres
BuchLogic, Language, Information, and Computation - Proc. WoLLIC 2017
TypIn Konferenzband
SerieLecture Notes in Computer Science

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.