Stealing the idea from @mathemensch, I want to start a 'Simone learns forcing' thread. It is going to be extremely non-linear, and I will probably drop it after the first day. Also, I might be very wrong about things, so if you're willing to read through this, be careful.

Day 1: we begin at chapter VII of Kunen's Set Theory. Some notation is needed, mainly because set theorists tend to give fancy names to things. A 'forcing notion' is going to be a poset P, usually assumed to have a maximal element 1. A '(forcing) condition' is any p \\in P.

We will often use the wording "enough ZFC". This usually means that, since every derivation formally needs only finitely many axioms, we will always work under the assumptions that what we need of ZFC is true in our models.

Now, models is kind of a tricky word. You can't exhibit models of ZFC in ZFC (basically due to Goedelian phenomena) so what we will actually use is a baby/non-informative version of the reflection principle: we can find countable transitive models for finite portions of ZFC.

So we fix an effective enumeration of the axioms of ZFC, start with some countable transitive model (c.t.m.) M of *enough ZFC* and, inside ZFC, build a 'generic extension' N of M that may satisfy *less* axioms of ZFC than M, but has more interesting properties (e.g. \\neg CH).

One way to do so is through P-names. Now, the idea is that the people living in M (the ground model) may have never seen elements from the generic extension N, but can talk about them even if they don't know they exist. Think about God. We have *language* to speak about God.

The inhabitants from M have the language to speak about elements of the generic extension, and the way they do so is through P-names. A P-name is defined recursively as a *binary relation* whose elements are couples of a P-name and an element of P.

P-names form, if P is non-empty, a proper class, called V^P. We can work with M^P, which is the intersection of M and V^P or, equivalently, the set of "things that are P-names if you ask the people from M". Each P-name can be valued, once again recursively.

We need to fix a non-empty filter G in P. We can value a P-name x at G by taking the set of all valuations of P-names y at G for which there exists a p \\in P such that (y,p) \\in x. This opens a world of new possibilites, by using machinery such as generic filters.

This is a lot to think about, so I think I'll stop right after defining what will be the generic extension N. We call it M[G], and it's the set of all valuations at G of P-names from M^P. I try to think about this as considering all elements of a certain model that are [...]

[...] type-definable in a smaller model. There might be an analogy P-names/types, but I'll need to think more about it. [end of Day 1]