Definability of truth in Set Theory I have a questions about the definability of truth in set theory.
Suppose that $\mathcal{L}$ is a language for a first order set theory $T$.
Let $Sat(A,x, y)$ be the formula that define the satisfaction relation, that this, $Sat(A,\ulcorner \varphi\urcorner, a)$ if only if  $A \vDash \varphi[a]$, where $\varphi$ is a formula in the language of $\mathcal{L}$, $A$ is a transitive set, $\ulcorner \varphi\urcorner$ is the Gödel codification, and $a=(a_1, \ldots, a_n) \subset A^n$.
If $\varphi$ is a sentence, $Sat(A,\ulcorner \varphi\urcorner, \emptyset)$ if only if $A \vDash \varphi$.
If this is correct, the following is correct: $\psi(x) := \forall A (Sat(A,x, \emptyset))$ is definable. The above formula say "for all $A$ transitive, $\varphi$ is truth in $A$". But by the Gödel's completeness theorem we know that for all sentence $\varphi$, $\psi(\ulcorner \varphi\urcorner)$ if only if $\ulcorner \varphi\urcorner$ is a theorem, but this contradicts the Tarski's theorem of undefinability of truth. What is wrong?
The problem is that $Sat(A,x, y)$ is definable for $A$ transitive set , but $A$ is  a model of $T$ is not definable? for example when $T$ is $ZFC$.
Is there a set theory $T$ in which the above reasoning is correct?
Thanks.
 A: Yes, it is true that "$\ulcorner\phi\urcorner$ is true in all models of ZFC" is expressible in set theory (all transitive models, or just all models, period). But that is not the same thing that Tarski's theorem prohibits. Tarski's theorem says "$\ulcorner\phi\urcorner$ is true" is not definable. In other words it prohibits defining a predicate $T$ such that for any $\phi,$ $T(\ulcorner \phi\urcorner)\leftrightarrow \phi.$
The error you are making is confusing the logical consequences of ZFC with the true statements (in V). What the completeness theorem tells you is that "$\phi$ is true in all models of ZFC" is the same as "$\phi$ is a theorem of ZFC" which means the syntactic definition of consequence is equivalent to the model-theory definition. It doesn’t say that something is true (in $V$) if and only if it is true in all models.

Also, on a more minor note, it's not the case that if something is true in all transitive models then it is true in all models. For instance, any arithmetical statement that is true in $V$ will be true in all transitive models of ZFC, since $V_\omega$ in a transitive model will be the same thing as in $V$. But of course there are many arithmetic statements that ZFC does not decide, so there will be non-transitive models that disagree with $V$ on these.
