For the sake of presentation, the technical content is split into two parts, discussing the propositional case first, and addressing first-order theories and nonground programs in a second part. In particular, the organization is as follows: Section 2 introduces essential preliminaries for the treatment of the propositional case. In Section 3, we develop a characterization of uniform equivalence by means of countermodels in HT, and proceed with an alternative characterization in terms of equivalence interpretations, before we turn to generalizing and characterizing relativized hyperequivalence for propositional theories.

After some introductory background on quantified HT, Section 4 deals with generalizations of previous results to first-order theories under generalized answer-set semantics. In Section 5, we apply our characterization of uniform equivalence to logic programs under various extended semantics in comparison with the traditional semantics over Herbrand domains, before we draw some conclusions in Section 6.

## 2 Preliminaries

We start with the propositional setting and briefly summarize the necessary background.

Corresponding first-order formalisms will be introduced when discussing first-order theories, respectively non-ground logic programs.

## 2.1 Propositional Here-And-There

In the propositional case we consider formulas of a propositional signature L, i.e., a set of propositional variables, and the connectives ∧, ∨, →, and ⊥ for conjunction, disjunction, implication, and falsity, respectively. Furthermore we make use of the following abbreviations: φ ≡ ψ for (φ → ψ) ∧ (ψ → φ); ¬φ for φ → ⊥; and ⊤ for **⊥ → ⊥**. A formula is said to be *factual*1if it is built using ∧, ∨, ⊥, and ¬ (i.e., implications of the form φ → ⊥),
only. A theory Γ is factual if every formula of Γ has this property.

The logic of here-and-there is an intermediate logic between intuitionistic logic and classical logic. Like intuitionistic logic it can be semantically characterized by Kripke models, in particular using just two worlds, namely "*here*" and "*there*" (assuming that the *here* world is ordered before the *there* world). Accordingly, interpretations (HT-interpretations)
are pairs (**X, Y** ) of sets of atoms from L, such that X ⊆ Y . An HT-interpretation is *total* if X = Y . The intuition is that atoms in X (the *here* part) are considered to be true, atoms not in Y (the *there* part) are considered to be false, while the remaining atoms (from Y \X)
are undefined.

We denote classical satisfaction of a formula φ by an interpretation X, i.e., a set of atoms, as X |= φ, whereas satisfaction in the logic of here-and-there (an HT-model), symbolically
(**X, Y** ) |= φ, is defined recursively:
1. (**X, Y** ) |= a if a ∈ X, for any atom a, 2. (**X, Y** ) 6|= ⊥,
3. (X, Y ) |= φ ∧ ψ if (**X, Y** ) |= φ and (**X, Y** ) |= ψ,