To simplify consider simple algebraic theories (universal algebra) A and L, but the question applies to geometric theories.
Syntactically, we can interpret L in A if we can define the operations of L as terms in A, AND then a) prove the axioms of L (which are equations in A) from the axioms of A, or even less, b) argue by any means that the equations hold in any model in Sets (using Choice etc) and then use the (easy) classical completeness theorem for algebraic theories.
This, given a model of A, determines a model of L (with same underlying set).
In the literature it is accepted that 2) holds for any (say, Grotendieck) topos, not only for models in Set.
In fact the proof in 1) a) can be done (or reproduced) directly in the internal language of the topos reasoning with the model (an object with operations etc) as it were a model in Set.
Now, in 1) a) the proofs are accepted to be classical (use excluded middle, etc), and in 1) b) even worst, no need to exhibit a proof in the theory A.
Then, in 3), this classical arguing of 1) a) would, in this case, be valid in any topos ?. And even worst, how can we justify 3) if b) was used in 1).
Help !
The only way out I see is that in 1) a) only intuitionistic logic is accepted, and b) is not accepted, for the validity of 3). But this is not what is usually done in the literature.
e.d.
