Equivalences in ASP by Countermodels in the Logic of Here-and-There 7 Definition 2 An HT-interpretation (**X, Y** ) is an *HT-countermodel* of a theory Γ if (**X, Y** ) 6|= Γ. The set of HT-countermodels of a theory Γ is denoted by Cs(Γ).

Intuitively, an HT-interpretation fails to be an HT-model of a theory Γ when the theory is not satisfied at one of the worlds (here or *there*). Note that satisfaction at the *there* world amounts to classical satisfaction of the theory by Y . A simple consequence is that if Y 6|=
Γ, then (**X, Y** ) is an HT countermodel of Γ for any X ⊆ Y . At the *here* world, classical satisfaction is a sufficient condition but not necessary. For logic programs, satisfaction at the *here* world is precisely captured by the reduct of the program Π wrt. the interpretation at the *there* world, i.e., if X |= ΠY.

Definition 3 A total HT-interpretation (**Y, Y** ) is *total-closed* in a set S of HT-interpretations if (**X, Y** ) ∈
S for every X ⊆ Y . We say that an HT-interpretation (**X, Y** ) is

- *closed* in a set S of HT-interpretations if (X′, Y ) ∈ S for every X ⊆ X′ ⊆ Y .

- *there-closed* in a set S of HT-interpretations if (**Y, Y** ) 6∈ S and (X′, Y ) ∈ S for every X ⊆ X′ ⊂ Y .
A set S of HT-interpretations is total-closed, if every total HT-interpretation (**Y, Y** ) ∈ S
is total-closed in S. By the remarks on the satisfaction at the *there* world above, it is obvious that every total HT-countermodel of a theory is also total-closed in Cs(Γ). Consequently, Cs(Γ) is a total-closed set for any theory Γ. By the same argument, if (**X, Y** ) is an HT-countermodel such that X ⊂ Y and Y 6|= Γ, then (**X, Y** ) is closed in Cs(Γ). The more relevant cases concerning the characterization of equivalence are HT-countermodels
(**X, Y** ) such that Y |= Γ.

## Example 2

Consider the theory Γ1 in Example 1 and a non-total HT-interpretation (X,L). Since
(X,L) is non-total, X ⊂ L holds, and therefore (X,L) 6|= ai, for some ai ∈ L. Thus, we have identified a HT-countermodel of Γ1. Moreover the same argument holds for any non-total HT-interpretation of the from (X′,L) (in particular such that X ⊆ X′ ⊂ Y ).

Therefore, (X,L) is there-closed in Cs(Γ1).

The intuition that, essentially, there-closed countermodels can be used instead of maximal non-total HT-models for characterizing uniform equivalence draws from the following observation. If (**X, Y** ) is a maximal non-total HT-model, then every (X′, Y ), such that X ⊂ X′ ⊂ Y , is a there-closed HT-countermodel. However, there-closed HTcountermodels are not sensitive to the problems that infinite chains cause for maximality.

Given a theory Γ, let Cu(Γ) denote the set of there-closed HT-interpretations in Cs(Γ).

Theorem 1 Two propositional theories Γ1, Γ2 are uniformly equivalent iff they have the same sets of there-closed HT-countermodels, in symbols Γ1 ≡u Γ2 iff Cu(Γ1) = Cu(Γ2).