A−-theories. Since the if direction just referred to A+-A−-theories (which, trivially, are extended A+-A−-theories too), we obtain the following.

Corollary 3 Two propositional theories Γ1, Γ2 are *relativized hyperequivalent wrt. extended* A+-A−-
theories if and only if they coincide on their HT-hyperequivalence interpretations wrt. A+
and A−.

Thus, also relativized uniform equivalence is independent of whether sets of atoms or factual theories are permitted as contexts. More generally, for any notion of relativized hyperequivalence, factual theories over A+ can be allowed in the context without altering the notion of equivalence captured. This holds essentially due to Proposition 4, which generalizes Lemma 1 (Lemma 5 in (Pearce and Valverde 2004)) in this respect.

A final result establishes, that the notion of relativized hyperequivalence which has been introduced in this section is a proper generalization of the respective logic programming version to the more general case of propositional theories under answer-set semantics. It is a straight forward consequence of Theorem 4, since the A+-A−-theories in the proof of the if direction consist of formulas corresponding to rules with heads restricted to positive atoms from A+ and body atoms from A−. Let us say that two propositional programs Π1 and Π2 are relativized hyperequivalent wrt. A+ and A− in the logic programming sense, in symbols Π1 A
+
A−≡ lp Π2, if and only if Π1 ∪ Π ≡a Π2 ∪ Π for any program Π, such that H−(r) = ∅, H+(r) ⊆ A+, and B(r) ⊆ A−, for all r ∈ Π.

Corollary 4 Given two programs Π1 and Π2, let A+ and A− be sets of propositional variables. Then, Π1 A
+
A−≡ lp Π2 if and only if Π1 A
+
A−≡ Π2.

## 4 Generalization To First-Order Theories

Since the characterizations, in particular of uniform equivalence, presented in the previous section capture also infinite theories, they pave the way for generalizing this notion of equivalence to non-ground settings without any finiteness restrictions. In this section we study first-order theories.

As first-order theories we consider sets of sentences (closed formulas) of a first-order signature L = hF,Pi in the sense of classical first-order logic. Hence, F and P are pairwise disjoint sets of function symbols and predicate symbols with an associated arity, respectively. Elements of F with arity 0 are called object constants. A 0-ary predicate symbol is a propositional constant. Formulas are constructed as usual and variable-free formulas or theories are called *ground*. A sentence is said to be *factual* if it is built using connectives
∧, ∨, ∃, ∀, and ¬ (i.e., implications of the form φ → ⊥), only. A theory Γ is factual if every sentence of Γ has this property. The abbreviations introduced for propositional formulas carry over: φ ≡ ψ for (φ → ψ) ∧ (ψ → φ); ¬φ for φ → ⊥; and ⊤ for **⊥ → ⊥**.

## 4.1 Static Quantified Logic Of Here-And-There

Semantically we refer to the static quantified version of here-and-there with decidable equality as captured axiomatically by the system QHTs= (Pearce and Valverde 2006; Lifschitz et al. 2007;