Equivalences in ASP by Countermodels in the Logic of Here-and-There 9 Proposition 1 Given a theory Γ, in general there is no theory Γ
′
such that (**X, Y** ) is an HT-countermodel of Γ iff it is a HT-model of Γ
′
, for any HT-interpretation (**X, Y** ).

## Proof

As observed in (Cabalar and Ferraris 2007), any theory has a total-closed set of countermodels. Consider the theory Γ = {a} and suppose there exists a theory Γ
′
, such that
(**X, Y** ) is an HT-countermodel of Γ iff it is an HT-model of Γ
′
. Then, vice versa, (**X, Y** )
is an HT-countermodel of Γ
′
iff it is an HT-model of Γ. Since for Y = {a}, (**Y, Y** ) is an HT-model of Γ, we conclude that (**Y, Y** ) is an HT-countermodel of Γ
′
. Because any theory has a total-closed set of countermodels, it follows that (∅, Y ) is an HT-countermodel of Γ
′
,
hence, an HT-model of Γ. Contradiction.

## 3.2 Characterizing Equivalence By Means Of Equivalence Interpretations

The characterization of countermodels by a theory in HT essentially fails due to total HTcountermodels. However, total HT-countermodels of a theory are not necessary for characterizing equivalence, in the sense that they can be replaced by total HT-models of the theory for this purpose.

Definition 4 An HT-countermodel(**X, Y** ) of a theory Γ is called a *here-countermodel* of Γ if Y |= Γ.

Definition 5 An HT-interpretation is an *equivalence interpretation* of a theory Γ if it is a total HT-model of Γ or a here-countermodel of Γ. The set of equivalence interpretations of a theory Γ is denoted by Es(Γ).

Theorem 2 Two theories Γ1 and Γ2 coincide on their HT-countermodels iff they have the same equivalence interpretations, symbolically Cs(Γ1) = Cs(Γ2) iff Es(Γ1) = Es(Γ2).

## Proof

For the only-if direction, assume that two theories, Γ1 and Γ2, have the same sets of HTcountermodels. This implies that they have the same here-countermodels. Furthermore, since the total HT-countermodels are equal, they also coincide on total HT-models. Consequently, Γ1 and Γ2 have the same equivalence interpretations.

For the if direction, assume that two theories, Γ1 and Γ2, coincide on their equivalence interpretations. Then they have the same total HT-models and hence the same total HTcountermodels. Since total HT-countermodels of every theory are total-closed in the set of HT-countermodels, the sets of HT-countermodels coincide on all HT-interpretations
(**X, Y** ) such that(**Y, Y** ) is a (total) HT countermodel. All remaining HT-countermodels are here-countermodels and therefore coincide by hypothesis and the definition of equivalence interpretations. This proves the claim.