Hereditary First-Order Logic: the tractable quantifier prefix classes

Abstract

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