On higher order query languages which on relational databases collapse to second order logic

• Flavio Ferrarotti
• Loredana Tec
• José María Torrull-Torres

In the framework of computable queries in Database Theory, there are many examples of queries to (properties of) relational database instances that can be expressed by simple and elegant third order logic (TO) formulae. In many of those properties the expressive power of TO is not required, but the equivalent second order logic (SO) formulae can be very complicated or unintuitive. From the point of view of the study of highly expressive query languages is then relevant to identify fragments of TO (and, in general, of higher-order logics of order _ 3) which do have an SO equivalent formula. In this article we investigate this precise problem as follows. Firstly, we define a general schema of 9TO formulae which consists of existentially quantifying a third order linear digraph of polynomial length, that is, a sequence of structures that represents a computation, by explicitly stating which operations are the ones which can be involved in the construction of a given structure in the sequence, when applied to the previous one. Then we give a constructive proof of the fact that all 9TO sub formulae of that schema can be translated into an equivalent SO formula. We give several examples which show that this is a very usual, intuitive, and convenient schema in the expression of properties. Secondly, aiming to formally characterize the fragment of TO which can be translated to SO, we define a restriction of TO, which we denote TOP , for polynomial TO, and we give a constructive proof on the fact that it collapses to SO. We define TOP as the fragment of TO where valuations can assign to TO relation variables only TO relations whose cardinalities are bounded by a polynomial that depends on the quantifier. Moreover, we define a similar restriction for every higher order logic of order i _ 4 (HOi), which we denote HOi,P , for polynomial HOi, and we give a constructive proof on the fact that for all i _ 4, HOi,P collapses to SO.