I am wondering if it is inconsistent to have a model of set theory V such that V contains an $A\subset \omega$ that codes its first order theory.I.e. for all $\{\underline\epsilon\}$-sentences $\phi$, 


$V\models \phi \leftrightarrow \langle\phi\rangle \in A$.


Tarski's theorem shows that such an A cannot be definable, but I see no reason why such an A cannot exist in general.


In the situation I am considering, the prospective A would be OD. This arises in the following situation: there is an iterable model $M$, an elementary embedding $j:M\rightarrow N$, and when one compares $M$ and $N$, the iterate of $M$ is a strict initial segment of the iterate of $N$ or vice versa.



Is it inconsistent for a model of set theory to contain its own first order theory?
First, let me point out as the others have that if there are large
cardinals, then indeed we expect this situation. For example, if
there is a [worldly cardinal](http://cantorsattic.info/Worldly), a cardinal $\kappa$ for which $V\_\kappa\models\text{ZFC}$, then
the theory of $V\_\kappa$ will of course be an element of
$V\_\kappa$ and therefore this will be a model of the kind you
seek.


But next, although one might think at first that your situation requires
large cardinals, let me point out that in fact the situation you have
described is in fact exactly equiconsistent with ZFC.


**Theorem.** There is a model of ZFC if and only if there is a
model of ZFC with an object $A$ as you describe.


**Proof.** The converse implication is immediate. For the forward
implication, suppose that ZFC is consistent. Let $T$ be the theory
of ZFC together with the assertions about the set $A$ that you
have described, namely, the scheme of assertions that
$\phi\iff\ulcorner\varphi\urcorner\in A$. My observation is that
if ZFC is consistent, then every finite subtheory of $T$ is
consistent. The reason is that if $M\models\text{ZFC}$, then since
any finite subtheory of $T$ involves only finitely many instances
of the theory scheme, it follows by the reflection theorem that
that finite subtheory holds in some $(V\_\alpha)^M$. So the whole
theory $T$ is consistent, and any model of this is a model of your
situation.**QED**


Indeed, the same argument shows that every computably saturated model of set theory contains an element coding its own theory. Basically, the argument I give above is realizing a certain computable type. 


Essentially the same idea shows that ZFC is consistent just in case there is a
model $M\models\text{ZFC}$ with a cardinal $\kappa$ for which
$V\_\kappa^M\prec M$. This is a little paradoxical at first, since
you might think that $M$ would have to think that such a
$V\_\kappa$ is a model of ZFC itself, but that conclusion is
unwarranted, since perhaps $M$ is $\omega$-nonstandard, in which
case its understanding of ZFC is is not accurate.


**Theorem**. There is a model of ZFC if and only if there is a model $M$ of ZFC with a cardinal $\kappa$ for which $V\_\kappa^M\prec M$. 


I have used this fact in a few arguments in papers of mine, such as my paper [A simple maximality principle](http://jdh.hamkins.org/maximalityprinciple/). 


Finally, let me reiterate and confirm your statement (sorry for my earlier confusion) that the theory of a model can never be definable in the model. This is a consequence of [Tarski's theorem on the non-definability of truth](https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem). If there were a formula $\varphi(\cdot)$ with one free variable such that a model of set theory $\langle M,\in^M\rangle\models\sigma$ just in case it satisfies $\varphi(\ulcorner\sigma\urcorner)$, then by the fixed-point lemma we can find a sentence $\sigma$ that is ZFC-provably equivalent to $\neg\varphi(\ulcorner\sigma\urcorner)$, and since $\sigma$ asserts its own falsehood, we easily get a contradiction. 


