proving (X′, Y ) |= ψ1 and (or) (X′, Y ) |= ψ2, for all X′ ⊆ Y such that X|A+ ⊆ X′|A+
and X′|A− ⊆ X|A−, i.e., (X′, Y ) |= ψ for all X′ under consideration. Assume (d), i.e.,
(**Y, Y** ) 6|= ψ. As a consequence, (**Y, Y** ) 6|= ψ1 or (and) (**Y, Y** ) 6|= ψ2, hence by induction hypothesis, for all X′ ⊆ Y , it holds that (X′, Y ) 6|= ψ1 or (and) (X′, Y ) 6|= ψ2. Therefore,
(X′, Y ) 6|= ψ, for all X′ ⊆ Y .

Finally, let ψ be of the form ψ1 → ⊥. Then, ψ1 is factual and of connective nesting depth depth n − 1. In case (c), if (**X, Y** ) |= ψ, then Y |= ψ, hence Y 6|= ψ1, i.e., (**Y, Y** ) 6|= ψ1 and by induction hypothesis (d), the same holds for any (X′, Y ) such that X′ ⊆ Y . Thus, in particular for X′ ⊆ Y such that X|A+ ⊆ X′|A+ and X′|A− ⊆ X|A−, it follows that
(X′, Y ) 6|= ψ1. Moreover, Y |= ψ, and therefore (X′, Y ) |= ψ → ⊥, for all X′ ⊆ Y such that X|A+ ⊆ X′|A+ and X′|A− ⊆ X|A−. For (d), assume (**Y, Y** ) 6|= ψ. Consequently Y 6|= ψ, and this implies (X′, Y ) 6|= ψ, for all X′ ⊆ Y . This concludes the inductive argument and proves (c) and (d) for factual formulas over A+ of arbitrary connective nesting.

Concerning the claim of the proposition, since (**X, Y** ) |= Γ implies (**X, Y** ) |= φ and
(**X, Y** ) |= ψ, for every A+-A−-formula φ in Γ and every factual formula ψ in Γ, we conclude that (X′, Y ) |= φ and (X′, Y ) |= ψ, for all X′ ⊆ Y such that X|A+ ⊆ X′|A+ and X′|A− ⊆ X|A−. This proves (X′, Y ) |= Γ, for all X′ under consideration.

Complementary to this result, given a total HT-model of an (extended) A+-A−-theory, we can infer its satisfaction for the following class of non-total HT-interpretations.

Proposition 5 Consider an extended propositional A+-A−-theory Γ, and a total HT-interpretation (**Y, Y** ).

Then, (**Y, Y** ) |= Γ implies (X′, Y ) |= Γ, for all X′ ⊆ Y such that X′|A+ = Y |A+ .

Proof Consider any A+-A−-formula φ in Γ, i.e., any formula that has positive occurrences of atoms from A+, and negative occurrences of atoms from A−, only. We show by induction on the formula structure of φ, that for all X′ ⊆ Y such that X′|A+ = Y |A+ :
(a) (**Y, Y** ) |= φ implies (X′, Y ) |= φ if φ is a positive occurrence; and (b) (**Y, Y** ) 6|= φ implies (X′, Y ) 6|= φ if φ is a negative occurrence.

For the base case, consider any atomic formula φ, and suppose first (a) that φ is a positive occurrence such that (**Y, Y** ) |= φ. Then φ is not ⊥, and thus is an atom a from A+ such that a ∈ Y . Since X′|A+ = Y |A+ for all X′ under consideration, we conclude that a ∈ X′.

Hence, (X′, Y ) |= φ. Suppose (b) φ is a negative occurrence. If (**Y, Y** ) 6|= φ, then φ is either ⊥, or an atom b from A−, such that b 6∈ Y . Since X′ ⊆ Y implies X′|A− ⊆ Y |A−
for all X′ under consideration, we conclude that b 6∈ X′. Hence, (X′, Y ) 6|= φ.

For the induction step, assume that (a) and (b) hold for any A+-A−-formula of connective nesting depth n − 1, and let φ be a formula of connective nesting depth n. Consider the case where φ is of the form φ1 ∧ φ2, respectively φ1 ∨ φ2. If φ is a positive occurrence
(a), then so are φ1 and φ2, both of connective nesting depth depth n − 1. From (**Y, Y** ) |= φ we conclude (**Y, Y** ) |= φ1 and (or) (**Y, Y** ) |= φ2. The induction hypothesis applies, proving (X′, Y ) |= φ1 and (or) (X′, Y ) |= φ2, for all X′ ⊆ Y such that X′|A+ = Y |A+ ,
i.e., (X′, Y ) |= φ for all X′ under consideration. In case φ is a negative occurrence (b),
then so are φ1 and φ2, both of connective nesting depth n − 1. Then, (**Y, Y** ) 6|= φ implies