Axiomatic Set Theory — Forcing

graph TD ZFC["ZFC\n(Charts 1–3)"] DefPoset["Def: Forcing poset\n(P,≤,1) preorder, splitting"] DefGeneric["Def: Generic filter\nG ⊆ P, dense meet"] DefNames["Def: P-names\nV^P = ⋃ Name(α)"] DefVal["Def: Interpretation\nval(u,G)"] DefCheck["Def: Check names\nx̌"] DefForce["Def: Forcing relation\np ⊩ φ"] T1["Thm: M[G] ⊨ ZFC\nM[G] is model"] T2["Thm: Coherence\nq≤p, p⊩φ ⇒ q⊩φ"] T3["Thm: Definability\n⊩ definable in M"] T4["Thm: Truth\nM[G]⊨φ iff ∃p∈G p⊩φ"] T5["Thm: Rasiowa-Sikorski\nG exists for countable M"] ExCohen["Ex: Cohen forcing\nFin(S,2)"] ZFC --> DefPoset DefPoset --> DefGeneric DefPoset --> DefNames DefNames --> DefVal DefVal --> DefCheck DefGeneric --> DefVal DefVal --> DefForce DefForce --> T1 DefForce --> T2 DefForce --> T3 DefForce --> T4 DefGeneric --> T5 DefPoset --> ExCohen classDef axiom fill:#ff6b6b,color:#fff,stroke:#c0392b classDef definition fill:#b197fc,color:#fff,stroke:#9775fa classDef theorem fill:#51cf66,color:#fff,stroke:#40c057 class ZFC axiom class DefPoset,DefGeneric,DefNames,DefVal,DefCheck,DefForce,ExCohen definition class T1,T2,T3,T4,T5 theorem