This proposition offers another way of proving Proposition 2, as[Lifschitz *et al.*, 2001]
showed that the equilibrium models of a program with nested expressions are the stable models of the same program in the sense of [Lifschitz *et al.*, 1999].

## 2.4 Properties Of Propositional Theories

This section shows how several theorems about logic programs with nested expressions can be extended to propositional theories.

## 2.4.1 Strong Equivalence

Two theories Γ1 and Γ2 are *strongly equivalent* if, for every theory Γ, Γ1 ∪ Γ and Γ2 ∪ Γ have the same stable models.

Proposition 5. For any two theories Γ1 and Γ2, the following conditions are equivalent:
(i) Γ1 *is strongly equivalent to* Γ2,
(ii) Γ1 is equivalent to Γ2 in the logic of here-and-there, and
(iii) for each set X *of atoms,* Γ
X
1 is equivalent to Γ
X
2 in classical logic.

The equivalence between (i) and (ii) is essentially Lemma 4 from [Lifschitz *et al.*, 2001]
about equilibrium logic. The equivalence between (i) and (iii) is similar to Theorem 1 from [Turner, 2003] about nested expressions, but simpler and more general.

Notice that (iii) cannot be replaced by
(iii') for each set X of atoms, Γ
X
1 is equivalent to Γ
X
2 in classical logic, not even when Γ1 and Γ2 are programs with nested expressions. Indeed, {p ← ¬p}
is strongly equivalent to **{⊥ ← ¬**p}, but {p ← ¬p}
∅ = {p **← ⊤}** is not classically equivalent to **{⊥ ← ¬**p}
∅ = **{⊥ ← ⊤}**.

Replacing, in a theory Γ, a (sub)formula F with a formula G is guaranteed to preserve strong equivalence iff F is strongly equivalent to G. Indeed, strong equivalence between F and G is clearly a necessary condition: take Γ = {F}.

It is also sufficient because - as in classical logic - replacements of formulas with equivalent formulas in the logic of here-and-there preserves equivalence in the same logic.

Cabalar and Ferraris [2007] showed that any propositional theory is strongly equivalent to a logic program with nested expressions. That is, a propositional theory can be seen as a different way of writing a logic program. This shows that the concept of a stable model for propositional theories is not too different from the concept of a stable model for a logic program.