Hereditary First-Order Logic: the tractable quantifier prefix classes

TL;DR

This paper characterizes the quantifier prefix classes in first-order logic for which the hereditary model checking problem is polynomial-time solvable, revealing a clear boundary between tractable and coNP-complete cases.

Contribution

It provides a complete classification of quantifier prefixes in first-order logic that determine the computational complexity of hereditary model checking problems.

Findings

Hereditary model checking is in P for prefixes of the form ∀*∃∗ or ∀*∃∀*

For other prefixes containing ∃∃∀ or ∃∀∃, the problem is coNP-complete

Deciding whether Her(φ) is in P is NP-hard unless P=NP

Abstract

Many computational problems can be modelled as the class of all finite structures $\mathbb A$ that satisfy a fixed first-order sentence $\phi$ hereditarily, i.e., we require that every (induced) substructure of $\mathbb A$ satisfies $\phi$. We call the corresponding computational problem the hereditary model checking problem for $\phi$, and denote it by Her$(\phi)$. We present a complete description of the quantifier prefixes for $\phi$ such that Her$(\phi)$ is in P; we show that for every other quantifier prefix there exists a formula $\phi$ with this prefix such that Her$(\phi)$ is coNP-complete. Specifically, we show that if $Q$ is of the form $\forall^\ast\exists\forall^\ast$ or of the form $\forall^\ast\exists^\ast$, then Her$(\phi)$ can be solved in polynomial time whenever the quantifier prefix of $\phi$ is $Q$. Otherwise, $Q$ contains $\exists \exists \forall$ or $\exists \forall \exists$ as a subword, and in this case, there is a first-order formula $\phi$ whose quantifier prefix is $Q$ and Her$(\phi)$ is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula $\phi$ whether Her$(\phi)$ is in P (unless P$=$NP).