Theory Forcing_Main

sectionThe existence of generic extensions

theory Forcing_Main
  imports
    Ordinals_In_MG
    Choice_Axiom
    Succession_Poset

begin

subsectionThe 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

subsectionExtensions 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
  textRecall 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

lemma ZF_replacement_overhead_sub_ZF: "{⋅Replacement(p)⋅ . p  overhead}  ZF"
  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]
      satT_mono[OF _ ZF_replacement_overhead_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