Destructive Rule-Based Properties and First-Order Logic

We study properties characterized by applying successively a "destructive" rule expressed in first-order logic. The rule says that Points, a(1),...,a(k) of a structure can be removed if they satisfy a certain first-order formula. phi(a(1),...,a(k)). The property defined this way by the formula is the set of finite structures such that we are able to obtain the empty structure when applying the rule repeatedly. Many classical properties can be formulated by means of a. "destructive" rule. We do a systematic study of the computational complexity of these properties according to the fragment of first-order logic in which the rule is expressed. We give the list of minimal fragments able to define NP-complete properties and maximal fragments that define only PTIME properties (unless PTIME = NP), depending on the number k of free variables and the quantifier symbols used in the formula. We also study more specifically the case where the formula has one free variable and is universal.