Some $\Pi^1_1$ sentences are elementary Johan van Benthem showed that a $\Pi^1_1$ sentence of the form $$ \forall \bar P \forall \bar x \phi(\bar P,\bar x), $$ where $\bar P$ and $\bar x$ are second-order and first-order variables, respectively, and $\phi$ is a quantifier-free formula, is actually equivalent to a first-order sentence.  In his book Modal Logic and Classical Logic, he uses the Keisler-Shelah theorem and the following lemma to prove this.  Here, $W$ is the domain of the ultraproduct.
The idea behind the use of the set $B$ is not clear to me.  What good does it do?  Apparently it is used to ensure Condition (ii), but I do not understand how exactly $B$ is used to derive it.  
It resembles a common argument for ultraproducts where you look at the diagonal, but I'm not sure.  My confusion may have arisen due to the fact that he may be using symbols $f^1, \dots, f^n$ for two different things: as something he fixes at the beginning and as "bound variables" that define conditions and sets.  Also, it may be related to the subtle point of whether he fixed elements of $W$ first and picked representatives $f^1, \dots, f^n$, where the problem of well-definedness could arise, or he fixed $f^1, \dots, f^n$ before taking a quotient to form $W$.
 A: In order to get (ii), one needs the predicates $Y^i_j$ on $F_i$ to be properly connected with the predicates $Y_j$ on the ultraproduct $F$. Before I spell out what "properly connected" means, let me avoid a lot of sub- and super-scripts by assuming that there's only one $Y$ and it's a unary predicate; everything I say will extend to the general case by just adding a lot of sub- and super-scripts. Now "properly connected" means that, for each of the $n$ functions $f^j$, we want $Y^i(f^j(i))$ to hold (in $F_i$) if and only if $Y(f^j)$ holds in $F$. (This will be an essential part of the basis case in an induction on $\beta_k$ proving (ii).) But there's a problem getting this "properly connected" situation: What if, for some $j$ and $r$, we have $Y(f^j)$ true and $Y(f^r)$ false (so we also want $Y^i(f^j(i))$ true and $Y^i(f^r(i))$ false) but $f^j(i)=f^r(i)$? We can't have $Y^i$ being true and also false at one and the same element. Fortunately, the problem isn't very serious. In the problematic situation, we have $f^j\neq f^r$ as elements of the ultrapower $F$, and so $f^j(i)\neq f^r(i)$ for $U$-almost all $i$. As long as we choose $i$ among these good ones, the problem disappears. And $B$ is precisely the set of $i$'s that are good in this sense.
