§ Forcing machinery
- Let be a countable mode of ZFC (exists by lowenheim skolem).
- Let ( for subobject classifier).
- Take to be the set of partial functions from with finite support
- Note that elements of can be thought of as finite lists, where we know the values where they are 0, where they are 1.
- Also note that elements of can be arranged in an obvious partial order.
§ Ideal of a post
- We define an ideal to be a set of elements which are pairwise compatible (all pairs of elements have a union), and is downward closed (all elements with less information is present in the ideal).
- More formally, for any and , if , then . So .
- For every , there is some such that ( is a directed set).
§ Maximal ideal
- A maximal ideal is an ideal such that for any , either is incompatible with , or is in .
§ Density in a poset
- A subset of a poset is dense iff for any , there is some such that . Intuitively, at any point in the poset, it is possible to "add more information" to reach .
§ Generic Ideals
- We say that an ideal is generic iff for all dense .
- For any countable model , and a poset over it, We claim that for any , a generic ideal which contains ( ) exists.
§ Proof: Generic ideal always exists
- We wish to find a generic ideal that contains a special .
- Let be an enumeration of the dense subsets of that are members of the countable model .
- We can perform such an enumeration because is countable, and thus only has countable many sets.
- We will create a new sequence which hits each .
- Start with .
- Since is dense, there is some such that . Set .
- This gives us a sequence .
- Build an ideal . That is, we build the union of all the lower sets of . So this can also be written as , where , the down set of .
- is downward closed by construction, and is directed because for any two elements , there is some such that , , and WLOG, if , then , thereby making the set directed.
§ Separative poset
- is separative iff implies .
§ Generic ideal of separative poset is not in the model
- Claim: if is a generic ideal of , then is not in .
- Let , . Consider the set .
- Intuitively, is the set of all elements of which are incompatible with some element of .
- We must have \in by
comprehension(M), since is a model of ahd is a susbet of .
- To see that is dense, for any element , we need to find an element such that . See that iff there exists some , such that
- Since is dense, we have that , This gives us some element such that
incompatible(g, p)for some .
- TODO: this makes no sense!
§ Definition of forcing
- An element forces the sentence iff is true for every generic ideal such that . For every formula , forcing tells us for which pairs of it is the case that is true. It is written as .
- Written differently, we say that forces , iff for any , is true.
- That is to say, we can decide the truth of by looking at the presence/absence of in .
- See that for a fixed , forcing gives us a relation .
- What we want to show is this that this forcing relation, for each , is definable in .
- This will show that the collection of that force a is in (project the first components of .
§ Fundamental theorem of forcing
- For every formula , for every generic ideal over :
- 1. Definability: there is a set such that ( forces ) if and only if . That is, the forcing relation is definable in
- 2. Completeness: is true iff there is a such that . That is, any true sentence in must have a witnessing which forces it, for any generic ideal .
- 3. Coherence/Stability: If , for all , we have . Truth once forced cannot be unforced, truth is inflationary, truth is stable, etc.
- The FTF (fundamental theorem of forcing) is an algorithm on the ZFC syntax. It takes a formula , and produces a ZFC proof of (1), (2), (3).
§ Architecture of FTF
§ Net to capture generic ideal
- If is a generic ideal of , and , then there is a , such that all such that are in . That is, .
- QUESTION: How can if is a proper class relative to , and is a subset of ? Isn't a superset of a proper class a proper class?
- Recalling that
(p, q) ∈ P are compatible iff
∃r ∈ P, p ≤ r ∧ q ≤ r. If no such
r exists, then
(p, q) are incompatible.
- Suppose we take some
(p, q) ∈ P. We can have
(1) p ≤ q,
(2) q ≤ p,
(3) (p, r) compatible,
(4) (p, r) incompatible. Consider:
\ / \
p d e
\ / |
p <= q
q <= p.
∃r, (p <= r, q <= r) compatible.
(p, e) incompatible.
- We wish to show that there is a such that all its extensions lie in .
- That is to say, all of the extensions of do not lie in .
§ Proof of net lemma
- To prove: If is a generic ideal of , and , then there is a , such that all such that are in . That is, .
- Let be the set of elements in that is incompatible with every element in :
- If were dense in , then an element would be the element we are looking for, where all the extensions of is in .
- Let's try to show that is dense. Let be arbitrary. We need to find a such that .
- If for every , then we are done, since , and thus .
- On the other hand, suppose there is a such that . That is, there is an such that .
- Now what? Now we make an observation: See that we can freely add into , because (1) if we consider , then . (2) could have an element . But this cannot happen, because this means that . But since is downward closed and , this means that , which is a contradiction as which has empty intersection with .
- TLDR: We can fatten up any set with , while not changing the result of !
- So we build , which is to say, .
- We claim that is dense. Suppose we have some . (1) for all , and thus and we are done. Otherwise, assume that there is some such that . then there is an , such that . This gives us an such that and we are done.
§ Simpler proof of net lemma (Unverified)
- Let .
- Let's now pick a concrete , and try to show that is dense. so we need to find a such that .
- Easy case: If has no extensions in , then by defn of ; we are done since , ahd thus density is fulfilled.
- Hard case: Suppose does have an extension , what then? How do I find an element of such that ? ( for extension)?
- Hard case: See that we will be using to consider to find an element whose every extension lies in . So suppose we add into (ie, ).
- While , we will still have that , because lies in , which has zero intersection with !
- Thus, we can throw in "for free" to fatten up to make it more dense, while knowing that will cull this portion.
- So define
- We claim that is dense.
- Suppose . If for all , , then . Otherwise, suppose . Then we have . Thus is dense.
- Let . Then we cannot have come from the portion of , since . This means that came from the first part of the set , where no extension of lies in . Thus we are done.
§ Intuition for Net definition
- A net could be defined in two ways: (A) , or (B) .
- It can't be (B), because (B) has a trivial solution !
- It should be (A), because (A) forces to be "non-trivial", since I can test it against all .
§ Names and name creation
- Let (for names) be defined transifinitely, where , , and take the union in the usual way at the limit ordinal.
- Intuitively, names let us create "hypothetical sets", which are realised into real sets for each subset . We keep those elements which are tagged by , and we remove those sets which are not.
§ Forcing equality
§ Step 1: Defining the forcing tuple set .
- to decide equality of , it is very sensitive to because elements can appear/disappear based on .
- We want all triplets where such that forces .
- Recall that forces means: if and only if .
- Thus, must be such that it is NECESSARILY POSSIBLY TRUE that every element must also be such that , and also vice verss: every must be such that .
- Let us prove the forward direction, where we want to force implies .
- Whenever , and , there must be an such that .
- We might be tempted to say that implies iff , but this is too strong. There could be many different collapses that allowed for . That is, we could have some , and forces .
- Now it looks like we need to define equality in terms of equality. We just perform induction on name rank, because to have , the name rank of must be lower than because we built the name rank universe by induction.
- So we define the condition on tripets of name rank less than to be that for ALL where , there is such that and ,
- So we define the relation by name rank induction.
§ Step 2: defining the net
- Next, we need to define the net .
- Let \}.
- Question: What is the meaning of the symbol in this context?
- SID: I guess is syntactic sugar for .
- See that is the set of all for which is possibly a subset or equal to .
- By the inductive hypothesis of name rank, FTF holds for and it follows that [I have no fucking idea what this means ].
§ Step 4: The equivalence of net, modality, relativized inclusion:
Therefore, all these conditions are equivalent.
- We will show that implies that . This by the net lemma will implu that there is a such that all larger elements will be trapped in the net .
- Then we will prove that if there is such a which traps elements in the net, then we have .