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, 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.

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. 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.


No, this is not a problem. If $U$ is a transitive set with $\mathcal{P}(\omega) \subseteq U$ then $U$ contains the real $\{\ulcorner\sigma\urcorner \mid U \vDash \sigma\}$. So, for example, $V_\alpha$ contains its own theory for every $\alpha>\omega$.


Adding to the existing answers, we can even have $A$ be $OD$ without resulting in contradiction. For example, for $\alpha$ a limit ordinal look at the real $$C_\alpha=\{i: 2^{\aleph_{\alpha +2i}}\not=2^{\aleph_{\alpha+2i+1}}\}.$$ Each $C_\alpha$ is clearly $OD$, but there's no reason we can't have $\{C_\alpha: \alpha\in ON\}=\mathbb{R}$ and hence $A=C_\alpha$ for some $\alpha$. (In fact, for any $V\models ZFC$ there is a forcing extension in which every real appears as some $C_\alpha$!)