Tree-depth, quantifier elimination, and quantifier rank
Yijia Chen, Jörg Flum · 2018
For a class K of finite graphs we consider the following three statements. (i) K has bounded tree-depth. (ii) First-order logic FO has an effective generalized quantifier elimination on K. (iii) The parameterized model checking for FO on K is in para-AC0. We prove that (i) ⟹ (ii) and (ii) ⟺ (iii). All three statements are equivalent if K is closed under taking subgraphs, but not in general.