The satisfaction relation is undefinable, but does it still "exist"? In Jech's book "Set Theory" chapter 13, he shows how the satisfaction relation $\models_{n}$ for $\Sigma_n$ formulas can be formalized in ZF.  As he pointed out previously, the full satisfaction relation cannot be formalized in the first order language of ZF.
I started thinking about what goes wrong in trying to define the union over $n\in\omega$ of these $n$-satisfaction relations.  Could someone shed some light on whether or not one of the following is correct, or if I'm just missing something else?
Option 1: The problem with defining the union is that these are classes, and one cannot take an infinite union of classes, in general, as there is no (first order) formula describing their union.
However, it seems to me that the collection of sentences in $Form$ of complexity $\Sigma_n$ that satisfy $\models_n$ form a set.  Taking a countable union of sets is no problem.  So I'm thinking that option 1 is not quite the whole picture.
Option 2: When we say that $\models_n$ is formalizable, the $n$ is a meta-language-natural number.  So there is no way to "collect" the classes along these meta-naturals.
Option 3: There is some way to form the union, in a way definable in ZF [which I don't see], but $V$ doesn't see [from its perspective] this union as forming a satisfaction relation.
Any further explication on these issues would be appreciated.
 A: Option 2 is exactly what is going on.  For each meta-language natural number $n$, we can write down a formula in the language of set theory that formalizes $\vDash_n$.  However, we cannot define a function on $\mathbb{N}$ which takes $n$ to this relation $\vDash_n$ for all $n$ at once.
This is related to Option 1.  Note that if we were defining the satisfaction relation (in the language of $\in$) on some set $U$, we could define $\vDash_n$ by recursion on $n$ (or more naturally, we could define $\vDash$ on all formulas by recursion on the complexity of the formula).  Indeed, this is exactly what we do in ordinary model theory, when we define the satisfaction relation for some first-order structure (whose underlying set really is a set).  But a recursive definition involves quantification over the initial segments of the recursion, so this does not work for $V$, since $\vDash_n$ is a proper class and not a set in that case and we can't quantify over classes.  Note that while there is only a set if we restrict to sentences, we need to define satisfaction of formulas with free variables (for a given assignment of values to those variables) in order to define satisfaction of sentences.  For instance, to say whether $\forall x\varphi(x)$ is true, we need to already know whether $\varphi(a)$ is true for each $a\in V$.
