It's been a while since I've dealt with something like this so I'm a bit fuzzy on the details which explains the question.
Let $T$ be a first order theory. For starters, say $T$ is finite.
Now assume $V$ is a model of ZF; and that $L^V \models "T$ has a model" (where $L^V$ is the constructible universe of $V$, and the sentence "$T$ has a model" can be written out in full since $T$ is finite.
Is it then true that $V\models "T$ has a model" ? I think it is, because as $T$ is first order, a model for it in $L^V$ will also be an actual model. If it's not true, then where does the obvious approach to proving it go wrong ?
As I see it intuitively, for any sentence $\phi$ in the language used for $T$, we will have $L^V \models "\mathfrak{M}$ is a model of $\phi$" iff $V\models$ the same thing : for the atomic formulas it comes from the fact that $L^V$ is a submodel of $V$ so the function symbols are interpreted the same way in both and $((x_1,...,x_n)\in R)^{L^V}$ iff $((x_1,...,x_n)\in R)^V $ for a fixed $R\in V$; and then the rest follows from the fact that $L^V$ is a transitive submodel of $V$ (for quantifications; the connectives should not be a problem).
If this is true, then how far can we go along this route; i.e. for instance can we replace "finite theory" by "recursively axiomatizable theory" (this would be about as far as we can get, since we need to be able to code "$x$ is a model of $T$" as a $\{\in\}$-sentence) ?
On the same line of ideas, I'm having a doubt as to what's necessary to prove the completeness theorem for finite/countable theories. I think that countable choice us enough but I don't recall whether it's necessary. If it's not and that completeness for these theories is provable from ZF alone then the above argument would be largely simplified; as $\omega^L = \omega$ and so proofs in $L$ are the same as proofs in $V$. But I suspect that countable choice or something in the likes of it is necessary; can anyone also put an end to this doubt ? (I'm not asking a separate question because as I pointed out the two are related - should I ?)
To sum up, here are my questions :
Is my argument for finite theories correct ? If not, why ? And if not, does the conclusion hold nonetheless ?
Can we go further than finite theories, e.g. with recursively axiomatizable theories ? If not, where does the process blow up ?
What choice principle is necessary to prove the completeness theorem for finite/countable theories ? Can this help for the two questions above ?
The completeness theorem only requires choice to well-order the language of the theory. If the language is already well-orderable, then no choice is needed. In particular, countable theories have countable (hence well-orderable) languages.
There are now two useful observations to make:
This is proved by induction on the complexity of $\varphi$, basically as you've said. (Incidentally, we do have to be careful with stronger "obvious" statements.)
Similarly, we have:
Noting that everything is well-orderable in $L$ (and $L$ is correct about well-orderings: if $L$ thinks something is a well-ordering, it really is), we have:
By contrast, if $V$ doesn't satisfy choice, there may be consistent theories in $V$ without models in $V$. The point, however, is that such theories are too complicated for $L$ to even talk about.
Kunen's book has a good introduction to absoluteness and arguments involving it. Incidentally, there are very very strong absoluteness principles out there - e.g. Shoenfield absoluteness - which will let you do quite a bit more than may seem possible at first. (For a silly example, Shoenfield shows that if ZFC+CH proves the Riemann hypothesis, then ZF already proves the Riemann hypothesis.)