Given a set of terms Θ, an element tc of its consistency set C ( Θ) can indeed be considered as the "type" of an element e of the domain of an ADM w.r.t. Θ . Any such element e belongs to the interpretations of some of the terms in Θ, and to the complements of the interpretations of the other terms. Thus, if c is the set of terms of Θ to which e belongs, then e also belongs to the interpretation of tc and it does not belong to the interpretation of any of the other terms in C(0). In this case we say that e realizes the type t c .

We are now ready to formulate the theorem that reduces the relativized satisfiability problem in a fusion of two local ADSs to relativized satisfiability in the component ADSs.

A proof of this theorem can be found in the appendix. Theorem 20. Let Si = (Li, Mi), i E {1, 2}, be two local ADSs in which L1 is based on the set of function symbols F and relation symbols R, and L2 is based on G and Q, and let L = L 1 ® L 2 and M = M 1 ® M 2 . If Γ is a finite set of assertions from L , then the following are equivalent:
1. Γ is satisfiable in ( L , M ).

2. There exist
(a) a set D C C 1 (F),
(b) for every term t E D an object variable at & obj(F),
(c) for every a E obj(F) a term t a E D,
ssssssssssse
(L1, M1):
(d) {a t : sur 1 (t) | t E D} U {T E sur 1 (VD)},
(c) {a : sur1 (t a) | a ∈ obj(Γ)},
(f) {R(a, b) | R(a, b) E Γ, R E R},
(g) { sur 1 (t 1 ) E sur 1 (t 2 ) | t 1 E t 2 E Γ} U { a : sur 1 (s) | (a : s) E Γ };
and the union Γ 2 of the following sets of assertions in L 2 is satisfiable in ( L 2 , M 2 ):
(h) {a t : sur2(t) | t E D} U {T E sur2(VD)},
(i) {a : sur2(ta) | a E obj(Г)},
(j) {Q(a, b) | Q(a, b) E Γ, Q E Q}.

Intuitively, (2a) "guesses" a set D of types (i.e., elements of the consistency set). The idea is that these are exactly the types that are realized in the model of Γ (to be constructed when showing (2 → 1) and given when showing (1 → 2)).  Condition (2b) introduces for ery type in D a name for an object realizing this type, and (2c) "guesses" for every object variable occurring in Γ a type from D .

Regarding (2d) and (2h), one should note that the set of assertions { a i : t | t ∈ D}U{T ⊆
\ D} states that every type in D is realized (i.e., there is an object in the model having this type) and that every object has one of the types in D . The sets of assertions (2d) and (2h) are obtained from this set through surrogation to make it digestible by the decision procedures of the component logics.