On the Computational Power of Extensional ESO

TL;DR

Extensional ESO sits between NP-expressiveness and finer logical fragments, and its computational power is shown to be exactly captured by hereditary first-order logic (HerFO). The paper further characterizes monotone extensional SNP as CSPs for finitely bounded structures, and demonstrates that extensional ESO can express natural NP-intermediate problems such as Graph Isomorphism and Monotone Dualization (up to polynomial-time equivalence). It proves that extensional ESO is not NP-rich unless E = NE, and argues for a rich, nuanced landscape where tractability meta-problems are undecidable and NP-intermediate behavior is plausible. The work thus maps a broad portion of the logic-to-complexity landscape, offering both concrete correspondences and guiding conjectures about NP-intermediate phenomena and open problems in descriptive complexity.

Abstract

Extensional ESO is a fragment of existential second-order logic (ESO) that captures the following family of problems. Given a fixed ESO sentence $Ψ$ and an input structure $\mathbb A$ the task if to decide whether there is an extension $\mathbb B$ of $\mathbb A$ that satisfies the first-order part of $Ψ$, i.e., a structure $\mathbb B$ such that $R^{\mathbb A}\subseteq R^{\mathbb B}$ for every existentially quantified predicate $R$ of $Ψ$, and $R^{\mathbb A} = R^{\mathbb B}$ for every non-quantified predicate $R$ of $Ψ$. In particular, extensional ESO describes all pre-coloured finite-domain constraint satisfaction problems (CSPs). In this paper we study the computational power of extensional ESO; we ask, for which problems in NP is there a polynomial-time equivalent problem in extensional ESO?. One of our main results states that extensional ESO has the same computational power as hereditary first-order logic. We also characterize the computational power of the fragment of extensional ESO with monotone universal first-order part in terms of finitely bounded CSPs. These results suggest a rich computational power of this logic, and we conjecture that extensional ESO captures NP-intermediate problems. We further support this conjecture by showing that extensional ESO can express current candidate NP-intermediate problems such as Graph Isomorphism, and Monotone Dualization (up to polynomial-time equivalence). On the other hand, another main result proves that extensional ESO does not have the full computational power of NP: there are problems in NP that are not polynomial-time equivalent to a problem in extensional ESP (unless E=NE).

Figures (2)

• Figure 1: Classes of computational problems studied in this paper. Solid arcs indicate inclusions, and a dashed arc from $A$ to $B$ indicates that every problem in $A$ is polynomial-time equivalent to a problem in $B$ --- for a cleaner picture we omit the solid arc from extensional EMSO to EMSO. GI stands for the Graph Isomorphism problem, and MD for the Monotone Dualization problem.
• Figure 2: Let $R$ be a binary and $U'$ be a unary relation symbol. Consider an extensional ESO $\{R,U'\}$-formula $\Phi$ of the form $\exists U \forall x ((U'(x) \Rightarrow U(x)) \land \phi)$ where $\phi$ is a first-order $\{R,U\}$-formula. On the left, we depict an $\{R,U'\}$-structure where the interpretation of $U'$ is indicated by black vertices, and the interpretation of $R$ is indicated by undirected edges. On the right, we depict the structure $\mathbb B$ with signature $\{R, D, E, <, S_U\}$, where $D^{\mathbb B}$ is indicated by the vertices inside the rectangle, $E^{\mathbb B}$ is indicated by bended dashed directed edges, $<^{\mathbb B}$ is the strict left-to-right linear order on $A \times \{0\}$, and the interpretation of $S_U$ is indicated by straight dotted arcs. Notice that every substructure $\mathbb B'$ of $\mathbb B$ either does not contain a directed $E$-cycle, or it encodes an expansion of $\mathbb A$ by a unary predicate $U$ where $U(x)$ if and only if $\mathbb B'\models\lnot \exists y. S_U(x,y)$. Moreover, this expansion satisfies the clause $\forall x (U'(x) \Rightarrow U(x))$. We use these facts in the proof of Theorem \ref{['thm:extESO->HerFO']}.

Theorems & Definitions (48)

• Example 1: Acyclic digraphs
• Example 2: Pre-coloured 3-colourability
• Theorem 2.1: Corollary 1.4.12 in Book
• Example 3: $k$-colouring problem
• Lemma 4.2
• proof
• Corollary 4.3
• Corollary 4.4
• Theorem 4.5
• proof