
## 4.1.1 The Transfer Result

This section is concerned with establishing the following transfer theorem:
Theorem 17. Let S 1 and S 2 be local ADSs, and suppose that the relativized satisfiability problems for S1 and S2 are decidable. Then the relativized satisfiability problem for S1 & S2 is also decidable.

The idea underlying the proof of this theorem is to translate a given set of assertions Γ
of S 1 8 S 2 into a set of assertions Γ 1 of S 1 and a set of assertions Γ 2 of S 2 such that Γ is satisfiable in S 1 ® S 2 iff F 1 is satisfiable in S 1 and F 2 is satisfiable in S 2 . The first (naive)
idea for how to obtain the set Fi (i = 1,2) is to replace in F alien terms (i.e., subterms starting with function symbols not belonging to Si ) by new set variables (the surrogate variables introduced below). With this approach, satisfiability of Γ would in fact imply stisfiability of the sets Fi, but the converse would not be true. The difficulty arises when trying to combine the models of Γ 1 and Γ 2 into one for Γ .  To ensure that the two models can indeed be combined, the sets Γ i must contain additional assertions that make sure that the surrogate variables in one model and the corresponding alien subterms in the other model are interpreted in a "compatible" way. To be more precise, there are (finitely many)
different ways of adding such assertions, and one must try which of them (if any) leads to a satisfiable pair Γ 1 and Γ 2 .

For the proof of Theorem 17, we fix two local AD Ss Si = ( Ci, Mi), i E {1, 2}, in which L is based on the set of function symbols F and relation symbols R , and L 2 is based on G
and Q. Let L = L 1 8 L 2 and M = M 1 8 M 2 .

In what follows, we use the following notation: for a set of assertions Γ, denote by term (Γ) and obj (Γ) the set of terms and object names in Γ t respectively.

We start with explaining how alien subterms in the set Γ can be replaced by new set variables. For each L-term t of the form h ( t 1 , . . , t n ), h E F U G , we reserve a new variable x t , which will be called the surrogate of t . We assume that the set of surrogate variables is disjoint to the original sets of variables. As sketched above, the idea underlying the introduction of surrogate variables is that the decision procedure for S 1 ( S 2 ) cannot deal with terms containing function symbols from G ( F ). Thus, these "alien" function symbols must be replaced before applying the procedure. To be more precise, we replace the whole alien subterm starting with the alien function symbol by its surrogate. For example, if the unary symbol f belongs to F t and the unary symbol g belongs to G then f(g(f(x))) is a
"mixed" L-term. To obtain a term of L 1 , we replace the subterm g(f(x)) by its surrogate, which yields f ( x q ( f ( x )) . Analogously, to obtain a term of L 2 , we replace the whole term by its surrogate, which yields xf(g(f(x))).  We now define this replacement process more formally. Definition 18. For an L-term t without surrogate variables, denote by sur 1 ( t ) the L 1 -term resulting from t when all occurrences of terms g(t 1 , . . , t n ), g E G, that are not within the scope of some g 1 E G are replaced by their surrogate variable x g ( t 1 ,..., t n ). For a set Θ of terms, put sur 1 ( Θ ) := { sur 1 ( t ) | t ∈ Θ} and define sur 2 ( t ) as well as sur 2 ( Θ ) accordingly.

Denote by sub(0) the set of subterms of terms in 0, and by sub1(0) the variables occurring in Θ as well as the subterms of alien terms (i.e., terms starting with a symbol