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.

Work supported by Austrian Science Fund (FWF): [I2420-N31]. Project: Higher-Order Logics and Structures. Initiated during a project sponsored visit of Prof. José María Turull-Torres. The research reported in this paper has been partly supported by the Austrian Ministry for Transport, Innovation and Technology, the Federal Ministry of Science, Research and Economy, and the Province of Upper Austria in the frame of the COMET center SCCH.

1 Introduction

There are many examples of properties of finite models (queries from the perspective of relational databases) that can be defined by simple and elegant sentences of higher-order logics of order three and above. Take for instance the property of a graph of being an n-hypercube graph $\mathbf{Q}_n$, i.e., an undirected graph whose vertices are binary n-tuples and such that two vertices are adjacent iff they differ in exactly one bit. We can build an $(n+1)$-hypercube $\mathbf{Q}_{n+1}$ by simply taking two isomorphic copies of an n-hypercube $\mathbf{Q}_n$ and adding edges between the corresponding vertices. This strategy can be formally expressed by means of a clear and elegant third-order logic sentence which expresses that $\mathbf G$ is an n-hypercube graph for some n iff the following holds:

• There is a sequence $\mathcal S$ of graphs, i.e., a third-order linear digraph whose nodes are undirected (second-order) graphs.

• The sequence $\mathcal S$ starts with a $K_2$-graph and ends with $\mathbf G$.

• For every graph $\mathbf{G}_{ succ }$ and its immediate predecessor $\mathbf{G}_{ pred }$ in the sequence $\mathcal S$, there is a pair of injective functions $f_1, f_2$ from $\mathbf{G}_{ pred }$ to $\mathbf{G}_{ succ }$ such that

  • $f_1$ and $f_2$ induce in $\mathbf{G}_{ succ }$ two isomorphic copies of $\mathbf{G}_{ pred }$,

  • $f_1$ and $f_2$ define a partition in the vertex set of $\mathbf{G}_{ succ }$, and

  • for every edge (x, y) of $\mathbf{G}_{ succ }$, $f^{-1}_1(x) = f^{-1}_2(y)$ or either the edge $(f^{-1}_1(x), f^{-1}_1(y))$ or $(f^{-1}_2(x), f^{-1}_2(y))$ belongs to $\mathbf{G}_{ pred }$.

Yet another example of a property that can be expressed by a simple and elegant third-order sentence is given by the formula-value query, consisting on determining whether a propositional formula $\varphi$ with constants in $\{F,T\}$ evaluates to true. We can express it in third-order logic by writing that there is a sequence of propositional formulae (represented as finite structures) which starts with $\varphi$, ends with the formula T, and such that every formula $\varphi _{ suc }$ in the sequence results from applying to exactly one sub-formula of its immediate predecessor $\varphi _{ pred }$ an operations of conjunction, disjunction, or negation which is “ready” to be evaluated (e.g., the conjunction in “$(T \wedge F)$”), or the elimination of a pair of redundant parenthesis (e.g., the parenthesis in “(T)”).

The high expressive power of third-order logic is not really necessary to characterize hypercube graphs, since they can be recognized in non-deterministic polynomial time (NP) and by Fagin’s theorem [6] existential second-order logic is then powerful enough to define this property. Nevertheless, to define the class of hypercube graphs in second-order logic is certainly more challenging than to define it in third-order logic (see the two strategies for hypercube graphs in [8]). Likewise, we do not really need third-order logic to express the formula-value query, since it is in DLOGSPACE [2].

It is then relevant to distinguish formulae of order three or higher which do have a second-order equivalent formula, from those which (most likely) do not. Beyond the significance of this questions to advance the theory of descriptive complexity, such a development can clearly empower us to write simpler and more intuitive queries, although still formal, by taking advantage of the higher level of expressivity of higher-order logics. Provided that those queries can be translated into formal languages with lower complexity of evaluation, this can be done without paying the extremely high complexity price which is associated to higher-order logics. Note that by the results in [6, 13], existential second-order logic captures NP while existential third-order logic already captures $NTIME (2^{n^{O(1)}})$.

Outline of Contributions. 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.

We start by defining in Sect. 3 a general schema of existential third-order formulae. The schema generalizes the approach described in our previous examples for hypercube graph and formula-value query. It essentially allows us to express an iteration of polynomial length. This iteration is represented by an unfolded sequence of relational structures which can be seen as a computation or derivation. Transitions are then specified by explicitly stating the operations which can be involved in the construction of a given structure in the sequence, when applied to the previous one. As further discussed in Sect. 3, this is a very usual, intuitive, and convenient schema in the expression of properties.

In Sect. 4, we characterize a broader fragment of third-order logic which is no longer restricted to formulae of a fixed schema as in the previous section. We call this fragment $\mathrm {TO}^{P}$, for polynomial third-order, and give a constructive proof of the fact that it collapses to second-order logic. Although the schema of existential third-order formulae proposed in Sect. 3 turned out to be a special case of $\mathrm {TO}^P$, it is still relevant. The translation of the formulae of that schema yields second-order formulae which are more intuitive and clearer than the general translation of $TO ^P$ formulae. Moreover, taking into consideration the examples in this paper, the translation proposed in Sect. 3 always results in second-order formulae which use relation variables of considerable smaller arity than the equivalent, but also more general translation proposed in this section. Since the maximum arity of the relation variables in the second-order formulae is relevant for the complexity of their evaluation (see [13] among others), it makes sense to study specific schemas of third-order formulae with the aim of finding more efficient translations.

In Sect. 5 we generalize the result in Sect. 4 by characterizing, for each order $i \ge 4$, a fragment $\mathrm {HO}^{i,P}$ of the i-th order logic which collapses to second-order. Again this result has interesting practical applications. As an example, consider a multilevel PERT chart such as those commonly used in engineering for planning and scheduling tasks of complex projects. The encoding of higher-order relations of order $\ge 3$ into second-order relations can be exploited as a normal form to store such type of complex multilevel PERT charts into a standard relational database. Under certain conditions, higher-order queries of order $\ge 3$ could then be synthesised into efficient SQL queries over such normalized relational database. Notice that, a related approach with synthesisation to efficient algorithms was already taken in [14].

We conclude the paper in Sect. 6 where we discuss in detail the expressive power of different fragments of the $\mathrm {HO}^{i,P}$ logics and their relationship with known fragments of second-order logic. In particular, adapting Makowsky and Pnueli [16] approach to prove hierarchies of arity and alternation of second-order formulae, we are able to prove interesting strict hierarchies of $\mathrm {HO}^{i,P}$ formulae.

Due to space limitations, in most cases we only present sketches of the proofs. Nevertheless, a technical report with the omitted details in Sects. 3–5 is accessible as a CoRR abstract in [9].

2 Preliminaries

We assume familiarity with the basic concepts of finite model theory [5, 15]. We only consider signatures, or vocabularies, which are purely relational. We use the classical Tarski’s semantics, except that in the context of finite model theory, only finite structures or interpretations are considered. If $\mathbf{A}$ is a structure of vocabulary $\sigma$, we denote its finite domain by $\textit{dom}(\mathbf {A})$ or A. By $\varphi (x_1,\ldots ,x_r)$ we denote a formula of some logic whose free variables are exactly $\{x_1,\ldots ,x_r\}$. We write $\mathbf{A} \, \models \, \varphi (x_1,\ldots ,x_r)[\bar{a}]$ to denote that $\varphi$ is satisfied by the structure $\mathbf{A}$ under all valuations v such that $v(x_i)=a_i$ for $1 \le i \le r$.

With HO$^{i}$ we denote the i-th order logic which extends first-order logic with quantifiers of any order $2 \le j \le i$, which in turn bind j-th order relation variables. In particular, HO$^2$ denotes second-order logic as usually studied in the context of finite model theory [5, 15], and HO$^3$ denotes third-order logic. A third-order relation type of width w is a w-tuple $\tau = (r_1,\ldots , r_{w})$ where $w, r_1,\ldots , r_{w} \ge 1$, and $r_1,\ldots , r_{w}$ are arities of (second-order) relations. For $i \ge 4$, an i-th order relation type of width w is a w-tuple $\tau = (\rho _1,\ldots , \rho _{w})$ where $w \ge 1$ and $\rho _1,\ldots , \rho _{w}$ are $(i - 1)$-th order relation types. A second-order relation is a relation in the usual sense. A third-order relation of type $\tau = (r_1,\ldots , r_{w})$ is a set of tuples of (second-order) relations of arities $r_1,\ldots , r_{w}$, respectively. For $i \ge 4$, an i-th order relation of type $\tau = (\rho _1,\ldots , \rho _{w})$ is a set of tuples of $(i-1)$-th order relations, of types $\rho _1,\ldots , \rho _{w}$, respectively. $A^\tau$ denotes the set of all higher-order relations of type $\tau$ over the domain of individuals A. We use uppercase calligraphic letters $\mathcal {X}^i$, $\mathcal {Y}^i$, $\mathcal {Z}^i$, ...to denote i-th order variables of order $i \ge 3$, uppercase letters $X, Y, Z, \ldots$ to denote second-order variables, and lower case letters $x, y, z, \ldots$ to denote first-order variables. With $\mathcal {X}^{i,\tau }$ we denote an i-th order variable of type $\tau$. If $\mathcal {X}^{i}$ is a third-order variable, we tend to omit the superscript. We sometimes use $X^r$ to denote that X is a second-order variable or arity r. Second-order variables of arity r are valuated with r-ary relations. For $i \ge 3$, i-th order relation variables are valuated with sets of tuples of $(i-1)$-th order relations according to their relation types. Thus, if v is a valuation, $\mathbf A$ is a structure and $\mathcal{X}^{i, \tau }$ is a higher-order variable, then $v (\mathcal{X}^{i, \tau })$ is a i-th order-relation of type $\tau$ in $A^\tau$. Independently of the order and type of the variables, we say that two valuations v and $v'$ are $\mathcal{X}$-equivalent if $v(\mathcal{Y}) = v'(\mathcal{Y})$ for every variable $\mathcal Y$ other than $\mathcal X$. For any $i \ge 3$, we define the notion of satisfaction in HO$^{i}$ by extending the usual notion of satisfaction of second-order logic formula as follows: $\mathbf {A},v \, \models \, \exists \mathcal {X}^{i, (\rho _1,\ldots , \rho _{w})}(\varphi (\mathcal {X}))$, where $\mathcal {X}$ is an i-th order relation variable and $\varphi$ is a well-formed formula, iff there is a i-th order relation $\mathcal {R}$ of type $\tau = (\rho _1,\ldots , \rho _{w})$ in $A^\tau$, such that $\mathbf {A},v^\prime \, \models \, \varphi (\mathcal {X})$ whenever $v^\prime$ is $\mathcal {X}$-equivalent to v and $v^\prime (\mathcal {X})=\mathcal {R}$. Likewise, $\mathbf {A},v \, \models \, \forall \mathcal {X}^{i, (\rho _1,\ldots , \rho _{w})}(\varphi (\mathcal {X}))$ iff for all i-th order relation $\mathcal {R}$ in $A^\tau$, it holds that $\mathbf {A},v^\prime \, \models \, \varphi (\mathcal {X})$ whenever $v^\prime$ is $\mathcal {X}$-equivalent to v and $v^\prime (\mathcal {X})=\mathcal {R}$.

3 A General Schema of Existential Third-Order Formulae

We define next a general schema of $\exists$TO formulae which consists of existentially quantifying a third-order linear digraph of polynomial length (i.e., 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. The schema is as follows:

(1)

where

• $\mathcal {C}$ ranges over third-order relations of type $\bar{s} = (i_1, \ldots , i_s)$, i.e., over sets of s-tuples of relations of arities $i_1, \ldots , i_s \ge 1$.

• $\text {TotalOrder}(\mathcal{C},\mathcal{O})$, $\text {First}(G)$, $\text {Last}(G)$ and $\text {Pred}(G_{ pred },G_{ succ })$ denote fixed second-order formulae which express that $\mathcal {O}$ is a total order over $\mathcal {C}$, G is the first relational structure in $\mathcal {O}$, G is the last relational structure in $\mathcal {O}$, and $G_{ pred }$ is the immediate predecessor of $G_{ succ }$ in $\mathcal {O}$, respectively.

• $\alpha _{\text {First}}(G)$ and $\alpha _{\text {Last}}(G)$ denote arbitrary second-order formulae which define, respectively, the properties that the first and last structure in $\mathcal {O}$ should satisfy.

• $\varphi (G_{ pred }, G_{ succ })$ denotes an arbitrary second-order formula that expresses the transition from $G_{ pred }$ to $G_{ succ }$, i.e., which operations can be used to obtain $G_{ succ }$ from $G_{ pred }$.

This is a very usual, intuitive, and convenient schema in the expression of natural properties of finite models. For a start, it can clearly be used to express the hypercube and formula-value query as described in the introduction. Significant additional examples are provided by the different relationships between pairs of undirected graphs (G, H) that can be defined as orderings of special sorts. Using schema (1) these relationships can be expressed by defining a set of possible operations that can be applied repeatedly to H, until a graph which is isomorphic to G is obtained. In particular, the following relationships fall into this category: (a) $G \le _{ immersion } H$: G is an immersion in H (see [1, 4, 12]); (b) $G \le _{ top } H$: G is topologically embedded or topologically contained in H (see [1, 4, 12]); (c) $G \le _{ minor } H$: G is a minor of H (see [4, 11]); (d) $G \le _{ induced-minor } H$: G is an induced minor of H (see [4]). Interestingly, in all these cases the length of the sequence is at most linear. The operations on graphs needed to define those orderings are: (E) delete an edge, (V) delete a vertex, (C) contract an edge, (T) degree 2 contraction, or subdivision removal, and (L) lift an edge. In particular the set of allowable operations for each of those orderings are: $\{E, V, L\}$ for $\le _{ immersion }$, $\{E, V, C\}$ for $\le _{ minor }$, $\{E, V, T\}$ for $\le _{ top }$, and $\{V, C\}$ for $\le _{ induced-minor }$ (see [4]).

The classical Kuratowski definition of planarity, provides yet another example of a property that can be defined using our schema (1) and also results in a polynomially bounded sequence of structures. By Wagner’s characterization [3]: a graph is planar if and only if it contains neither $K_{5}$ nor $K_{3,3}$ as a minor.

Provided some simple conditions are met, every third-order formula of the schema (1) can be translated into an equivalent second-order formula. Note that the proof of this results directly implies that the translation can be done by means of a simple and inexpensive algorithm.

Theorem 1

Every third-order formulae $\varPsi \equiv \exists \mathcal {C}^{\bar{s}} \mathcal {O}^{\bar{s}\bar{s}} \psi (\mathcal {C},\mathcal {O})$ of the schema (1) can be translated into an equivalent second-order formula $\varPsi '$ whenever the following conditions hold.

• i. The sub formulae $\alpha _{\text {First}}$, $\alpha _{\text {Last}}$ and $\varphi$ of $\varPsi$ are second-order formulae.

• ii. There is a $d \ge 0$ such that for every valuation v with $v(\mathcal {C}) = \mathcal {R}$, if $\mathbf {A}, v \, \models \, \exists \mathcal {O}^{\bar{s}\bar{s}} \psi (\mathcal {C},\mathcal {O})$, then $|\mathcal {R}| \le | dom (\mathbf {A})|^{d}$.

Proof

(Sketch). Let us first consider the case in which $\mathcal C$ is valuated with sets of non-empty graphs. Let t be the degree of a polynomial bounding the size of those graphs. Our strategy consists on encoding $\mathcal C$ as a pair of second-order variables C and $E_C$ of arities $d+t$ and $2(d+t)$, respectively. Notice that every formula that complies with schema (1) stipulates that $\mathcal O$ is a linear order of the graphs in $\mathcal C$ which represents the stages (or steps) of a computation. Consequently the number of stages needed is bounded by $n^d$, where n is the size of the structure. Since in turn each stage has a bound on the number of elements it adds or changes (at most $n^t$), we have to consider a set of $(d+t)$-tuples.

The encoding into second-order is completed by a total relation $R \subseteq ST \times C$, where C is the union of the domains of all the structures in the sequence. Every node in ST represents one stage, and through the forest R defines a subset of nodes, which is the vertex set of a sub graph (not necessarily connected) of the whole graph $(C,E_C)$. We use $C|_{R(\bar{x})}$, ${E_C}|_{R(\bar{x})}$ to denote the restriction of C and $E_C$, respectively, to $R(\bar{x})$, i.e., $C|_{R(\bar{x})}=\{\bar{y} \mid C(\bar{y}) \wedge R(\bar{x},\bar{y})\}$ and $E_C|_{R(\bar{x})}=\{(\bar{v},\bar{w}) \in E_C \mid R(\bar{x},\bar{v}) \wedge R(\bar{x},\bar{w})\}$. The sub graph of $(C,E_C)$ which corresponds to the stage $ST(\bar{x})$ is denoted as $(C|_ {R(\bar{x})},E_C|_{R(\bar{x})})$. In this way, $\varPsi$ can then be translated into an equivalent second-order formula $\varPsi '$ as follows:

(2)

where

• $\text {Linear}(ST,E_{ST})$, $\text {First}(\bar{x})$, $\text {Last}(\bar{x})$ and $\text {Pred}(\bar{x}, \bar{y}))$ denote second-order formulae which express that $(ST,E_{ST})$ is a linear digraph, $\bar{x}$ is the first node in $(ST,E_{ST})$, $\bar{x}$ is the last node in $(ST,E_{ST})$, and $\bar{x}$ is the immediate predecessor of $\bar{y}$ in $(ST,E_{ST})$, respectively.

• $R \subseteq ST \times C$ and $\text {Total}(R)$ are shorthands for $\forall \bar{x} \bar{y} (R(\bar{x}, \bar{y}) \rightarrow (ST(\bar{x}) \wedge C(\bar{y})))$ and $\forall \bar{x} (ST(\bar{x}) \rightarrow \exists \bar{y} (R(\bar{x}, \bar{y})))$, respectively.

• $\hat{\alpha }_{\text {First}}$ and $\hat{\alpha }_{\text {Last}}$ are second-order formulae built from $\alpha _{\text {First}}$ and $\alpha _{\text {Last}}$, respectively, by modifying them to talk about the graph described by $\bar{x}$ through $ST(\bar{x})$, $E_{ST}$ and R.

• $\hat{\varphi }$ is an second-order formula built from $\varphi$ by modifying it to talk about the graphs described by $\bar{x}$ and $\bar{y}$ through $ST(\bar{x})$, $ST(\bar{y})$, $E_{ST}$ and R.

For the case of relations of arbitrary arity, say S of arity $r \ge 1$, we simply need to consider $E_C$ as an r-ary relation (denoted $E^S_C$). Thus $E_{C}^S|_{R(\bar{x})} = \{(\bar{v}_1,\ldots ,\bar{v}_r) \in E^S_{C} :R(\bar{x},\bar{v}_1) \wedge \ldots \wedge R(\bar{x},\bar{v}_r)\}$. If we have a tuple of relations, say $l \ge 1$ relations of arities $r_1,\ldots ,r_l \ge 1$, respectively, then we have to consider similarly $E_{C_1}^{S_1}$,...,$E_{C_l}^{S_l}$.    $\square$

Remark 1

Every property definable by a third-order formula of the schema (1), where $\alpha _{\text {First}}$, $\alpha _{\text {Last}}$ and $\varphi$ are existential second-order formulae and condition (ii) in Theorem 1 also holds, can be checked in NP exactly as it happens for every property definable in existential second-order. It suffices to additionally guess polynomial-sized valuations for the existentially quantified third-order variables. Then, by Fagin’s theorem, we get that every property definable by such kind of third-order formulae can also be defined in existential second-order. Our approach however is fundamentally different. Instead of producing a non deterministic Turing machine, we produce a clear and intuitive second-order formula.

4 TO$^P$: A Restricted Third Order Logic

We define the logic $\mathrm {TO}^P$ as third-order logic restricted to third-order quantification ranging over third-order relations of cardinality bounded by a polynomial in the size of the structure. By contrast, the cardinality of an arbitrary third-order relation $\mathcal {R}$ over a structure $\mathbf {A}$ is exponentially bounded by $2^{| dom (\mathbf {A})|^{O(1)}}$.

Beyond the usual symbols, the alphabet of $\text {TO}^P$ includes a third-order quantifier $\exists ^{P,d}$ and countably many third order variable symbols $\mathcal {X}^{d,\bar{r}}$ for every $d \ge 0$ and third-order type $\bar{r}$. Whenever it is clear from the context, we avoid the superscript d in the $\mathrm {TO}^P$ variables. A valuation in a structure $\mathbf {A}$ assigns to each variable $\mathcal {X}^{d,\bar{r}}$ a third-order relation $\mathcal {R}$ in $A^{\bar{r}}$, such that $|\mathcal {R}|\le | dom (\mathbf {A})|^d$. The quantifier $\exists ^{P,d}$ has the following semantics: $\mathbf {A} \, \models \, \exists ^{P,d} \mathcal {X}^{d,\bar{r}} \varphi (\mathcal {X})$ iff there is TO relation $\mathcal {R}^{\bar{r}}$ of type $\bar{r}$, such that $\mathbf {A} \, \models \, \varphi (\mathcal {X})[\mathcal {R}]$ and $|\mathcal {R}|\le | dom (\mathbf {A})|^d$.

The following result shows that the expressive power of $\mathrm {TO}^P$ collapses to second-order logic. Same as in the previous section, the proof is constructive and directly implies that the translation can be done algorithmically.

Theorem 2

Every $\mathrm {TO}^P$ formula $\alpha$ can be translated into an equivalent second-order formula $\alpha '$.

Proof

(Sketch). Let $\mathbf A$ be a structure and $\mathcal {R}^{(r_1,\ldots ,r_s)}$ be a $\mathrm {TO}^P$ relation of type $(r_1,\ldots ,r_s)$ in $A^{(r_1,\ldots ,r_s)}$ which is bounded by a polynomial of degree $d \ge 0$, i.e., such that $|\mathcal {R}|\le | dom (\mathbf {A})|^d$. Assuming that all relations which appear in the tuples of $\mathcal R$ are non-empty, we can use a second-order relation $R_{\mathcal {R}}^{d+r_1+\ldots +r_s}$ of arity $(d+r_1+\ldots +r_s)$ to encode $\mathcal {R}^{(r_1,\ldots ,r_s)}$. More precisely, we can use d-tuples from $dom (\mathbf {A})^d$ as identifiers of tuples of second-order relations in $\mathcal {R}$, so that whenever a tuple $(a_1,\ldots ,a_d,a_{d+1},\ldots ,a_{d+r_1},\ldots ,$ $a_{d+r_1+\ldots +r_{s-1}+1},\ldots ,a_{d+r_1+\ldots +r_s}) \in R_{\mathcal {R}}$, then there is a tuple in $\mathcal {R}$ which can be identified by $(a_1,\ldots ,a_d)$, which consists of s second-order relations $S_1^{r_1},\ldots ,S_s^{r_s}$, of arities $r_1,\ldots ,r_s$, respectively, such that $(a_{d+1},\ldots ,$ $a_{d+r_1}) \in S_1,\ldots ,(a_{d+r_1+\ldots +r_{s-1}+1},\ldots , a_{d+r_1+\ldots +r_s}) \in S_s$.

The actual translation can be done by structural induction on the $\mathrm {TO}^P$-formula $\alpha$. We present next the two non-trivial cases.

Atomic Formulae. Let $\alpha$ be of the form $\mathcal {X}^{d,(r_1,\ldots ,r_s)}(X_1^{r_1},\ldots ,X_s^{r_s})$, where $s, r_1,\ldots ,r_s \ge 1$ and $\mathcal {X}$ is a $\text {TO}^P$ variable.

Note that there are $2^{s}$ possible patterns of empty and non-empty relations in an s-tuple of second-order relations. We denote by $\omega = (i_1,\ldots ,i_{|\omega |})$ the pattern of empty relations, with $1\le i_1< i_2<\ldots <i_{|\omega |}\le s$ being the indices of the components which are empty. Correspondingly, we denote by $\bar{\omega } = (j_1,\ldots ,j_{|\bar{\omega }|})$ the pattern of non-empty relations. By abuse of notation, we denote as $\{\omega \}$ and $\{\bar{\omega }\}$ the sets of indices in $\omega$ and $\bar{\omega }$, respectively. In particular if $\{\omega \} = \emptyset$ and $\bar{\omega } = (1,\ldots ,s)$, then all the components of the s-tuple of second-order relations are non-empty.

The idea for the translation is to replace $\mathcal X$ with $2^s$ second-order variables, one for each pattern $\omega$ of empty second-order relations. We use $X_{\mathcal {X},e,\omega }$ to denote the second-order variable that encodes those tuples of second-order relations (in the $\mathrm {TO}^P$ relation that valuates $\mathcal {X}$) which follow $\omega$. The arity of the second-order relation $X_{\mathcal {X},e,\omega }$ is $d + r_{j_1} + \cdots + r_{j_{|\omega |}}$ where $\bar{\omega } = (j_1,\ldots ,j_{|\bar{\omega }|})$. In what follows we use ${\bar{f}}_{\bar{\omega }} = \bar{f}_{j_1} \ldots \bar{f}_{j_{|\bar{\omega }|}}$ to denote a tuple of first-order variables formed by the concatenation of the tuples of first-order variables $\bar{f}_{j_1} = (f_{{j_1} 1},\ldots ,f_{{j_1} r_{j_1}})$,..., $\bar{f}_{j_{|\bar{\omega }|}} = (f_{{j_{|\bar{\omega }|}} 1},\ldots ,f_{{j_{|\bar{\omega }|}} r_{j_{|\bar{\omega }|}}})$.

Let $\varOmega = \{\omega \mid \omega = (i_1,\ldots ,i_{|\omega |})\,;\, 1 \le i_1< i_2< \ldots < i_{|\omega |} \le s\,;\, 0\le |\omega | \le s\,;\, \bar{\omega }=(j_1,\ldots ,j_{|\bar{\omega }|})\,;\, \{\bar{\omega }\}\cup \{\omega \}=\{1,\ldots ,s\}\,;\, \{\bar{\omega }\}\cap \{\omega \}=\emptyset \}$. The translation to second-order of $\mathcal {X}^{d,(r_1,\ldots ,r_s)}(X_1^{r_1},\ldots ,X_s^{r_s})$ is as follows:

Existential Case. Let $\alpha$ be of the form $\exists ^{P,d} \mathcal {X}^{d,(r_1,\ldots ,r_s)}(\varphi )$. In the translation we simply replace the existentially quantified $\mathcal X$ by its corresponding $2^s$ second-order variables and state that no d-tuple can be in more than one of the different second-order relations that encode the value of $\mathcal X$. The formula is as follows:

where $\varOmega$ is as before and $\varphi '$ is the second-order formula equivalent to the $\mathrm {TO}^P$ formula $\varphi$, obtained by applying inductively the described translations.    $\square$

5 $\mathrm {HO^{i,P}}$: Restricted Higher Order Logics

We say that a third-order relation $\mathcal {R}$ is downward polynomially bounded by d in a structure $\mathbf {A}$ if $|\mathcal {R}|\le | dom (\mathbf {A})|^d$. Likewise, we say that a relation $\mathcal {R}$ of order $i > 3$ is downward polynomially bounded by d in $\mathbf {A}$ if $|\mathcal {R}|\le | dom (\mathbf {A})|^d$ and further every relation $\mathcal{R}^j_i$ of order $3 \le j < i$ which appears in a tuple of $\mathcal R$ is downward polynomially bounded by d.

For $i = 4$, we define HO$^{4,P}$ as the extension of TO$^{P}$ with quantifiers that range over downward polynomially bounded relations of order 4. More general, for $i \ge 5$ we define HO$^{i,P}$ as the extension of HO$^{i - 1,P}$ with quantifiers that range over downward polynomially bounded relations of order i.

Beyond the symbols in the alphabet of $\mathrm {TO}^P$, the alphabet of HO$^{i, P}$ includes a j-th order quantifier $\exists ^{j, P, d}$ for every $i \ge j \ge 4$, as well as countably many variable symbols $\mathcal {X}^{j, d, \tau }$ for every j-th order type $\tau$. We sometimes avoid the superscripts d and $\tau$ for clarity.

A valuation in a structure $\mathbf {A}$ assigns to each variable $\mathcal {X}^{j, d, \tau }$ a j-th order relation $\mathcal {R}$ in $A^{\tau }$ which is downward polynomially bounded by d. The quantifier $\exists ^{j, P,d}$ has the following semantics: $\mathbf {A} \, \models \, \exists ^{j, P,d} \mathcal {X}^{j, d, \tau } \varphi (\mathcal {X})$ iff there is a j-th order relation $\mathcal {R}$ of type $\tau$, such that $\mathbf {A} \, \models \, \varphi (\mathcal {X})[\mathcal {R}]$ and $\mathcal {R}$ is downward polynomially bounded by d in $\mathbf {A}$.

Same as with $\mathrm {TO}^P$, for every order $i \ge 4$ the expressive power of $\mathrm {HO}^{i,P}$ collapses to second-order logic.

Theorem 3

For every order $i \ge 3$, every $\mathrm {HO}^{i, P}$ formula $\alpha$ can be translated into an equivalent second-order formula $\alpha '$.

The actual proof of this theorem is quite long and cumbersome. Due to space limitations we omit it here. The details can nevertheless be consulted in the technical report in [9]. To gain some intuition on how this translations works, let us consider the case of $HO^{4,P}$. The general idea is to represent the fourth-order relations as a normalized relational database. Assume w.l.o.g. that the type of every relations of order 3 and 4 has width $s \ge 1$, and that every such relation is downward polynomially bounded by $d \ge 1$. In the case of a formula of the form $\mathcal {X}^{4,d,\tau }(\mathcal {Y}_1^3,\ldots ,\mathcal {Y}_s^3)$ of $\mathrm {HO}^{4,P}$ we can represent the fourth-order variable $\mathcal {X}^{4,d,\tau }$ using $2^s$ second-order variables $\mathrm {X}_{{\mathcal {X}^{4},{\omega }_{3,\mathcal {X}}}}$ of arities between d and $d+(s \cdot (d + s))$, depending on the pattern $\omega _{3,\mathcal {X}}$ of non-empty relations. Thus, each $\mathrm {X}_{{\mathcal {X}^{4},{\omega }_{3,\mathcal {X}}}}$ can encode the tuples of (non-empty) third-order relations whose pattern is $\omega _{3,\mathcal {X}}$. In turns, each $\mathcal {Y}^3_j$ can be represented by $2^s$ second-order variables as explained in Sect. 4 for the case of $\mathrm {TO}^P$.

6 Fragments of $\mathrm {HO}^{i,P}$ Formulae

The aim of this section is to gain a better understanding of the syntactic restrictions relevant as to the expressive power of the $\mathrm {HO}^{i,P}$ logics.

In [17] we showed that for any $i \ge 3$ the deterministic inflationary fixed-point quantifier (IFP) in HO$^{i}$ (i.e., where the variable which is bound by the IFP quantifier is an $(i+1)$-th order variable) is expressible in $\exists$HO$^{i+1}$. Let $IFP|_P$ denote the restriction of IFP where there is a positive integer d such that in every structure $\mathbf {A}$, the number of stages of the fixed-point is bounded by $| dom (\mathbf {A})|^d$. And let $(SO + IFP)$ denote second-order logic extended with the deterministic inflationary fixed-point quantifier, where the variable which is bound by the IFP quantifier is a third order variable. Note that the addition of such IFP quantifier to second-order means that we can express iterations of length exponential in $| dom (\mathbf {A})|$, so that it is strongly conjectured that $(SO + IFP)$ strictly includes second-order logic as to expressive power. However, as a consequence of Theorem 2 this is not the case with $IFP|_P$.

Corollary 1

For every formula in $(SO + IFP|_P)$ there is an equivalent second-order formula.

Let us define $\varSigma {TO^P_n}$ as the restriction of $TO^P$ to prenex formulae of the form $Q_1 V_1 \ldots Q_k V_k (\varphi )$ such that:

• $Q_1, \ldots , Q_k \in \{\forall ^{P,d}, \exists ^{P,d}, \forall , \exists \}$.

• $V_i$ for $1 \le i \le k$ is either a second-order or $\mathrm {TO}^P$ variable (depending on $Q_i$).

• $\varphi$ is a $\mathrm {TO}^P$ formula free of $\mathrm {TO}^P$ as well as second-order quantifiers (first-order quantifiers as well as free $\mathrm {TO}^P$ and second-order variables are allowed).

• The prefix $Q_1 V_1 \ldots Q_k V_k$ starts with an existential block of quantifiers and has at most n alternating (between universal and existential) blocks.

By the well known Fagin-Stockmeyer characterization [18] of the polynomial-time hierarchy, for every $n \ge 1$ the prenex fragment $\varSigma _n$ of second-order logic captures the level $\varSigma ^\mathrm {poly}_n$ of the polynomial-time hierarchy. From the proof of Theorem 2 is immediate that every formula in $\varSigma {TO^P_n}$ can be translated into an equivalent second-order formula in $\varSigma _n$.

Corollary 2

$\varSigma {TO^P_n}$ captures $\varSigma ^\mathrm {poly}_n$.

Consider the $AA (r,m)$ classes of second-order logic formulae where all quantifiers of whichever order are grouped together at the beginning of the formula, forming up to m alternating blocks of consecutive existential and universal quantifiers, and such that the arity of the second-order variables is bounded by r. Note that, the order of the quantifiers in the prefix may be mixed. As shown by Makowsky and Pnueli [16], the $AA (r,m)$ classes constitute a strict hierarchy of arity and alternation. Their strategy to prove this result consisted in considering the set $AUTOSAT ( AA (r,m))$ of formulae of $AA (r,m)$ which, encoded as finite structures, satisfy themselves. As the well known diagonalization argument applies, it follows that $AUTOSAT ( AA (r,m))$ is not definable by any formulae of $AA (r,m)$, but it is definable in a higher level of the same hierarchy. Similarly to Makowsky and Pnueli arity and alternation hierarchy of second-order formulae, we can we define hierarchies of $\mathrm {HO}^i$ and $\mathrm {HO}^{i,P}$ formulae as follows.

Definition 1

( $AA ^i$ - and $AAD ^i$ -hierarchies). The maximum-width of a type $\tau = (\rho _1, \ldots , \rho _s)$ of order $i \ge 3$ (denoted as ) is defined as follows:

• if $i = 3$.

• if $i > 3$.

For $r, m, i \ge 1$, we define the level $AA ^i(r,m)$ of the $AA ^i$-hierarchy as the class of formulae $\varphi \in \mathrm {HO}^{i+1}$ of the form $Q_1 V_{1} \ldots Q_k V_{k}(\psi )$ such that:

• i $\psi$ is a quantifier-free $\mathrm {HO}^{i}$-formula.

• ii For $j = 1, \ldots , k$, each $Q_j$ is either an existential or universal quantifier and each $V_j$ is a variable of order $\le i+1$.

• iii The prefix $Q_1 V_{1} \ldots Q_k V_{k}$ has at most m alternating blocks of quantifiers.

• iv If $V_j$ is a second-order variable, then its arity is bounded by r.

• v If $V_j$ is of order $\ge 3$, then the maximum-width of the type $\tau$ of $V_j$ is $\le r$.

For $r, m, i, d \ge 1$, the level $AAD ^i(r,m,d)$ of the $AAD ^i$-hierarchy is obtained by adding the following condition to the definition of $AA ^i(r,m)$.

• If $V_j$ is a variable of order $\ge 3$, then the quantifier $Q_j$ has a superscript $d_j \le d$, which denotes the degree of the polynomial bounding the size of the valuations of $V_j$ (recall definition of $\mathrm {HO}^{i,P}$).

Note that in the formulae of the $AA ^i$ and $AAD ^i$ hierarchies the quantifiers of the highest order do not necessarily precede all the remaining quantifiers in the prefix, as it is the case in the $\varSigma ^i_m$ hierarchies of higher-order logics.

As proven in [7, 10], it is possible to gerenarlize Makowsky and Pnueli result regarding the $AA$-hierarchy [16] to every higher-order logic of order $i \ge 2$.

Theorem 4

(Theorem 4.28 in [7]). For every $i, r, m \ge 1$, there are Boolean queries not expressible in $AA ^i(r,m)$ but expressible in $AA ^i(r+c(r), m+6)$, where $c(r) = 1$ for $r > 1$ and $c(r) = 2$ for $r = 1$.

The proof of the previous result in [7] also follows the strategy introduced in [16]. That is, it uses the diagonalization argument to prove the lower bound for the definability of $AUTOSAT ( AA ^i(r,m))$, and shows a formula in $AA ^i(r+c(r), m+6)$ that defines $AUTOSAT ( AA ^i(r,m))$ to prove the upper bound.

Interestingly, the formula $\psi _A \in AA ^i(r+c(r), m+6)$ used in the proof of Proposition 4.27 in [7] to define $AUTOSAT ( AA ^i(r,m))$ can be straightforwadly translated to a formula $\psi _A^d$ that defines $AUTOSAT ( AAD ^i(r,m,d))$. We simply need to qualify with an appropriate superscript $d_j \le d$ the existential and universal quantifiers associated to each higher-order variable $V_j$ of order $\ge 3$ which appears in $\psi _A$, so that $V_j$ becomes restricted to range over higher-order relations which are downward polynomially bounded by $d_j$. Since d as well as the order and the maximum-width of the higher-order types are bounded, a finite set of variables is still sufficient to encode the valuations for the different variables that might appear in any arbitrary sentence in $AAD ^i(r,m,d)$. The resulting $\psi _A^d$ formula is clearly in $AAD ^i(r+c(r), m+6, d)$. It no longer defines $AUTOSAT ( AA ^i(r,m))$ when $i \ge 2$, since the size of the higher-order relations that interpret the higher-order variables of order $\ge 3$ in $\psi _A^d$ are downward polynomially bounded by d and thus insufficient to encode every possible valuation for variables of order $\ge 3$. This is clearly not a problem if we only consider sentences in $AAD ^i(r,m,d)$. In fact, in this latter case we need higher-order variables that encode only those valuations which are downward polynomially bounded by some positive integer $\le d$.

The previous observation together with the fact that by using the same diagonalization argument we can prove that $AUTOSAT ( AAD ^i(r,m,d))$ is not definable in $AAD ^i(r,m,d)$, gives us the following strict hierarchies of $\mathrm {HO}^{i,P}$ formulae for every order i.

Theorem 5

For every $i \ge 2$ and $r, m, d \ge 1$, there are Boolean queries not expressible in $AAD ^i(r,m,d)$ but expressible in $AAD ^i(r+c(r), m+6, d)$, where $c(r) = 1$ for $r > 1$ and $c(r) = 2$ for $r = 1$.

Lemma 1 is a direct consequence of the translations in Theorems 2 and 3.

Lemma 1

Let $r, m, d \ge 1$ and $i \ge 2$. For every sentence $\varphi$ in $AAD ^i(r,m,d)$, there is an equivalent sentence $\varphi '$ in $AA ^1(r^i+ d \cdot (i-1),m+2)$.

The following result suggest that the exact converse of the previous lemma is unlikely to hold. It further shows the relationship between the levels of the arity and alternation hierarchy of Makowsky and Pnueli and the $AAD^i$ hierarchies.

Lemma 2

Let $r, m \ge 1$. For every second-order sentence $\varphi$ in $AA ^1(r,m)$, there are three sentences $\varphi '$, $\varphi ''$ and $\varphi '''$, each of them equivalent to $\varphi$, such that:

• i. $\varphi ' \in AAD ^{\left\lceil {\frac{r}{2}}\right\rceil + 1}(2,m,2)$.

• ii $\varphi '' \in AAD ^2(2,m,r)$.

• iii $\varphi ''' \in AAD ^2(\left\lceil \root 2 \of {r}\right\rceil ,m,\left\lceil \root 2 \of {r}\right\rceil (\left\lceil \root 2 \of {r}\right\rceil -1))$.

A Sketch of the proof of Lemma 2 is included in Appendix A.

Our final result gives a fine grained picture of the effect, as to expressive power, of simultaneously bounding the arity, alternation and maximum degree of the $\mathrm {HO}^{i,P}$-sentences.

Theorem 6

For every $r, m, d \ge 1$, there are Boolean queries not expressible in $AAD ^2(r,m,d)$ but expressible in $AAD ^{c}(2,m+8,2)$ as well as in $AAD ^2(2,m+8,(r+1)^2+d)$ and in $AAD ^2(q,m+8,q(q-1))$, where $c=\left\lceil {\frac{((r+1)^2+d}{2}}\right\rceil + 1$ and $q = \left\lceil \root 2 \of {((r+1)^2+d)}\right\rceil$.

Proof

By Lemma 1, we get that $AAD ^2(r,m,d) \subseteq AA ^1(r^2 + d,m+2)$, i.e., the class of Boolean queries definable by $TO^P$-sentences in $AAD ^2(r,m,d)$ is included in those definable by second-order sentences in $AA ^1(r^2 + d,m+2)$. In turns, by Makowsky and Pnueli [16] result (first level ($i=1$) in Theorem 4), we get that $AA ^1(r^2 + d,m+2) \subset AA ^1(r^2+d+1, m+8)$. Finally, by Lemma 2 we get that the class of Boolean queries definable in $AA ^1(r^2+d+1, m+8)$ is included in $AAD ^{c}(2,m+8,2)$ as well as in $AAD ^2(2,m+8,(r+1)^2+d)$ and in $AAD ^2(q,m+8,q(q-1))$.    $\square$

Appendix A Proof Sketch of Lemma 2

All three sentences $\varphi '$, $\varphi ''$ and $\varphi '''$ can be defined by structural induction on $\varphi$. We show only the non trivial cases.

If $\varphi$ is an atomic formula of the form $X(x_1, \ldots , x_s)$ where $s \le r$. Then

• $\varphi '$ is $\mathcal {X}^c(\mathcal {X}^{c-1}_1,\mathcal {X}^{c-1}_2) \wedge \mathcal {X}^{c-1}_1(\mathcal {X}^{c-2}_1) \wedge \mathcal {X}^{c-1}_2(\mathcal {X}^{c-2}_2,\mathcal {X}^{c-2}_3) \wedge \cdots \wedge$

        $\mathcal {X}^{3}_1(X_1) \wedge \mathcal {X}^{3}_2(X_2) \wedge \cdots \wedge \mathcal {X}^{3}_{c-2}(X_{c-2},X_{c-1}) \wedge$

        $X_{c-1}(x_{s-1},x_{s}) \wedge X_{c-2}(x_{s-3},x_{s-2}) \wedge \cdots \wedge X_1(\bar{x})$, where $\bar{x} = (x_1)$ or $\bar{x} = (x_1, x_2)$ depending on whether s is odd or even, respectively, and $c=\left\lceil {\frac{r}{2}}\right\rceil + 1$.

• $\varphi ''$ is $\bigwedge \limits _{\bar{w} \in W} \Big ( \big ( \bigwedge \limits _{1\le j < l \le s} \alpha _{i,j} \big ) \rightarrow \psi _{\bar{w}} \Big ),$ where

  • $W = \{(i_1,i_2,\cdots ,i_s)\mid 1\le j \le s \; \text {and} \; 1\le i_j \le j \}$

  • $\alpha _{i,j} =\{\begin{array}{c} x_i=x_j \;\textit{if}\; i=j \\ x_i\not =x_j \;\textit{if}\; i\not =j \end{array}$

  • $\psi _{\bar{w}}$ is $X_{1_{\bar{w}}}(x_1,x_1)$ if $i_u = i_v$ for every $i_u, i_v \in \bar{w}$.

    Otherwise $\psi _{\bar{w}}$ is $\bigwedge \limits _{(u,v) \in A_{\bar{w}}} X_{1_{\bar{w}}}(x_u,x_v)$, where

    .

• $\varphi '''$ is $\mathcal {X}(X_1,\cdots ,X_t) \bigwedge \limits _{1\le i\le t-1} X_i(x_{k_i+1},\cdots ,x_{k_i+u}) \wedge X_t(x_{s-t},\cdots ,x_s)$

  Where $t=\left\lceil \root 2 \of {r}\right\rceil$, $k_i=((i-1)t)\,+\,min((i-1), (s-t) \mod (t-1))$, $u=|\frac{s-t}{t-1}|+c$, and $c=1$ if $i\le (s-t) \mod (t-1)$, $c=0$ otherwise.

If $\varphi$ is a formula of the form $\exists X (\psi )$ where X is a second-order variable of arity $s \le r$. Then

• ,

  where again $c=\left\lceil {\frac{s}{2}}\right\rceil + 1$, and $\psi '$ is the formula in $AAD ^c(2,m,2)$ equivalent to $\psi$, obtained by applying the translation inductively.

• $\varphi ''$ is $\exists ^{P,s} \mathcal {X}_{\bar{w}_1} \mathcal {X}_{\bar{w}_2} \cdots \mathcal {X}_{\bar{w}_{\left| W\right| }} \exists X_{1_{\bar{w}_1}} X_{2_{\bar{w}_1}} X_{1_{\bar{w}_2}} X_{2_{\bar{w}_2}} \cdots X_{1_{\bar{w}_{\left| W\right| }}} X_{2_{\bar{w}_{\left| W\right| }}} (\psi '')$,

  where $\bar{w}_1,\bar{w}_2,\cdots ,\bar{w}_{\left| W\right| }$ is an arbitrary lexicographic order of W and $\psi ''$ is the formula in $AAD ^2(2,m,s)$ equivalent to $\psi$, obtained by applying the translation inductively.

• $\varphi '''$ is $\exists ^{P,h} \mathcal {X} \exists X_1 X_2 \cdots X_t(\psi ''')$ where $t =\left\lceil \root 2 \of {s}\right\rceil$, $h = t(t-1)$ and $\psi '''$ is the formula in $AAD ^2(t,m,t(t-1))$ equivalent to $\psi$, obtained by applying the translation inductively.

It is not difficult to show by structural induction that $\varphi '$, $\varphi ''$ and $\varphi '''$ are equivalent to $\varphi$. We only need to see that every second-order relation of arity $s \le r$ can be encoded as a higher-order relation of the type used in the translation and with the required polynomial bound.