Models within a model of set theory Assume (M,∊M) is a model of ZF. Assume also that (n,∊n) ∊ M is a model in the sense of M and (N,∊N) is a model in the real world with the property that for all sentences σ
N ⊨ σ   if and only if   M ⊨ (n ⊨ σ).
By using conjunction ∧ it follows that, if T is a finite set of sentences then
N ⊨ T   if and only if   M ⊨ (n ⊨ T).   (1)
For example, if T consists of only two sentences σ1 and σ2 then
N ⊨ T   iff   N ⊨ σ1∧σ2   iff   M ⊨ (n ⊨ σ1∧σ2)   iff   M ⊨ (n ⊨ T) 
However, for an infinite set of sentences T the same argument to prove (1) does not work. Furthermore I think that (1) is not true for infinite T but the reasons for this are unclear to me.
Let's take T=ZF for example. To prove (1), could we not proceed as follows? First we construct ZF (the set of sentences) inside M. We can surely do this inside a model of ZF. Let's call this set ZFM. Then if we knew that there is some kind of correspondence between ZFM and the real world ZF, then using this correspondence, could we somehow deduce (1) or even one implication of the equivalence (1)?
My question is that what kind of relationship (if any) there is between the set of sentences constructed in the model M, say TM, and the real T. And if they happen to be fundamentally different, then what are the reasons behind this? Furthermore, is there some property of the model M which guarantees that TM and the real T are essentially the same?
 A: There is an interesting observation surrounding the latter
part of your post, recently discussed in an article of
Brice Halimi (Université Paris Ouest), that many set
theorists find surprising. It is the following:
Theorem. Every model of ZFC contains an element that
is a model of all the ZFC axioms.
To be more precise, if $\langle M,{\in}^M\rangle$ is a
model of of ZFC, then there is an object $n$ in $M$ which
$M$ thinks to be a model in the language of set theory and
furthermore, every individual axiom of ZFC is true in $n$.
The proof is relatively simple (and it seems that each part
of it was known classically, although Brice has pulled them
nicely together). Suppose that $\langle M,{\in}^M\rangle$
is a model of ZFC. This implies, of course, that ZFC is
consistent. If it happens that $M$ is $\omega$-standard,
meaning that it has no nonstandard natural numbers, then
$M$ will have the same proofs that we do outside of $M$,
and so $M$ will agree that ZFC is consistent. Hence, by the
Completeness theorem, $M$ will be able to build a model of
ZFC, such as by the Henkin method. Alternatively, suppose
that $M$ is $\omega$-nonstandard. We know that for any
natural number $m$, the Reflection theorem ensures that
some $V_\alpha$ is a model of the $\Sigma_m$-fragment of
ZFC. Thus, inside $M$, every standard $m$ has the property
that there is some $(V_\alpha)^M$ satisfying the $\Sigma_m$
fragment of the (nonstandard) version of ZFC inside $M$.
Since the standard cut of the natural numbers is not
amenable to $M$, it must be that there is some nonstandard
natural number $k$ such that $M$ believes that there is
some $(V_\alpha)^M$ satisfying what $M$ thinks is the
$\Sigma_k$ fragment of ZFC. Since this includes all the
standard part of ZFC, we find in this case that there is a
model of ZFC inside $M$, as desired. QED
The reason set-theorists often find the result surprising
is that on its face, it seems to conflict with the
consequence of the Incompleteness theorem, that if ZFC is
consistent, then there are models of
$ZFC+\neg\text{Con}(ZFC)$. A model of this theory can have
no element that it thinks is a model of ZFC. The difference
between this result and the result above is exactly the
difference that your question is about: the model $n$
inside $M$ is not a model of the full nonstandard version
of ZFC inside $M$, but it is a model of all the standard
ZFC axioms.
A: We will always have ${\rm ZF}^M\supseteq {\rm ZF}$.  The problem comes
if $M$ contains nonstandard sentences--which is equivalent to the question of whether $M$ contains nonstandard natural numbers since we can identify formulas with their Godel codes.
If there are no nonstandard integers, then they type of externl induction you are doing works fine, but if there aren't it might break down at a nonstandard stage.
A: In connection with the last paragraph of the question, which asks about general theories $T$ rather than ZFC, it should be mentioned that what happens will depend very sensitively on how $T$ is defined.  The point is that the definition of $T$ is what will be interpreted in $M$ to produce $T^M$.  
If $T$ is defined by an explicit algorithm that decides, for any sentence $A$, whether $A$ is an axiom of $T$, then the standard elements of $T^M$ will be exactly the elements of $T$ (under the identification described by Joel between finite strings in $M$ and in the real world).  Of course, as pointed out by Dave and Joel, $T^M$ can also contain additional, nonstandard axioms.
If $T$ is defined by a computable enumeration process, then every real axiom of $T$ will be an axiom of $T^M$ but $T^M$ might have additional standard formulas as axioms (enumerated at nonstandard stages of the process), as well as nonstandard ones.  
And for general definitions of theories $T$, just about anything can happen.  For example, a perfectly legal (though admittedly silly) definition of a theory $T$ would be "the ZFC axioms if they're consistent, and the axioms for a dense linear ordering otherwise."  Since some but not all models $M$ of ZFC think that ZFC is consistent, there will be massive disagreement as to what the (standard) axioms in $T^M$ are.
