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.

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.