A truth definition, wrong, but where Consider the theory ZFC of language with connectives $\neg$, $\rightarrow$, predicative symbol $\in$ and quantifier $\forall$.
Assume that we are working in ZFC.  Let $\mathcal{V}$ be the class of all set.  It is well-known that the notion of satisfaction "$\mathcal{V} \models \varphi$" cannot be defined.  My question is "where does the obstruction lie?".  To be specific, let me proceed in some detail.
An assignment is any function whose domain is the set of all variables.  Suppose that $s$ is an assignment and $x$ is a variable.  Then $s(x|\alpha)$ is an assignment which is the same with $s$ but the value $\alpha$ at $x$.


*

*For any assignment $s$, variables $x$ and $y$, define $\mathcal{V} \models_s x \in y$ if $s(x)$ is an element of $s(y)$.

*$\mathcal{V} \models_s \neg \varphi$ if $\mathcal{V} \not \models_s \varphi$ for every (formal) formula $\varphi$.

*$\mathcal{V} \models_s (\varphi \rightarrow \psi)$ if $\mathcal{V} \not \models_s \varphi$ or $\mathcal{V} \models \psi$.

*$\mathcal{V} \models_s \forall x \varphi$ if for every $\alpha$, $\mathcal{V} \models_{(s|\alpha)} \varphi$

*We define $\mathcal{V} \models \varphi$ if $\mathcal{V} \models_s \varphi$ for every assignment $s$.


(where $\mathcal{V} \not \models$ is an abbreviation for "not $\mathcal{V} \models$".)
It seems that "$\mathcal{V} \models $" has been succesfully defined.
Where is the first flaw, if any?
Reading comments, I feel like it will be helpful to make a statement so that it can be tested correct or not. 
Let $F$ be the set of all formulas.
By the recursion theorem, for every assignment $s$, there is a function 
$T_s: F \longrightarrow \{0, 1 \}$ 
with the properties


*

*$T_s (x \in y) = 1$ if and only if $s(x) \in s(y)$.

*$T_s (\neg \varphi)$ if and only if $T_s (\varphi) = 0$.

*$T_s (\varphi \rightarrow \psi)$ if and only if $T_s (\varphi) = 0$ or $T_s(\psi) =1$.

*$T_s (\forall x \varphi)$ if and only if for every $\alpha$, $T_{s(x|\alpha)} \varphi =1$.

 A: It seems that you are trying to inductively defined a class of the form $S = \{(\phi, \vec{x}) : \phi \in \text{Form} \wedge \vec{x} \in V^{\omega} \wedge V \vDash \phi(\vec{x})\}$. The trouble in formalizing this induction within ZFC is in step four. Assigning a truth value to $(\forall v)\phi(v)$ requires checking $\phi(x)$ for all $x \in V$. There is no way to formalize this in ZFC via the usual transfinite induction scheme - Whatever fixed iterative defined function you use can be diagonalized against. Although, one can formalize satisfaction if you are willing to restrict yourself to $\Sigma_n$ formulas. I think Kanamori has some remarks on this in the introductory chapter of his book.
A: Here I attach an answer because, although there had been a successful answer, it have takes me some time to recognize what is really a problem to proceed with the argument when we deal with a model which is possibly a proper class.
When we define the notion of satisfaction, with a model with a universe which is a set(anyway, the phrase 'with a universe which is a set' is actually redundant because my the term 'model' we always mean a set. This time, however, for emphasis.) we usually do the same thing.
However, there is still a problem of definiteness with the argument.
We cannot give a 'formula' which defines satisfaction because, we may need higher nested quantifiers to cover more complex formulas.
To resolve this problem, that is, to apply recursion theorem properly, we need to deal with the powerset of the set of all possible assignments as a codomain of the recursion.


*

*$h(x \in y) = \left\{ s: \textrm{assignment}| s(x) \in s(y) \right\}$ for each pair of variables $x$ and $y$.


...


*

*$h(\forall x \varphi) = \left\{ s: \textrm{assignment}| \textrm{for ever $\alpha$ in the universe, $s(x|\alpha) \in h(\varphi)$ } \right\}$


Here, you can see the problem occurs when the universe is a proper class.
There is no such a function $h$.
