TITLE: Ultrafilters and the exposition of forcing
QUESTION [8 upvotes]: 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.

REPLY [4 votes]: 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.
{"set_name": "stack_exchange", "score": 8, "question_id": 94929}