Ultrafilters and the exposition of forcing I've just been reading Timothy Chow's "A beginner's guide to forcing."  
Question: Does an exposition of forcing really need to delve into ultrafilters?
What I have in mind:  If ZFC proved CH, the proof would apply to any Boolean-valued model M, giving CH the truth value 1 in M.  Doesn't that mean that one has proved the independence of CH as soon as one has any Boolean model where CH as truth value less than 1?  And if one then, psychologically speaking, still really wants a 2-valued model where CH fails, already having independence, one need only appeal to Godel's completeness theorem.  
 A: If you only want independence of CH, then yes, exhibiting a Boolean-valued model where CH gets value $\ne1$ is perfectly sufficient. Moreover, if we consider the construction of the Boolean-valued model as a syntactic interpretation, the verification that theorems of ZFC hold in the model can be done in a purely syntactic way, hence one obtains easily a proof of consistence of ZFC${}+\neg$CH relative to ZFC in a weak fragment of arithmetic.
On the other hand, if you are interested in the actual models of set theory, then the approach via Gödel’s completeness theorem is not quite satisfactory, since it breaks the salient features of the construction ($M[G]$ is an end-extension of $M$ with the same ordinals). Also, for statements more complicated than CH, it is often easier (more intuitive) to verify that the statement holds in $M[G]$ than directly computing Boolean truth values.
A: I just thought I would pop in here and start an argument by adding my category-theorist's point of view.  (-:
To a category theorist, a Boolean-valued model is the internal logic of a sheaf topos.  Explicitly computing Boolean truth values is the same as working with subobjects in that category, while "jumping inside the Boolean brackets", as Andreas describes, corresponds to working inside the internal logic.
Now a sheaf topos is always the "classifying topos" of some geometric theory, which means that it contains a "generic model" of that theory.  In the case of sheaves for double-negation topologies on posets, which classical forcing usually restricts itself to, these models can be described as ultrafilters.
But I think there is value, especially expositionally, in taking seriously the idea that we are talking about classifying toposes of more general theories than this, and that what we obtain from forcing is a generic model of some theory.  Even if having such a generic model is equivalent to having a certain kind of ultrafilter, it seems to me that often the generic model of the theory has a more direct connection to the statements we are trying to force.
For instance, to force $\neg \mathrm{CH}$, we may start with the "theory of an injection $\alpha \hookrightarrow 2^{\aleph_0}$" for some uncountable $\alpha$.  The classifying topos of this theory will then contain such the "generic" such injection.  (We then have to pass to an extra subtopos if we want, unaccountably, to preserve PEM.)  I find this idea much easier to understand as a beginner, though it is of course equivalent to the usual presentation.
In short, I think one should be able to work with generic objects, which one might argue are at the heart of forcing, without necessarily needing to think about ultrafilters in particular.
A: As Joel and Emil have already explained, one can get perfectly correct consistency proofs by directly computing Boolean truth values, without using a generic ultrafilter.  I've found, however, that those direct computations tend to be rather tedious, and that the most convenient way (for me) to carry them out consists of three steps: (1) Show that (first-order) logical deduction preserves the property of having Boolean truth value 1.  (More generally, if $\phi$ is a logical consequence of some hypotheses $\psi_i$, then $\Vert\phi\Vert$ is $\geq$ the meet of the $\Vert\psi_i\Vert$ in the Boolean algebra.)  (2) Show that certain fundamental facts have Boolean value 1.  (3) Deduce (in first-order logic) whatever other information I need from those fundamental facts.  Now, what should the "fundamental facts" in item (2) be?  Among others (like the ZFC axioms, the fact that the Boolean copy $\check V$ of the ground model is a transitive class containing all ordinals, etc.) there is the fundamental fact that a certain element $\dot G$ of the $B$-valued universe is a $\check V$-generic ultrafilter in $\check B$.  So, even when I'm "officially" computing Boolean truth values, I'm still (in part (3) of the process --- parts (1) and (2) are done once and for all, as they're the same for all Boolean algebras) talking about an ultrafilter generic over the ground model.  In fact, I'll go further and claim that, even when people explicitly write out Boolean truth-value computations, without any sign of my 3-step process, they're usually still thinking in terms of generic ultrafilters.
A: Your proposed ultrafilter-free proof is fine. Once you know that statements hold with Boolean value exceeding a given nonzero value $b$ in the Boolean algebra $\mathbb{B}$, then it is easy to see that this theory of all assertions having value at least $b$ is consistent, and so yes, there is a model of this theory by the completeness theorem. 
In the ultrafilter proof, the ultrafilters in the Boolean valued model are used to transform the Boolean-valued model to a classical 2-valued model.  The quotient of any Boolean-valued model of a theory gives a first-order structure satisfying any statement whose Boolean value is in the ultrafilter. My perspective is that this quotient process is illuminating of the connection between the Boolean valued model and the resulting quotient model. For example, if $U$ is an ultrafilter on a complete Boolean algebra $\mathbb{B}$ and $V^{\mathbb{B}}$ is the $\mathbb{B}$-valued universe, then the quotient process actually provides an elementary embedding $$j:V\to \bar V\subset\bar V[G],$$ called the Boolean ultrapower embedding, where $\bar V$ is the Boolean ultrapower and $G$ is $\bar V$-generic. The entire embedding and the class $\bar V[G]$ exist as classes in $V$ definable from $U$ and $\mathbb{B}$. The case in which $\bar V$ is well-founded is extremely interesting, for this has large cardinal strength, and the Boolean ultrapower reveals the two central concepts of forcing and large cardinals to be two facets of the same underlying construction, the Boolean ultrapower. (I am currently writing a paper with Dan Seabold on the topic of well-founded Boolean ultrapowers, due out soon, but you can see the lecture notes from my tutorial An introduction to the Boolean ultrapower, which I gave last year at the Young Set Theorists Workshop in Bonn.) 
The ultrafilter-free proof ignores this connection between the ground model and the resulting model. If you include the diagram of the ground model in your theory, however, then one can prove that the Boolean ultrapower is implicit in your construction (and it will provably be a factor of the embedding that takes each object to its interpretation in your model). 
Also, there is a sense in which the ultrafilter-free proof doesn't save any logical strength, since the completeness theorem on which it relies is equivalent to the existence of ultrafilters. For example, if $F$ is any filter on a power set $P(X)$, then one may consider the theory in the consisting of the diagram of $\langle X,A\rangle_{A\subset X}$, with a constant for every element of $X$ and a predicate $A$ for every subset $A\subset X$, and the assertions about which elements are in which subsets. Now add a new element $c$ to the language and the assertions that $c\neq a$ for each $a\in X$ and $A(c)$ for each $A\in F$. This theory is finitely consistent since $F$ is a filter and hence it is fully consistent. So by the completeness theorem it has a model, and the set of $A$ for which $A(c)$ in this model is an ultrafilter extending $F$. 
