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 "xM[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 ― ‹localeG_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)  MN
(α. 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 termM[G] denotes the generic extension
of termM using the poset of sequences term2⇗<ω⇖›.›
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  MN
(α. Ord(α)  (α  M  α  N))
((M, [] ⋅AC⋅)  N  ZFC)"
proof -
from assms
have "N.
M  N  N  ω  Transset(N)  MN
(α. 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