Proof The proof is by induction on the formula structure of φ. Let M = h**I, J, K**i, M |= φ, and M′ = hI, J′, Ki for some J ⊆ J
′ ⊆ K. For the base case, consider an atomic sentence φ. If φ is of the form p(t1**, . . . , t**n), then p(ct I 1
, . . . , ct In
) ∈ J because M |= φ. By the fact that J
′ ⊇ J we conclude that p(ct I
1
, . . . , ct In
) ∈ J
′
and hence M′|= φ. If φ is of the form t1 = t2 then M |= φ implies t I
1 = t I 2
, and thus M′|= φ. Note also that M |= φ implies φ 6= ⊥. This proves the claim for atomic formulas.

For the induction step, assume that M |= φ implies M′|= φ, for any sentence of depth n−1, and let φ be a sentence of depth n. We show that M |= φ implies M′|= φ. Suppose φ is the conjunction or disjunction of two sentences φ1 and φ2. Then φ1 and φ2 are sentences of depth n − 1. Hence, M |= φ1 implies M′|= φ1, and the same for φ2. Therefore, if M models both or one of the sentences then so does M′, which implies M |= φ implies M′|= φ if φ is the conjunction or disjunction of two sentences. As for implication, since φ is factual we just need to consider the case where φ is of the form φ1 → ⊥, i.e., ¬φ1.

Then, M |= ¬φ1 iff hI, Ki |= ¬φ1 iff M′|= ¬φ1. This proves M |= φ implies M′|= φ if φ is an implication with ⊥ as its consequence. Eventually, consider a quantified sentence φ, i.e., φ is of the form ∀xφ1(x) or ∃xφ1(x). In this case, M |= φ implies M |= φ1(cε) and hI, Ki |= φ1(cε), for all ε ∈ U, respectively M |= φ1(cε), for some ε ∈ U, in case of existential quantification. Since each of the sentences φ1(cε) is of depth n − 1, the same is true for M′ by assumption, i.e., M′|= φ1(cε) and hI, Ki |= φ1(cε), for all ε ∈ U, respectively M′|= φ1(cε), for some ε ∈ U. It follows that M |= φ implies M′|= φ also for quantified sentences φ of depth n, and therefore, for any sentence φ of depth n. This proves the claim.

The different notions of closure naturally extend to (sets of) QHT-interpretations. In particular, a total QHT-interpretation M = h**I, K, K**i is called *total-closed* in a set S of QHT-interpretations if hI, J, Ki ∈ S for every J ⊆ K. A QHT-interpretation h**I, J, K**i is closed in a set S of QHT-interpretations if hI, J′, Ki ∈ S for every J ⊆ J
′ ⊆ K, and it is there-closed in S if hI, K, K**i 6∈** S and hI, J′, Ki ∈ S for every J ⊆ J
′ ⊂ K.

The first main result lifts the characterization of uniform equivalence for theories by HT-countermodels to the first-order case.

## Theorem 5

Two first-order theories are uniformly equivalent iff they have the same sets of there-closed QHT-countermodels.

The proof idea is the same as in the propositional case, thus for space reasons the proof is skipped. The same applies to Theorem 6 and Proposition 7 (cf. (Fink 2009) for full proofs).

We next turn to an alternative characterization by a mixture of QHT-models and QHTcountermodels as in the propositional case. A QHT-countermodel h**I, J, K**i of a theory Γ
is called QHT here-countermodel of Γ if hI, Ki |= Γ. A QHT-interpretation h**I, J, K**i is an QHT equivalence-interpretation of a theory Γ, if it is a total QHT-model of Γ or a QHT
here-countermodel of Γ. In slight abuse of notation, we reuse the notation Se, S ∈ {**C, E**}
and e ∈ {**c, a, s, u**}, for respective sets of QHT-interpretations, and arrive at the following formal result: