I am beginning to read a paper called "Well-Founded Boolean Ultrapowers as Large Cardinal Embeddings" by Joel David Hamkins and Daniel Evan Seabold. In the first section, they review the method of forcing using Boolean-valued models. The authors write that "there is NO need for the ultrafilter $U$ to be generic in any sense" in order to develop the theory from this section, and I'm having trouble understanding why this is the case. In particular, it is shown (lemma 8) that the assertion that $\dot{G}$ is a $\check{V}-$generic filter on $\check{\mathbb{B}}$ has Boolean value $1$ and that (lemma 10, Łoś lemma) if $\mathbb{B}$ is a complete Boolean algebra and $U$ is any ultrafitler on $\mathbb{B}$, then $V^\mathbb{B}/U\vDash\phi[[\tau_0]_U,…,[\tau_n]_U]$ if and only if the Boolean value for $\phi(\tau_0,…,\tau_n)$ is in $U$. If $G$ were not generic, and $G\in V$, then $G^c=\mathbb{B}\setminus G$ would be dense in $\mathbb{B}$ and it would seem that these lemmas would show that $G\cap G^c$ is nonempty. I can provide some of my thoughts below and hopefully someone can point out what details I am misunderstanding. For clarity, I'll write the Boolean value of a sentence $\phi$ as $[[\phi]]$.
I follow Lemma 8, which is proved by assuming that $D\in V$ is a dense set in $\mathbb{B}$ and arguing that $[[\check{D}\cap\dot{G}\neq\emptyset]]=\Sigma_{b\in D}[[\check{b}\in\dot{G}]]=\Sigma_{b\in D}b=1$. I believe that my confusion lies in applying Łoś lemma to this statement to get that $G$ intersects $D$ in $V^\mathbb{B}/U$. Because Łoś lemma relies on fullness, we can pick some antichain $\check{A}$ in $\check{D}$ and mix over $\check{A}$ to produce some $\dot{d}$ with $[[\dot{d}\in\dot{G}]]=1$. In the inductive proof of Łoś lemma, to show that $[[\dot{d}\in\dot{G}]]=1\in U$ implies $V^\mathbb{B}/U\vDash[\dot{d}]_U\in[\dot{G}]_U$, we could argue that because $A$ is an antichain, the fact that $U$ is generic means it chooses one element of $A$ and collapses $\dot{d}$ to some particular element of $D$, making the satisfaction claim true. However, if $U$ is not generic, it need not meet $A$ (or, if we try to run the same argument to show that $G$ meets $A$, then we regress infinitely and continue to beg the question), so $[\dot{d}]_U=\emptyset$, which does not allow us to conclude the satisfaction claim.
If someone could point out what I'm missing that would be great!
Best Answer
As mentioned in the comments, the Łoś lemma is fine... the issue is you're identifying $[\dot G]_G$ with $[\check G]_G$ when that doesn't hold unless $G$ is generic. It is true that we have $[\check b]_G\in_G [\check G]_G$ iff $[\check b]_G \in_G [\dot G]_G$ (iff $b\in G$), but that doesn't suffice for equality.
We can calculate $$ ||\tau\in \check G || = \sum_{b\in G}||\tau=\check b|| \\||\tau\in \dot G|| = \sum_{b\in B} b\cdot ||\tau = \check b||.$$ If $G$ is generic, then either of these sums being in $G$ implies that one of the terms is in $G$, which amounts in both cases to $||\tau = \check b||\in G$ for some $b\in G,$ so it's true then. (Of course, in this case everything is trivial: the Boolean ultrapower embedding is an isomorphism and the entire forcing extension collapses to $V$.)
For an explicit check that these aren't equal, consider $B=P(\mathbb N)$ and let $G$ be a non-generic (i.e. non-principal) ultrafilter. Let $b_0,b_1,\ldots$ be a countable sequence of elements of $G$ such that $i\notin b_i.$ Then let $\tau$ be the mixture with $||\tau = \check b_i|| =\{i\}$. Then we have $\sum_i ||\tau = \check b_i|| = 1,$ but $b\cdot ||\tau = \check b|| = 0$ for all $b\in B.$ So $||\tau \in \check G|| = 1$ and $||\tau \in \dot G || = 0.$ And we don't have containment in the other direction either: let $\tau$ be the mixture with $|| \tau = \check{\{i\}}|| = \{i\}.$ Then $||\tau =\check b|| = 0$ for $b\in G,$ but $\sum_i \{i\}\cdot ||\tau = \check{\{i\}}|| = 1,$ so $||\tau \in \check G || = 0 $ and $||\tau \in \dot G|| = 1.$
One might reasonably wonder how the seeming non-triviality in this case squares with the well-known fact that you don't get anything new by forcing with an power-set algebra. The Boolean ultrapower $\check V_G$ (i.e. $V^B/G$ restricted to equivalence classes of names with $||\tau \in \check V|| =1$) in this case is just isomorphic to the regular old ultrapower of $V^{\mathbb N}/G,$ and the elementary embedding $j: V\to \check V_G,$ $x\mapsto [\check x]_G$ corresponds to the standard ultrapower embedding.
By elementarity, $j(B)$ will be the power set of $\mathbb N$ in $\check V_G.$ The full quotient $V^B/G$, as it turns out, behaves exactly over $\check V_G$ as the forcing extension behaves over the ground model classically (with $[\dot G]_G$ playing the role of the generic), so we see a boring old power set and get triviality: $\check V_G= V^B/G$. So indeed, we don't get any difference from the ground model on what sentences hold, since $V$ embeds elementarily into the "forcing extension".
We can also see clearer the difference between $\dot G$ and $\check G$ (in this particular case). The fact that it's generic over a power set algebra says $[\dot G]_G$ must be a principal ultrafilter, which in this case must be generated by a nonstandard element of $\mathbb N^{\check V_B}$. In fact, by the above, we should have $||\dot G\in \check V||\in G$ so we expect it's a mixture of check names, and in fact it's not hard to see it is just the mixture $||\dot G = \check U_i || = \{i\}$ where $U_i$ is the principal ultrafilter generated by $i$. On the other hand, $[\check G]_G = j(G)$ is by elementarity a nonprincipal ultrafilter on $\mathbb N^{\check V_B}.$