(iii) (by Lemma 13) implications (19) such that both bj and si belong to X, and
(iv) the reduct of (20) relative to X.

Notice that (i)–(iii) together are equivalent to X, so that every every proper subset of X doesn't satisfy Γ
X . It remains to show that X |= ΓX. Clearly, X satisfies (i)–
(iii). To show that X satisfies (iv) it is sufficient, by Lemma 5 (consider (20) as a propositional formula), to show that X satisfies (20): it does that by hypothesis (b).

## 4.9 Proof Of Propositions 15 And 16

Lemma 14. If, for every aggregate, computing op(W) ≺ N requires polynomial time then
(a) checking satisfaction of a theory with aggregates requires polynomial time, and
(b) computing the reduct of a theory with aggregates requires polynomial time.

Proof. Part (a) is easy to verify by structural induction. Computing the reduct essentially consists of checking satisfaction of subexpressions of each formula of the theory. Each check doesn't require too much time by (a). It remains to notice that each formula with aggregates has a linear number of subformulas.

Proposition 15. If, for every aggregate, computing op(W) ≺ N *requires polynomial time then the existence of a stable model of a theory with aggregates is a* Σ
P
2
-complete problem.

Proof. Hardness follows from the fact that theories with aggregates are a generalization of theories without aggregates. To prove inclusion, consider that the existence of a stable model of a theory Γ is equivalent to satisfiability of:
exists X such that **for all** Y , if Y ⊆ X then Y |= ΓX iff X = Y
It remains to notice that, in view of Lemma 14, checking (for any X and Y )
if Y ⊆ X then Y |= ΓX iff X = Y
requires polynomial time.

Lemma 15. Let F be a formula with aggregates containing monotone and antimonotone aggregates only, no equivalences and no implications other than negations. For any sets X, Y and Z such that Y ⊆ Z*, if* Y |= F
X *then* Z |= F
X.