From I know so far, there are two different approaches to independence proofs: Forcing and constructing Boolean models via Boolean Algebras. I’m quite familiar with Boolean algebras (up to representation theorem but not Boolean Spaces) and I’ve $4$ different questions:-
Which topics will I need in order to study independence proofs but are not covered in Enderton’s? (for example, I’ve heard that I will need to know about Martin’s axiom)
Which approach do you recommend to first study independence proofs? Forcing or Boolean models? and why?
If you do recommend forcing, Which texts do you recommend to study from? given that this is self-study so it will be better if the book is self-contained and develop the topic more slowly than as if there were an instructor.
If you do recommend Boolean Models, Which text do you recommend? What about “Simplified Independence Proofs” by Rosser?
I’m not sure what is covered in Enderton’s book, so I will just assume that it was the basic set theoretic introductory material, and answer according to that. Your mileage may vary according to what you actually know.
To study and understand independence proofs you need to be comfortable with several things:
Basic logic, namely the completeness theorem and very basic model theory. One exception is that you need to understand the basic mechanics of the incompleteness theorem, or at least Tarski’s theorem on the undefinability of truth.
Transfinite recursion and induction, and other well-founded inductions.
Basic order theoretic ideas, since forcing is about using partial orders correctly.
The distinction of working “inside” a model and “outside” a model. This can be seen as an extension of the Tarski’s theorem mention from before. But in reality this merits its own bullet. This distinction is supremely important for comprehending how these things work.
The construction of $L$, and other inner models like $L[A]$, $L(A)$ and $\rm HOD$-like models. You don’t need to know fine structure, or all the properties which are true in $L$ and so on. But you need to know what it means for something to be in $L$ or in $L[A]$. While we’re on the subject, the basics of absoluteness arguments are very useful as well (Mostowski, Shoenfield, Levy).
If you’re interested in $\sf AC$ related results, many can be formulated in the language of urelements or atoms (or equivalently, $\sf ZF-Reg$). These are a bit easier to wrangle at first, but they do necessitate some time for understanding how they work and eventually a lot more time to understand why this method is fundamentally different than (although strikingly similar to) the usual forcing+symmetries arguments.
Finally, it is not directly related to many of the basic proofs. But it is definitely going to come up as you progress along. Large cardinals are quite entangled with independence proofs. They allow us to measure the strength of independence of statements. For example, the failure of the tree property at $\aleph_2$ is provable in certain extensions of $\sf ZFC$. But if we knew that weakly compact cardinals are inconsistent, then we would know that it is provable directly from $\sf ZFC$.
I recommend forcing using Boolean valued models. Namely, you construct a Boolean valued model and use a generic filter. The reason is that it becomes very enlightening to understand that a forcing is really just approximating truth values of statements. It is a very neat and very clever way to look at things.
However, it is nearly impossible to work with. It’s much easier to describe the conditions as actual approximations of the objects that you’re trying to build, rather than some abstract set of truth values. In fact, it is so much handier, that in many cases we neglect the notion of partial order completely. Opting instead to work with quasi-orders (e.g. it is incredibly easier to understand iterated forcing when it is given as a quasi-order, rather than a complete Boolean algebra).
Regardless to this, it is important to understand the Boolean valued model construction. It is also important to understand that every quasi-order induces a quotient partial order, which in turn induces a quotient separative partial order, which in turn has a unique completion to a complete Boolean algebra. And forcing with either one of these objects gives us the same results.
The above equivalence is useful, and it sits on the edge between actual forcing and Boolean valued models. Two forcings are equivalent if the Boolean algebra they induce [as above] is the same, which means that understanding the Boolean algebra means understanding the forcing, in some sense, and vice versa. I think that Boolean valued models are a great way of understanding the Boolean algebra better. It might be a bit advanced at this point, but Solovay’s theorem about the consistency of having a real-valued measurable cardinal [assuming the consistency of a measurable cardinal] is a perfect example for that.
For forcing, I’d take Halbeisen’s “Combinatorial Set Theory” book (which is available freely as a preprint on the author’s website!) that also includes a lot of the other things I’ve mentioned so far.
I can also recommend Jech’s “Set Theory” as a good place to learn about Boolean valued approach to forcing, but ultimately he goes to partial orders and I wasn’t very clear as to how it works. But once you have the idea down, getting used to Jech is a hearty recommendation, since the book is a very useful reference. It’s easier if you have someone to help you step through Jech, so if you don’t have a guide at this point, it might be worth putting this on hold until you develop a stronger intuition about forcing.
One point for Jech, however, is that he wrote two very good books “Multiple Forcing” and “The Axiom of Choice”. Both should be read once you have the basics of the technique down. The first one covers the basics of forcing, include several important examples and several important extensions (products, iterations, proper forcing). The second book is a great start for independence proof related to the axiom of choice, with atoms and with symmetric extensions.
I haven’t read Rosser’s book, so I can’t evaluate it. But I’ll point out again that the Boolean valued models is an approach which is more “logic oriented” where you want to work in a universe and say things about your theory from within that universe. It can be used to formalize all sort of arguments related to forcing within weak arithmetic theories, which is great. But I don’t think it’s the first point one should focus on when learning forcing, and I think that if one is ultimately interested in choice related results, forcing is more important than Boolean valued models.
About Martin’s Axiom, let me share a minor insight I have now, three years after the comments mentioned by Martin. I think it’s confusing if forcing does not sit right. In general forcing axioms are very important, and the consistency of Martin’s Axiom is very important, both as an example for iterated forcing and for a bunch of independence results that follow from it.
So you either do it before talking about forcing at all, or only after forcing sits right. If you do it half-assed, the result can be literally damaging to your understanding of forcing and forcing axioms.
For forcing I recommend “Set Theory:An introduction To Independence Proofs” by Kunen, which is self-contained, and has a whole chapter (out of 8 chapters) om Martin’s Axiom.And a great set of exercises and problems. Also “Lectures In Set Theory”, edited by Morley, as a supplement.