My mind is getting a bit twisted with notions relating to formalizing $\vDash$ for sets and classes in the $ZFC$. The end result I believe is:
For sets $A$, we may formalize $\vDash$ in $ZFC$ (and a fragment of it), and we may make statements such as $ZFC \vdash \forall \varphi \in T(A \vDash \ulcorner \varphi \urcorner)$ (where $T$ indicates some godelized set of sentences such as $ZFC$)
Moreover, in the metatheory it is fairly easy to prove that for every formula $\varphi$, $ZFC \vdash (A\vDash \ulcorner \varphi \urcorner) \iff \varphi^A$ (has to be in the metatheory since we're quantifying over actual formulas).
But the same cannot be done for proper classes. For proper classes, the best we can do is stick to relativizations $\varphi^M$ for a proper class $M$. The reason given is "due to Tarski's indefinability of truth". I have multiple questions here:
So if I naively replicated Tarski's recursive definition of truth anyway and tried to define $M \vDash \varphi$ in $ZFC$, using basically the exact same technique as for sets, what goes wrong? I'm guessing it has to do with the fact that we're quantifying over a proper class. But when we have a single proper class $M$, what's the problem? I realize we can't do $\forall M$ (where $M$ proper classes), but what's the problem with saying $\forall a \in M$ (that is, $\forall a M(a)$ where $M(x)$ is the defining formula for $M$) to help define $\vDash \forall x \varphi(x)$? Does it have to do with the fact that recursions have to happen on set like and well founded relations?
Given formulas $\varphi$, the relativization $\varphi^M$ is defined recursively. So again, fixing $M$ proper class, what's stopping us from talking about $\ulcorner \varphi^M \urcorner$, and for instance, saying $ZFC \vdash \forall \varphi (ZFC(\varphi) \rightarrow \ulcorner \varphi^M \urcorner)$. I have the feeling this is a dumb question but I would appreciate it nonetheless. Edit: Nevermind, $\ulcorner \varphi^M \urcorner$ is just a number and just $ZFC \vdash \ulcorner \varphi^M \urcorner$ doesn't make sense without an accompanying $\vDash$ somewhere. Yep that was indeed stupid.
Finally, so Tarski's indefinability of truth, at a high level, is why we can't define the relation $\vDash$ on proper classes. Shouldn't the same apply for sets? Meaning, why doesn't the fact that we can define $\vDash$ for sets contradict Tarski's indefinability of truth.