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