A “formalistic” variant of the Gödel completeness theorem A week ago I asked this at MathStackExchange, but without success.
I think, the following variant of the Gödel completeness theorem must be true, but I can't find the references. I would be grateful if specialists in logic could give me them (or enlighten me in case that something must be corrected).
A question. Joseph Shoenfield in his "Mathematical logic" (section 4.7) gives a definition of an interpretation of a theory in another theory. This notion allows to define a model of a first order theory $T$ as its interpretation in some variant of an axiomatic set theory, say, in MK (or in ZFC, I don't think that this choice is important.). (I understand that this is not the custom in mathematical logic, but I invite readers to look at this way, I will explain my motives later.)
Suppose now that we have a first order theory $T$. We define its model in MK in the way I described above, and consider the class ${\mathcal M}_T$ of all models of $T$ in MK. Each model $M\in {\mathcal M}_T$ can be considered as another first order theory, an extension by definitions of the theory MK  in the sense of Kenneth Kunen's "Foundations of mathematics" (section II.15). 
Moreover, we can add the symbol ${\mathcal M}_T$ into the signature of MK and the definition of ${\mathcal M}_T$ into the list of axioms of MK, and we'll get another first order theory, an extension by definition of MK. Let us denote this new first order theory by MK+${\mathcal M}_T$.
Now let us take a formula $\varphi$ in $T$. It has an analog $\varphi_M$ in each model $M\in {\mathcal M}_T$, and we can consider a formula $\varphi^*$ in MK+${\mathcal M}_T$ which states that 

$\forall M\quad M\in {\mathcal M}_T\Rightarrow \varphi_M$

My question is if the following proposition is true (up to some possible specifications):

Proposition. A formula $\varphi$ is deducible in $T$ if and only if the corresponding formula $\varphi^*$ is deducible in MK+${\mathcal M}_T$.

As far as I understand, this can be considered as a "weakened analog" of the Gödel completeness theorem, and the stronger one must state the same about all the formulas $\varphi$ simultaneously. 
About my motives. This comes from one of my questions at MathOverflow. I believe, there must be a way to explain mathematical logic such that the references to sets and functions appear after the axiomatic construction of the set theory (and not before, as it is now). I am not a specialist in Logic (my field is Analysis), but I am interested in this because (I teach logic sometimes, and) I am writing a textbook on university mathematics where I am planning to add a chapter about Set theory and mathematical logic. From the discussion at MathOverflow I got an impression that the idea to simplify the exposition is not hopeless, it is possible to explain everything inside the standard principle that

a mathematician can't use a term before giving a precise definition.

That is why in my text (I wrote already a draft of this chapter) Set theory preceeds mathematical logic, so that I can use the notions of set and function after their formal definition. But my problem is a lack of references. I would appreciate very much if somebody could help me with this. 
EDIT 01.04.2018. Recently one of my friends showed me an article by K.Smorynski in Handbook of Mathematical Logic (edited by Jon Barwise) where he formulates a  statement which he calls "the Hilbert-Bernays theorem" (Theorem 6.1.1 in volume 4) and which as far as I understand is equivalent to the following:

If a formal theory $T$ is consistent then it has an interpretation in PA.

I believe this is more or less equivalent to what Matt F. suggests in his answer:

If a formal theory $T$ is consistent then it has an interpretation in MK.

And if somebody could give me a reference to this statement (with a proof), this, I believe, will be a proper solution to what I need. Does anybody know such a reference?
 A: This proposition is equivalent to $Con(MK)$.  I'll make free use of the fact that $MK$ can prove the soundness of first-order logic.  I'll also use the abbreviation $M(\varphi)$ to mean the interpretation of $\varphi$ under $M$, e.g. if the language of $T$ is the language of groups, and $M$ is the interpretation of $T$ with the symmetric group $S_3$, and $\varphi = \forall x, xx=1$, then $M(\varphi) = \forall x \in S_3, xx=1$. 
Suppose we have the proposition.  Then the case $T=\emptyset$, $\varphi = \bot$ gives $Con(MK)$.
Now suppose we have $Con(MK)$ and want to prove the proposition.
The easy direction is that if $\varphi$ is deducible (i.e. $T \vdash \varphi$), then so is $\varphi^*$ (i.e. $MK+T^* \vdash \varphi^*$).
The harder direction is that if $\varphi$ is not deducible (i.e. $T \nvdash \varphi$), then neither is $\varphi^*$ (i.e. $MK+T^* \nvdash \varphi^*$).
First, if $\varphi$ is not deducible, then there is a model $M$ of $T+\neg \varphi$.  We can prove this just by formalizing Henkin's proof of the completeness theorem.  In particular $MK \vdash M(\neg\varphi^*)$. 
Now, suppose $MK+T^*\vdash \varphi^*$.  Then $MK\vdash M(\neg\varphi^*)$, and $MK\vdash M(\varphi^*)$.  But this is impossible by the consistency of $MK$, so $MK+T^*\nvdash \varphi^*$ as desired.
