The Complexity and Expressive Power of Second-Order Extended Logic
Shiguang Feng, Xishun Zhao
TL;DR
This paper investigates the expressive power of second-order extended Horn logics on all finite structures to understand their relation to PTIME and co-NP. It introduces intermediary formalisms, notably DATALOG$^{*}$, DATALOG$^{r}$, DATALOG$^{*r}$ and stratified versions, and proves a series of collapses and separations among Horn fragments and DATALOG, culminating in SO-HORN$^{r}$ and SO-HORN$^{*r}$ collapsing to FO$(LFP)$ while SO-HORN$^{*}$ remains strictly weaker. It further shows that DATALOG$^{r}$ and S-DATALOG$^{r}$ are equivalent to FO$(LFP)$, whereas DATALOG$^{*}$ is a proper sublogic, and demonstrates that SO-EHORN$^{r}$ is equivalent to $\Pi_{1}^{1}$, thereby capturing co-NP on all finite structures. Collectively, these results clarify the landscape of Horn-like logics, their relation to datalog and FO$(LFP)$, and implications for descriptive complexity in finite-model theory. The findings advance our understanding of which logical frameworks can capture PTIME or co-NP on finite structures, with potential implications for complexity-theoretic characterizations and logical encodings of computational problems.
Abstract
We study the expressive powers of SO-HORN$^{*}$, SO-HORN$^{r}$ and SO-HORN$^{*r}$ on all finite structures. We show that SO-HORN$^{r}$, SO-HORN$^{*r}$, FO(LFP) coincide with each other and SO-HORN$^{*}$ is proper sublogic of SO-HORN$^{r}$. To prove this result, we introduce the notions of DATALOG$^{*}$ program, DATALOG$^{r}$ program and their stratified versions, S-DATALOG$^{*}$ program and S-DATALOG$^{r}$ program. It is shown that, on all structures, DATALOG$^{r}$ and S-DATALOG$^{r}$ are equivalent and DATALOG$^{*}$ is a proper sublogic of DATALOG$^{r}$. SO-HORN$^{*}$ and SO-HORN$^{r}$ can be treated as the negations of DATALOG$^{*}$ and DATALOG$^{r}$, respectively. We also show that SO-EHORN$^{r}$ logic which is an extended version of SO-HORN captures co-NP on all finite structures.