How EXACTLY does Tarski's undefinability of truth interfere with defining $\vDash$ for proper classes, and why doesn't it do so for sets? 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.
 A: I think you have things pictured a bit off. (In order to talk freely about classes, the following analysis takes place in $\mathsf{NBG}$ for simplicity; as usual, this can be "$\mathsf{ZFC}$-ified" straightforwardly at the cost of making all the statements annoyingly circuitous and only applicable to definable classes.)
Below, unless stated otherwise "structure" will mean "transitive set or class containing $\mathsf{HF}$ as a subset thought of as an $\{\in\}$-structure." The requirement that $\mathsf{HF}\subseteq M$ is really just an overkill way of guaranteeing that Godel coding works properly; if you prefer, you can instead demand that $M$ satisfy some very weak set theory like $\mathsf{KP}$ (which will in fact imply containment of $\mathsf{HF}$ but may feel more natural).

The set/class distinction really doesn't interact with Tarski at all. Tarski's undefinability theorem applies to every structure, class- or set-sized:

Suppose $M$ is a transitive set or class with $\mathsf{HF}\subseteq M$, thought of as an $\{\in\}$-structure. Then $Th(M)$, thought of as a subset of $\omega$ in the obvious way, is not parameter-freely-definable in $M$.

The size of $M$ plays no role; what Tarski does, regardless of the size of $M$, is limit where a parameter-free definition of $Th(M)$ can take place. For example, we have:

Suppose $M,N$ are set-or-class-sized structures with $M\subsetneq N$. Then Tarski's theorem does not immediately preclude $Th(M)$ from being parameter-freely-definable in $N$.

The only special thing about $V$ is that there is no "outside" we can go to to get a parameter-free definition of truth. But that's the only way $V$ differs from a set-sized structure here. Indeed, with set-sized structures there are very simple ways of "going outside to get the theory" without even going to the level of proper-class-sized structures! For example, suppose $M\subseteq N$ are set-sized structures. Let $M_N$ be the expansion of $N$ by a new unary predicate $U$ with $U^N=M$. Note that $M_M$, while not literally the same structure as $M$, is biinterpretable with $M$ so this doesn't always give us more power. However:

For every set-sized structure $M$, we have $Th(M)$ is parameter-freely-definable in $N_M$ where $N=V_{height(M)+1}$.

This is massive overshooting actually, but it makes the necessary point. And the reason this doesn't work for proper-class-sized structures is simple and has nothing to do with Tarski: if $M$ is a proper class, there is no "level of the cumulative hierarchy above $M$".
(Incidentally, it's not immediately clear to me whether we actually need to expand the language!)

This leaves us with one major interesting question remaining: when is the theory of a class-sized structure parameter-freely-definable in $V$? As noted above, Tarski says nothing directly here for classes other than $V$ (or other than minor modifications of $V$). In fact, there is a simple example of a proper-class-sized structure whose theory is parameter-freely definable in $V$: the class of ordinals, $\mathsf{Ord}$. This is vastly less complicated than one might expect, and its theory is in fact parameter-freely-definable in $(\mathbb{N};+,\times)$ alone!

*

*OK, $\mathsf{Ord}$ doesn't fit our picture since $\mathsf{HF}\not\subseteq\mathsf{Ord}$. Perhaps a better thing to look at is what I'll call "$\mathsf{HF(Ord)}$," the class-sized structure gotten by closing $\mathsf{Ord}$ under pairing. This is now significantly more complicated - it interprets true first-order arithmetic for example - but still extremely simple compared to other structures in the context of set theory, and in particular its theory is still parameter-freely definable in $V$.

