ZFC in M[G]

Im folgenden sei stets M ein Grundmodell, P ∈ M eine Forcing- Halbordnung und G ein P -generischer Filter über M.

(Null) gilt, da ∅ ∈ M ⊆ M[G]

(Ext) gilt, da M[G] transitiv

(Fund) gilt, da M[G] transitiv

(Inf) gilt, da ω ∈ M ⊆ M[G]

(Paar) ∀x, y ∈ M[G] : {x, y} ∈ M[G]

Bew.: Sei x = ẋ^{G}, y = ẏ^{G} ∈ M[G] Dann ist {(ẋ, 1), (ẏ, 1)} ∈ M^{P} und {(ẋ, 1), (ẏ, 1)}^{G} = {ẋ^{G}, ẏ^{G}} = {x, y}.

(Aus) ∀x ∈ M[G] : {a ∈ x|φ^{M[G]}} ∈ M[G]

Bew.: Sei φ(v, y⃗) eine ∈ -Formel, x = ẋ^{G}, y⃗ = \overrightarrow{ẏ^{G}} ∈ M[G]. Betrachte ṡ = {(ṫ, p) ∈ dom(ẋ) × P | p ⊩ ṫ ∈ ẋ ∧ φ(ṫ, ẏ)} Nach Forcingtheorem (und unter Verwendung von (Aus)^{M}) ist dann ṡ = {(ṫ, p) ∈ dom(ẋ) × P | (p ⊩^{∗} ṫ ∈ ẋ ∧ φ(ṫ, ẏ))^{M}} ∈ M^{P}. Beh.:Es gilt ṡ^{G} = \{a ∈ x | φ^{M[G]}(a, \overrightarrow{ẏ^{G}})\}. Bew.:Sei ṫ^{G} ∈ ṡ^{G}, d.h. (ṫ, p) ∈ dom(ẋ) × P, p ∈ G und p ⊩ ṫ ∈ ẋ ∧ φ. Nach Forcingtheorem gilt dann ṫ^{G} ∈ ẋ^{G} ∧ φ^{M[G]}. Sei umgekehrt ṫ^{G} ∈ ẋ^{G} ∧ φ^{M[G)}(ṫ^{G}, \overrightarrow{ẏ^{G}}), also (ṫ^{G} ∈ ẋ^{G} ∧ φ^{M[G]}(ṫ^{G}, \overrightarrow{ẏ^{G}}))^{M[G]}. Nach Forcingtheorem existiert dann p′ ∈ G : p′ ⊩ (ṫ ∈ ẋ ∧ φ). Damit ist (ṫ, p′) ∈ ṡ und ṫ^{G} ∈ ṡ^{G}.

(Ver) ∀x ∈ M[G] : ⋃ x ∈ M[G]

Bew.: Sei x = ẋ^{G} ∈ M[G]. Sei ṫ = ⋃ dom(ẋ) ∈ M^{P}.

Dann ist ⋃ x ⊆ ṫ^{G}. Behauptung folgt mit Aussonderung.

(Pot) ∀x ∈ M[G] : (P(x) ∩ M[G]) ∈ M[G]

Bew.: Sei x = ẋ^{G} ∈ M[G].

Sei ṫ = S × {1} Name in M mit S = {ṡ ∈ M^{P} | dom(ṡ) ⊆ dom(ẋ)} ∈ M. Sei y = ẏ^{G} ∈ M[G] mit y ⊆ x. Es genügt zu zeigen, y ∈ ṫ^{G}. Sei dazu ṡ = {(ṙ, p) | r ∈ dom(ẋ) ∧ p ⊩ ṙ ∈ ẏ} ∈ S; damit ṡ^{G} ∈ ṫ^{G} Beh.:Es gilt y = ṡ^{G}.

Bew.:Sei ż^{G} ∈ ẏ^{G} ⊆ ẋ^{G}, dann gilt ż ∈ dom(ẋ) ∧ (ż^{G} ∈ ẏ^{G})^{M[G]}. Nach Forcingtheorem existiert q ∈ G q ⊩ ż ∈ ẏ, damit ist (ż, q) ∈ ṡ und somit ż^{G} ∈ ṡ^{G}. Sei nun ż^{G} ∈ ṡ^{G} , d.h. ∃p ∈ G (ż, p) ∈ ṡ mit ż ∈ dom(ẋ) und p ⊩ ż ∈ ẏ. Nach Forcingtheorem gilt damit aber (ż^{G} ∈ ẏ^{G})^{M[G]} ↔ ż^{G} ∈ ẏ^{G}. Behauptung folgt nun mit Aussonderung.

(Ers) ∀x, y, y′ ∈ M[G] : ((φ^{M[G]}(x, y) ∧ φ^{M[G]}(x, y′) ⟶ y = y′) ⟶ ∀a ∈ M[G] {y ∈ M[G] | ∃x ∈ a φ^{M[G]}(x, y)} ∈ M[G])

Bew.: Sei φ Formel mit obiger Eigenschaft. Sei a = ȧ^{G}, z⃗ = \overrightarrow{ż^{G}} ∈ M[G] und R = {y ∈ M[G] | ∃x ∈ a φ^{M[G]}(x, y, z⃗)}. Nach dem Reflexionssatz existiert ein S ∈ M, S ⊆ M^{P}, so dass ∀ẋ ∈ dom(ȧ) gilt ∀p ∈ P ((∃ẏ ∈ M^{P} p ⊩ φ(ẋ, ẏ, ż)) ⟶ ∃ẏ ∈ S p ⊩ φ(ẋ, ẏ, ż)). Sei ṫ = S × {1} ∈ M^{P}. Beh.: R ⊆ ṫ^{G}. Bew.:Sei y = ẏ^{G} ∈ R, d.h. es ex (ẋ, q) ∈ ȧ, q ∈ G, x = ẋ^{G}. Also gilt φ^{M[G]}(ẋ^{G}, ẏ^{G}, \overrightarrow{ż^{G}}). Nach Forcingtheorem ∃p ∈ G mit p ⊩ φ(ẋ, ẏ, ż). Nach Wahl von S existiert nun ein ẏ′ ∈ S mit p ⊩ φ(ẋ, ẏ′, ż). Erneute Anwendung des Forcingtheorems liefert φ^{M[G]}(ẋ^{G}, ẏ′^{G}, \overrightarrow{ż^{G}}). Wegen der Funktionalität von φ ist nun ẏ^{G} = ẏ′^{G}. Also haben wir (ẏ′, 1) ∈ ṫ und damit y = ẏ^{G} = ẏ′^{G} ∈ ṫ^{G}. Die Behauptung folgt nun wiederum aus (Aus)^{M[G]}.

(AC) Wir zeigen eine unter ZF zu (AC) äquivalente Fassung:

∀x∃α ∈ On∃f(f ist Funktion ∧dom(f) = α ∧ x ⊆ ran(f))

Bew.: Beachte zuerst, dass für x = ẋ^{G}, y = ẏ^{G} ∈ M[G] op(ẋ, ẏ) = {({(ẋ, 1), (ẋ, 1)}, ({(ẋ, 1), (ẏ, 1)}, 1)} ein Name für das geordnete Paar (x, y) ist, d.h. op(ẋ, ẏ)^{G} = (x, y). Sei nun x = ẋ^{G} ∈ M[G]. Dann ist dom(ẋ) ∈ M und nach (AC)^{M} gibt es eine Ordinalzahl α ∈ On ∩ M und eine Bijektion f ∈ M f : α ⟶ dom(ẋ) ; γ ⟼ ẏ_{γ} Setze ż = {op(γ̌, ẏ_{γ}) | γ < α} × {1} ∈ M^{P}. ż^{G} = {(γ, ẏ_{γ}^{G}) | γ < α} ist dann eine Funktion mit dom(ż^{G}) = α und ẋ^{G} ⊆ ran(ż^{G}).