Hereditary First-Order Logic: the tractable quantifier prefix classes

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 ${\mathrm{\forall }}^{\ast }\mathrm{\exists }{\mathrm{\forall }}^{\ast }$ or of the form ${\mathrm{\forall }}^{\ast }{\mathrm{\exists }}^{\ast }$, then Her$(\phi )$ can be solved in polynomial time whenever the quantifier prefix of $\phi$ is $Q$. Otherwise, $Q$ contains $\mathrm{\exists }\mathrm{\exists }\mathrm{\forall }$ or $\mathrm{\exists }\mathrm{\forall }\mathrm{\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).