Forbidden Induced Subgraphs and the Los-Tarski Theorem

Let C be a class of finite and infinite graphs that is closed under induced subgraphs. The well-known Los-Tarski Theorem from classical model theory implies that C is definable in first-order logic (FO) by a sentence ' if and only if C has a finite set of forbidden induced finite subgraphs. It provides a powerful tool to show nontrivial characterizations of graphs of small vertex cover, of bounded tree-depth, of bounded shrubdepth, etc. in terms of forbidden induced finite subgraphs. Furthermore, by the Completeness Theorem, we can compute from (sic) the corresponding forbidden induced subgraphs. Our results (a) and (b) show that this machinery fails on finite graphs. (a) There is a class of finite graphs that is definable in FO and closed under induced subgraphs but has no finite set of forbidden induced subgraphs. (b) Even if we only consider classes C of finite graphs that can be characterized by a finite set of forbidden induced subgraphs such a characterization cannot be computed from an FO-sentence (sic) that defines C and the size of the characterization cannot be bounded by f(|(sic)|) for any computable function f. Besides their importance in graph theory, our results also significantly strengthen similar known theorems for arbitrary structures.