I’m trying to work through the forcing relation in set theory and the independence proof of GCH in particular. Although I feel like each step locally makes sense, I’m a bit confused about the necessity of some of the last steps which makes me think I’ve misunderstood something fundamental about the strategy. My understanding of the high-level argument is:
- Take a countable transitive model of ZFC M and take a generic ultrafilter G over some suitable Poset in M
- Show that the extended model M[G] is also a model of ZFC and that M can prove this
- Even though M cannot “see” G, by use of Names and the forcing relation we can prove that there is some element p in G such that M proves that, for any generic ultrafilter G’ containing p, the sentence we want to force is true in M[G’].
- So M proves that the sentence we want to force is in fact consistent with ZFC
Maybe this is a misunderstanding on my part, if so happy to be corrected here!
If that’s largely accurate though, I guess I’m confused why we need to prove so much about what M can prove about M[G] from its own “perspective”. Intuitively it seems enough that we can see “from the outside” that if M is a model of ZFC then so is M[G], and so the Names/forcing relation steps seem confusing to me - I’m not seeing the necessity of proving that all of this is provable from within our original model.