On fragments of third order logic that on finite structures collapse to second order logic

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

In the framework of computable queries in Finite Model Theory, there are many examples of properties (queries) 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. In this article we start a research line in the direction of finding ways to isolate the fragments of TO (and, in general, HOi, for i _ 3) formulae which do have an SO equivalent formula. 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.