Questions about definability of truth Suppose that I work in Zermelo-Fraenkel set theory with the axioms of choice (ZFC). Using the recursion theorem, I can define the truth value of formulas in the language $\mathcal{L}$ of set theory (one predicate symbol $\in$), $Val_\mathcal{M}(\varphi)$, for structures $\mathcal{M}$ whose universe is a set.
Hence, for any set $A$, I can define the relation $\left( A, \in\upharpoonright_A \right)\models\varphi$ in the language of set theory.
Since $\left( A, \in\upharpoonright_A \right)$ interprets $\mathcal{L}$, it seems that this relation can define the set of all true formulas (with respect to the model $A$). This contradicts Tarski's theorem. What am I missing?
My second question is why this definition for $Val_\mathcal{M}(\varphi)$ fails when $\mathcal{M}$ is a proper class, and why the existence of such a definition of truth over a proper class would contradict Tarski's theorem (whereas the same definition over a set exists and does not contradict it).
 A: Short version: the Skolem functions on a proper class are too big.
Long version: the way we define the predicate "$A\models\varphi$" is via Skolem functions: $A\models \varphi$ if there is a Skolem function witnessing that $\varphi$ is true in $A$. For instance, if $\varphi$ is the sentence "$\forall x\exists y(x\in y)$," then a Skolem function for "$\varphi$ holds in $A$" should be a function $f: A\rightarrow A$ such that $$\forall x\in A[ x\in_A f(x)].$$ So "$A\models\varphi$" will in general have the form "$\exists f: A\rightarrow A [. . .]$." 
The problem is that if we try to similarly define truth for a proper class structure - say, all of $V$ - then we're left with a formula of the form $$"\exists f: V\rightarrow V[. . .]"$$ Such an $f$ is a class function - basically, a proper class. But we can't quantify over classes, so this formula isn't actually something we can express.
So this explains why the standard construction of a truth predicate breaks down for proper class-sized structures. But how do we know such a definition can't exist at all? Maybe there's some other way to get one.
Well, this is exactly what is ruled out by Tarski's theorem on the undefinability of truth! The proof of Tarski's theorem is the following: such a definition would let us define, via a formula $\varphi$, the set of (Godel numbers of) sentences which are true in $V$. We can now use the Diagonal Lemma to write a sentence expressing, roughly, "I am not true" which clearly isn't something we can do.
Which brings us to your final question: why doesn't our ability to define truth predicates for set-sized structures contradict Tarski's theorem? The answer is that we can happily build a truth predicate for a structure $A$, as long as we're content to do so outside the structure $A$. For instance, if we expand $V$ to have a constant naming the set of Gödel numbers of sentences true in $V$, the resulting structure $V^*$ clearly defines a truth predicate for $V$. However, since the sentence defining "truth in $V$" in $V^*$ is not a sentence in the language $\{\in\}$, we can't use the Diagonal Lemma to get a contradiction. Set-sized structures are "far from" $V$, so $V$ can build truth predicates for them.
A: What you cannot define according to Tarski is not just truth in some model of $\mathcal L$, but truth about the actual set-theoretical universe in which your truth-predicate is itself evaluated.
You can't do that with the usual machinery for reasoning about models, because the usual recursive truth function would require you to recursively define a function $F$ such that among other things, if $\varphi(x)$ is a model with one free variable,
$$ F(\ulcorner \varphi\urcorner) = \{ Y \in \mathbf V \mid (\mathbf V,\in,x\mapsto Y)\vDash \varphi(x) \} $$
But if $\varphi$ is true too often, the thing on the right of this may be too large to be a set at all -- so certainly it cannot be the value of some function applied to a representation of $\varphi$.
