# Theory Forcing_Main

```section‹The existence of generic extensions›

theory Forcing_Main
imports
Ordinals_In_MG
Choice_Axiom
Succession_Poset

begin

subsection‹The generic extension is countable›

lemma (in forcing_data1) surj_nat_MG : "∃f. f ∈ surj(ω,M[G])"
proof -
let ?f="λn∈ω. val(G,enum`n)"
have "x ∈ ω ⟹ val(G, enum ` x)∈ M[G]" for x
using GenExtI bij_is_fun[OF M_countable]
by simp
then
have "?f: ω → M[G]"
using lam_type[of ω "λn. val(G,enum`n)" "λ_.M[G]"] by simp
moreover
have "∃n∈ω. ?f`n = x" if "x∈M[G]" for x
using that GenExt_iff[of _ G] bij_is_surj[OF M_countable]
unfolding surj_def by auto
ultimately
show ?thesis
unfolding surj_def by blast
qed

lemma (in G_generic1) MG_eqpoll_nat: "M[G] ≈ ω"
proof -
obtain f where "f ∈ surj(ω,M[G])"
using surj_nat_MG by blast
then
have "M[G] ≲ ω"
using well_ord_surj_imp_lepoll well_ord_Memrel[of ω] by simp
moreover
have "ω ≲ M[G]"
using ext.nat_into_M subset_imp_lepoll by (auto del:lepollI)
ultimately
show ?thesis
using eqpollI by simp
qed

subsection‹Extensions of ctms of fragments of \$\ZFC\$›

context G_generic1
begin

lemma sats_ground_repl_fm_imp_sats_ZF_replacement_fm:
assumes
"φ∈formula" "M, [] ⊨ ⋅Replacement(ground_repl_fm(φ))⋅"
shows
"M[G], [] ⊨ ⋅Replacement(φ)⋅"
using assms sats_ZF_replacement_fm_iff
by (auto simp:replacement_assm_def ground_replacement_assm_def
intro:strong_replacement_in_MG[simplified])

lemma satT_ground_repl_fm_imp_satT_ZF_replacement_fm:
assumes
"Φ ⊆ formula" "M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}"
shows
"M[G] ⊨ { ⋅Replacement(φ)⋅ . φ ∈ Φ}"
using assms sats_ground_repl_fm_imp_sats_ZF_replacement_fm
by auto

end ― ‹\<^locale>‹G_generic1››

theorem extensions_of_ctms:
assumes
"M ≈ ω" "Transset(M)"
"M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ overhead}"
"Φ ⊆ formula" "M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}"
shows
"∃N.
M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ M≠N ∧
(∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N)) ∧
((M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅) ∧ N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ Φ}"
proof -
from ‹M ⊨ ⋅Z⋅ ∪ _› ‹Transset(M)›
interpret M_ZF_ground_trans M
using M_satT_imp_M_ZF_ground_trans
by simp
from ‹M ≈ ω›
obtain enum where "enum ∈ bij(ω,M)"
using eqpoll_sym unfolding eqpoll_def by blast
then
interpret M_ctm1 M enum by unfold_locales
interpret forcing_data1 "2⇗<ω⇖" seqle 0 M enum
using nat_into_M seqspace_closed seqle_in_M
by unfold_locales simp
obtain G where "M_generic(G)" "M ≠ M[G]"
using cohen_extension_is_proper
by blast
text‹Recall that \<^term>‹M[G]› denotes the generic extension
of \<^term>‹M› using the poset of sequences \<^term>‹2⇗<ω⇖›.›
then
interpret G_generic1 "2⇗<ω⇖" seqle 0 _ enum G by unfold_locales
interpret MG: M_Z_basic "M[G]"
using generic pairing_in_MG
Union_MG  extensionality_in_MG power_in_MG
foundation_in_MG replacement_assm_MG
separation_in_MG infinity_in_MG replacement_ax1
by unfold_locales simp
have "M, []⊨ ⋅AC⋅ ⟹ M[G], [] ⊨ ⋅AC⋅"
proof -
assume "M, [] ⊨ ⋅AC⋅"
then
have "choice_ax(##M)"
unfolding ZF_choice_fm_def using ZF_choice_auto by simp
then
have "choice_ax(##M[G])" using choice_in_MG by simp
then
show "M[G], [] ⊨ ⋅AC⋅"
using ZF_choice_auto sats_ZFC_iff_sats_ZF_AC
unfolding ZF_choice_fm_def by simp
qed
moreover
note ‹M ≠ M[G]› ‹M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}› ‹Φ ⊆ formula›
moreover
have "Transset(M[G])" using Transset_MG .
moreover
have "M ⊆ M[G]" using M_subset_MG[OF one_in_G] generic by simp
ultimately
show ?thesis
using Ord_MG_iff MG_eqpoll_nat ext.M_satT_Zermelo_fms
satT_ground_repl_fm_imp_satT_ZF_replacement_fm[of Φ]
by (rule_tac x="M[G]" in exI, auto)
qed

using instances1_fms_type instances_ground_fms_type
unfolding overhead_def ZF_def ZF_schemes_def by auto

theorem extensions_of_ctms_ZF:
assumes
"M ≈ ω" "Transset(M)" "M ⊨ ZF"
shows
"∃N.
M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZF ∧ M≠N ∧
(∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N)) ∧
((M, []⊨ ⋅AC⋅) ⟶ N ⊨ ZFC)"
proof -
from assms
have "∃N.
M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ M≠N ∧
(∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N)) ∧
((M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅) ∧ N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ formula}"
using extensions_of_ctms[of M formula] satT_ZF_imp_satT_Z[of M]
satT_mono[OF _ ground_repl_fm_sub_ZF, of M]
by (auto simp: satT_Un_iff)
then
obtain N where "N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ formula}" "M ⊆ N" "N ≈ ω" "Transset(N)"
"M ≠ N" "(∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)"
"(M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅"
by blast
moreover from ‹N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ formula}›
have "N ⊨ ZF"
using satT_Z_ZF_replacement_imp_satT_ZF by auto
moreover from this and ‹(M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅›
have "(M, []⊨ ⋅AC⋅) ⟶ N ⊨ ZFC"
using sats_ZFC_iff_sats_ZF_AC by simp
ultimately
show ?thesis
by auto
qed

end```