I'm currently reading through Mendelson's `Introduction to Mathematical Logic', and one of the proofs has left me dissatisfied.
In general, I am fine with seeing metamathematical results proven using model theory, so long as they are not too fundamental - i.e. if I feel that one could develop a theory without these results that is sufficiently strong to in principle be later used as a metatheory to prove said results in. This is why I am fine with the completeness theorem being proved using model theoretic tools, as I believe that one can develop set theory without it to the point that one could then use that set theory as a metatheory in which model theoretic results can be proved.
I run into a problem with this view in chapter 2.9. of Mendelson's book, however, as a result is proved using model theory that I view as being absolutely funadamental. Proposition 2.28 of this chapter essentially states that if $K$ is a first order theory with equality, and $\vdash_K (\exists ! u)\beta(u, x_1, \dots , x_n)$, then the theory $K^*$ obtained by adding to $K$ a new function letter $f$ of $n$ arguments along with the proper axiom $\beta(f(x_1, \dots, x_n), x_1, \dots , x_n)$ and instances of other logical axioms that need be amended is in a sense `equivalent' to $K$. There is an effective procedure which shows that any theorem provable in $K^*$ is also provable in $K$ (and vice versa, of course).
I view it as fundamental that one may introduce new constants whenever one has shown unique existence, without adding strength to a theory, but the proof this book uses for this is model theoretic and non-constructive.
The author acknowledges this later on, stating that Kleene gives a constructive syntactical proof in his 1952 text `Introduction to metamathematics' but I cannot easily get a hold of this book in order to see the proof.
I am wondering here if anyone would be able to give the proof, or at least an outline, or direct me to where I can find a proper, syntactical proof of the theorem in Mendelson's book. I would like to at least be able to view the page of Kleene's book in which the result is proved, and if it looks good enough I'll buy the text (since I imagine the proof will rely on earlier lemmas I'd need to dig into), but so far I haven't be able to find a preview of the page.
To be precise in what follows, here are what I am assuming are the axioms:
Along with the rules of inference given by Modus Ponens and Generalization.
The main tool to use after this is the Deduction Theorem, which I assume if fundamental enough that you're familiar with it.
Something additional I will assume you'll be fine with is the fact that if $\Phi$ is a consistent set of sentences in a signature $\sigma$, then expanding $\sigma$ with new constants (giving, say, $\sigma'$) still leaves $\Phi$ consistent. Basically, the proof is that we can transform any proof of $\bot$ from $\Phi$ over $\sigma'$ into a proof of $\bot$ from $\Phi$ over $\sigma$ by replacing any newly-used constants with unused variables.
This same idea is used to show that if $\Phi \vdash \exists x \varphi(x)$ then $\Phi \cup \{\varphi(c)\}$ is consistent (over the new language), where $c$ is some new constant. Indeed, suppose for the sake of a contradiction that $\Phi \cup \{\varphi(c)\} \vdash \bot$, so that by the Deduction Theorem we have $\Phi \vdash (\varphi(c) \to \bot)$. Take the proof of $\varphi(c) \to \bot$ and turn it into a proof of $\varphi(x) \to \bot$, using the fact that relative to $\Phi$ there isn't anything special about the constant $c$ and so replacing it with any other constant or variable shouldn't affect the validity of the proof. By generalization, we find that $\Phi \vdash \forall x (\varphi(x) \to \bot)$.
Now, $\Phi \vdash \exists x \varphi(x)$ by hypothesis. $\exists x \varphi(x)$ is the same as $\neg \forall x \neg \varphi(x)$, or $((\forall x (\varphi(x) \to \bot))\to \bot)$. But we've shown that $\Phi \vdash \forall x (\varphi(x) \to \bot)$, and so by Modus Ponens we have $\Phi \vdash \bot$, contradicting the assumed consistency of $\Phi$.
At this point we can prove your result (though what we've done above is remarkably close). Suppose $\Phi \vdash \exists u \varphi(u,x_1,\ldots, x_n)$ for every $x_1,\ldots, x_n$. Then we can choose for $x_1,\ldots, x_n$ a constant symbol $c_{x_1,\ldots, x_n}$ and add $\varphi(c_{x_1,\ldots, x_n},x_1,\ldots, x_n)$ to $\Phi$. From the above, the resulting theory is consistent.
Now add a function symbol $f$ and add the sentences $f(x_1,\ldots, x_n)=c_{x_1,\ldots, x_n}$ to $\Phi$. Now all we need to do is show that the resulting theory is consistent. But this follows almost immediately from the same kinds of arguments from above: if we have a proof of $\bot$, we can just replace any instance of $f(x_1,\ldots, x_n)$ with $c_{x_1,\ldots, x_n}$ to get the necessary contradiction.