  The elimination distance to some target graph property P is a general graph
modification parameter introduced by Bulian and Dawar. We initiate the study of
elimination distances to graph properties expressible in first-order logic. We
delimit the problem's fixed-parameter tractability by identifying sufficient
and necessary conditions on the structure of prefixes of first-order logic
formulas. Our main result is the following meta-theorem: for every graph
property P expressible by a first order-logic formula \phi\in \Sigma_3, that
is, of the form \phi=\exists x_1\exists x_2\cdots \exists x_r \forall
y_1\forall y_2\cdots \forall y_s \exists z_1\exists z_2\cdots \exists z_t \psi,
where \psi is a quantifier-free first-order formula, checking whether the
elimination distance of a graph to P does not exceed k, is fixed-parameter
tractable parameterized by k. Properties of graphs expressible by formulas from
\Sigma_3 include being of bounded degree, excluding a forbidden subgraph, or
containing a bounded dominating set. We complement this theorem by showing that
such a general statement does not hold for formulas with even slightly more
expressive prefix structure: there are formulas \phi\in \Pi_3, for which
computing elimination distance is W[2]-hard.
