Proof For the only-if direction, assume (**X, Y** ) is an equivalence interpretation of Γ. Then Y |= ψ for all ψ ∈ Γ and therefore (**X, Y** ) |= ¬¬ψ for all ψ ∈ Γ. If X = Y , then by Lemma 2,
(**X, Y** ) also satisfies ¬¬a → a for all a ∈ L. In this case, (**X, Y** ) |= Γφ for all φ ∈ Γ.

We continue with the case where X ⊂ Y . Then, (**X, Y** ) is a here-countermodel of Γ, i.e.,
there exists φ ∈ Γ such that (**X, Y** ) 6|= φ. This implies that (**X, Y** ) |= φ → (¬¬a → a)
for all a ∈ L, i.e., (**X, Y** ) |= Γφ. This proves the claim for X ⊂ Y .

For the if direction, assume that (**X, Y** ) |= Γφ for some φ ∈ Γ. Then, (**X, Y** ) |=
¬¬ψ for all ψ ∈ Γ, which implies Y |= ψ for all ψ ∈ Γ. Consequently, (**X, Y** ) is an equivalence interpretation of Γ if X = Y . If X ⊂ Y , we conclude that (**X, Y** ) does not satisfy ¬¬a → a for some a ∈ L by Lemma 2. However, (**X, Y** ) |= Γφ for some φ ∈ Γ,
hence (**X, Y** ) |= φ → (¬¬a → a) for all a ∈ L. Therefore, (**X, Y** ) 6|= φ must hold for some φ ∈ Γ. This proves, since X ⊂ Y , that (**X, Y** ) is a here-countermodel of Γ, i.e., an equivalence interpretation of Γ.

For infinite propositional theories, we thus end up with a characterization of equivalence interpretations as the union of the HT-models of an infinite number of (infinite) theories. At least for finite theories, however, a characterization in terms of a (finite) theory is obtained
(even for a potentially extended infinite signature).

If L
′ ⊃ L and M = (**X, Y** ) is an HT-interpretation over L
′
, then M|L denotes the restriction of M to L: M|L = (X|L, Y |L). The restriction is *totality preserving*, if X ⊂ Y
implies X|L ⊂ Y |L.

Proposition 3 Let Γ be a theory over L, let L
′ ⊃ L, and let M an HT-interpretation over L
′
such that M|L is totality preserving. Then, M ∈ Cs(Γ) implies M|L ∈ Cs(Γ).

## Proof

Let M = (X′, Y ′), M|L = (**X, Y** ), and assume M 6|= Γ. First, suppose M is total, hence, Y
′ 6|= Γ. Then, Y 6|= Γ, because otherwise Y
′
|= Γ would hold, since Γ is over L. This proves the claim for total HT-countermodels, and since HT countermodels are total-closed, for any HT-countermodel M = (X′, Y ′), such that Y
′ 6|= Γ.

We continue with the case that Y
′
|= Γ. Then X′ ⊂ Y
′ holds, which means that M
is an equivalence interpretation of Γ. Therefore, M 6|= φ for some φ ∈ Γ. Additionally, M |= ¬¬ψ for all ψ ∈ Γ (recall that Y
′
|= Γ). This implies M |= Γφ, where Γφ =
{¬¬ψ | ψ ∈ Γ} ∪ {φ → (¬¬a → a) | a **∈ L}**. Therefore, M|L |= Γφ, i.e., M|L
is an equivalence interpretation of Γ. Since the restriction is totality preserving, M|L is non-total. This proves M|L 6|= Γ.

This eventually enables the characterization of the HT-countermodels of a finite theory by another finite theory, as stated in the next result.

Theorem 3 Let Γ be a finite theory over L, and let M be an HT-interpretation. Then, M ∈ Es(Γ) iff M|L |=Wφ∈Γ
Vψ∈Γφ ψ, and M|L is totality preserving.