We consider the model-checking problem for first-order logic, that is, the problem to decide for a given graph $G$ and first-order formula $\varphi$ whether $G\models \varphi$.

Much work has gone into identifying classes $\mathcal{C}$ of graphs on which this problem becomes fixed-parameter tractable, i.e. can be solved in time $f(|\varphi|)\cdot n^c$ for some constant $c$ and computable function $f : \N \rightarrow \N$.

It is known that if $\mathcal{C}$ has locally bounded expansion, then the problem is indeed fixed-parameter tractable on $\mathcal{C}$.

In this note we show that if $\mathcal C$ is not nowhere dense and in addition is closed under taking sub-graphs and
satisfies some effectivity conditions then FO-model
checking is not FPT on $\mathcal C$ unless FPT = AW[*].

It is still an open problem whether first-order model-checking is fixed-parameter tractable on classes of graphs which are nowhere dense, leaving a gap between our lower bound and the best currently known upper bounds.

We show that if $\mathcal C$ is a class of graphs which is
"nowhere dense" then first-order model-checking is
fixed-parameter tractable on $\mathcal C$. As all graph classes which exclude a fixed minor, or are of bounded local tree-width or locally exclude a minor are nowhere dense, this generalises algorithmic meta-theorems obtained for these classes in the past
(see \cite{FlumGro01,FrickGro01,DawarGroKre07}).

Conversely, if $\mathcal C$ is not nowhere dense and in addition is closed under taking sub-graphs and
satisfies some effectivity conditions then FO-model
checking is not FPT on $\mathcal C$ unless FPT = AW[*].

Hence, for classes of graphs closed under sub-graphs, this essentially gives a precise characterisation of classes for which FO model-checking is tractable.

However, our result generalises to much more general classes of graphs. In particular we show that every class which can efficiently be coloured "over a class with the type representation property" allows tractable first-order model-checking. Such classes include all classes which are nowhere dense and also all classes of bounded clique-width. This result therefore unifies all known meta-theorems for first-order logic.

We show that if $\mathcal C$ is a class of graphs which is
"nowhere dense" then first-order model-checking is
fixed-parameter tractable on $\mathcal C$. As all graph classes which exclude a fixed minor, or are of bounded local tree-width or locally exclude a minor are nowhere dense, this generalises algorithmic meta-theorems obtained for these classes in the past
(see \cite{FlumGro01,FrickGro01,DawarGroKre07}).

Conversely, if $\mathcal C$ is not nowhere dense and in addition is closed under taking sub-graphs and
satisfies some effectivity conditions then FO-model
checking is not FPT on $\mathcal C$ unless FPT = AW[*].

Hence, for classes of graphs closed under sub-graphs, this essentially gives a precise characterisation of classes for which FO model-checking is tractable.

However, our result generalises to much more general classes of graphs. In particular we show that every class which can efficiently be coloured "over a class with the type representation property" allows tractable first-order model-checking. Such classes include all classes which are nowhere dense and also all classes of bounded clique-width. This result therefore unifies all known meta-theorems for first-order logic.