As a consequence of this result, and the usual relationships on HT-models, we can characterize equivalences of propositional theories also by selections of equivalence interpretations, i.e., a mixture of non-total here-countermodels and total HT-models, such that the characterizations, in particular for uniform equivalence, are also correct for infinite theories.

Definition 6 Given a theory Γ, we denote by

- Cc(Γ), respectively Ec(Γ), the restriction to total HT-interpretations in Cs(Γ), respectively in Es(Γ);
- Ca(Γ) the set of there-closed HT-interpretations of the form (∅, Y ) in Cs(Γ), and by Ea(Γ) the set of total-closed HT-interpretations in Es(Γ) (i.e., equilibrium models);
- Eu(Γ) the set of closed HT-interpretations in Es(Γ).
By means of the above sets of HT-countermodels, respectively equivalence interpretations, equivalences of propositional theories can be characterized as follows.

Corollary 1 Given two propositional theories Γ1 and Γ2, the following propositions are equivalent for e ∈ {**c, a, s, u**}:
(1) Γ1 ≡e Γ2; (2) Ce(Γ1) = Ce(Γ2); (3) Ee(Γ1) = Ee(Γ2).

Example 4 In our running example, Cu(Γ1) 6= Cu(Γ2), as well as Eu(Γ1) 6= Eu(Γ2), by the remarks on non-total HT-interpretations in Example 3.

Since equivalence interpretations do not encompass total HT-countermodels, we attempt a direct characterization in HT.

Lemma 2 For any HT-interpretation (**X, Y** ) of signature L and τǫ = {¬¬a → a | a **∈ L}**, it holds that (**X, Y** ) |= τǫ iff X = Y .

Proof
(**X, Y** ) |= τǫ for all a ∈ L iff (**X, Y** ) |= ¬¬a → a for all a ∈ L iff, for every a ∈ L, it holds that (X, Y ) 6|= ¬¬a or (**X, Y** ) |= a, and Y |= ¬¬a → a. The latter is a tautology, and (**X, Y** ) 6|= ¬¬a iff a 6∈ Y . We conclude that (**X, Y** ) |= τǫ iff (**X, Y** ) |= a for all a ∈ Y , i.e., iff X = Y .

By means of this lemma, we can use formulas of the form ¬¬a → a to ensure for a given formula φ of Γ that if (**X, Y** ) |= φ then X = Y , i.e., that the HT-interpretation is total.

Proposition 2 Let M be an HT-interpretation over L. Then, M ∈ Es(Γ) for a theory Γ iff M |= Γφ for some φ ∈ Γ, where Γφ = {¬¬ψ | ψ ∈ Γ} ∪ {φ → (¬¬a → a) | a **∈ L}**.