When adjoining a new sort that is supposed to model the powerset of the original domain of discourse, what is the appropriate notion of embedding? Edit. This question hasn't generated much interest so far. Any suggestions for improvement would be much appreciated, so please leave a comment. Best wishes.

Often, we begin with a first-order theory $(T,L)$ and then adjoin a 'sort of all subsets' to obtain a bigger theory $(T',L').$ My concern is this. I want to know that if we're working in the bigger theory $(T',L')$ and we prove a theorem in the language of $L$, then this theorem can be deduced from $T$ alone.
Lets consider the issue in more detail.
By the term first-order theory, let us mean an ordered pair $(T,L)$ where $L$ is a (many-sorted) first-order language, and $T$ is an arbitrary (not necessarily deductively closed) subset of $L$.
Now consider a first-order theory $(T,L)$ with a single sort $X$. We can obtain a new first-order theory $(T',L')$ by adding


*

*a new sort $\mathcal{P}(X)$

*a membership relation $\in\; : X \rightarrow \mathcal{P}(X),$

*an axiom of extensionality for the elements of $\mathcal{P}(X)$

*and a comprehension* schema.


Now presumably, the inclusion map $f : L \rightarrow L'$ is some sort of an embedding (not just of the languages, but more importantly, of the theories). What is the appropriate notion of embedding for this situation, and how do we know that $f$ has the property of interest? By proving that $f$ is indeed an embedding in the appropriate sense, we should be able to deduce as an immediate corollary that if we're working in the bigger theory $(T',L')$ and we prove a theorem in the language of $L$, then this theorem can be deduced from $T$ alone.
*The comprehension schema can be stated as follows. For all natural numbers $n$ and $m$ and all formulae $$\varphi(a_0,\cdots,a_n,A_0,\cdots,A_m,y)$$ in the language $L'$, we take the following as an axiom.

For all $(a_0 : X)(\cdots)(a_n : X)$ and all $(A_0 :
 \mathcal{P}(X))(\cdots)(A_m : \mathcal{P}(X))$, there exists $Y :
 \mathcal{P}(X)$ such that for all $x : X$ we have $$x \in Y
 \Leftrightarrow \varphi(a_0,\cdots,a_n,A_0,\cdots,A_m,y).$$

 A: The definition you are looking for is conservative extension.
I think the easiest way to show that $T'$ is a conservative extension of $T$ is to note that every model $\mathcal{M}$ of $T$ can be extended to a model $\mathcal{M}'$ of $T'$ in the obvious way (by setting $\mathcal{P}(X)$ to be the usual powerset). In the wikipedia article I linked to, this is called a model theoretic conservative extension. It follows that $T'$ is a conservative extension of $T$ using the completeness theorem for first order logic.
Something to note about this construction is that it is not always as useful as you might think. For example, you might expect that if $T$ is Peano arithmetic $\mathbf{PA}$, then $T'$ is second order arithmetic $\mathbf{Z}_2$. This is not the case, and in fact $\mathbf{Z}_2$ is definitely not conservative over $\mathbf{PA}$.
A: There's not a special name for the embedding; in this case $L$ is just a subset of $L'$ so there's not even much need to talk about "embedding".  There is one piece of terminology; we say that $T'$ is conservative over $T$ if, for every sentence $\phi \in L$, if $\phi$ is provable in $T'$ then it is provable in $T$. 
In most cases of interest, the second-order theory with full comprehension will not be conservative over the original theory. Usually we have to weaken the comprehension scheme to fix this. For example, the second-order theory conservative over PA is known as $\mathsf{ACA}_0$, and is obtained by extending the language and then adding comprehension and induction axioms for all arithmetical formulas (formulas that do not quantify over sets). 
Somewhat similarly, NBG set theory is a second-order extension of ZFC set theory, and NBG is conservative over ZFC for sentences in the language of ZFC. But NBG does not have full comprhension, it only has comprehension for formulas that do not quantify over classes. If we add full comprehension we obtain something like Morse-Kelly set theory which is no longer conservative over ZFC. 
In general, the choice of the right comprehension scheme to get conservativity is delicate. If you add no additional axioms than the second-order extension is conservative over the original, but not useful for proving any new theorems. If you add too many comprehension axioms, the new theory is likely to be too strong. So some amount of context-specific proof is required for each result to show that a particular amount of comprehension is still conservative over the original theory. 
