Theory CH

section‹Forcing extension satisfying the Continuum Hypothesis›

theory CH
  imports
    Kappa_Closed_Notions
    Cohen_Posets_Relative
begin

context M_ctm2_AC
begin

declare Fn_rel_closed[simp del, rule del, simplified setclass_iff, simp, intro]
declare Fnle_rel_closed[simp del, rule del, simplified setclass_iff, simp, intro]

abbreviation
  Coll :: "i" where
  "Coll  Fn⇗M⇖(ℵ⇘1⇙⇗M, ℵ⇘1⇙⇗M, ω →⇗M2)"

abbreviation
  Colleq :: "i" where
  "Colleq  Fnle⇗M⇖(ℵ⇘1⇙⇗M, ℵ⇘1⇙⇗M, ω →⇗M2)"

lemma Coll_in_M[intro,simp]: "Coll  M" by simp

lemma Colleq_refl : "refl(Coll,Colleq)"
  unfolding Fnle_rel_def Fnlerel_def refl_def
  using RrelI by simp

subsection‹Collapse forcing is sufficiently closed›

― ‹Kunen IV.7.14, only for term‹ℵ1››
lemma succ_omega_closed_Coll: "succ(ω)-closed⇗M⇖(Coll,Colleq)"
proof -
  ― ‹Case for finite sequences›
  have "nω  f  n <→⇗M(Coll,converse(Colleq)).
          qM. q  Coll  (αM. α  n  q, f ` α  Colleq)" for n
  proof (induct rule:nat_induct)
    case 0
    then
    show ?case
      using zero_lt_Aleph_rel1 zero_in_Fn_rel
      by (auto simp del:setclass_iff) (rule bexI[OF _ zero_in_M], auto)
  next
    case (succ x)
    then
    have "fsucc(x) <→⇗M(Coll,converse(Colleq)). α  succ(x). f`x, f ` α  Colleq"
    proof(intro ballI)
      fix f α
      assume "fsucc(x) <→⇗M(Coll,converse(Colleq))" "αsucc(x)"
      moreover from xω this
      have "fsucc(x) < (Coll,converse(Colleq))"
        using mono_seqspace_rel_char nat_into_M
        by simp
      moreover from calculation succ
      consider "αx" | "α=x"
        by auto
      then
      show "f`x, f ` α  Colleq"
      proof(cases)
        case 1
        then
        have "α, x  Memrel(succ(x))" "xsucc(x)" "αsucc(x)"
          by auto
        with fsucc(x) < (Coll,converse(Colleq))
        show ?thesis
          using mono_mapD(2)[OF _ αsucc(x) _ α, x  Memrel(succ(x))]
          unfolding mono_seqspace_def
          by auto
      next
        case 2
        with fsucc(x) < (Coll,converse(Colleq))
        show ?thesis
          using Colleq_refl mono_seqspace_is_fun[THEN apply_type]
          unfolding refl_def
          by simp
      qed
    qed
    moreover
    note xω
    moreover from this
    have "f`x  Coll" if "f: succ(x) <→⇗M(Coll,converse(Colleq))" for f
      using that mono_seqspace_rel_char[simplified, of "succ(x)" Coll "converse(Colleq)"]
        nat_into_M[simplified] mono_seqspace_is_fun[of "converse(Colleq)"]
      by (intro apply_type[of _ "succ(x)"]) (auto simp del:setclass_iff)
    ultimately
    show ?case
      using transM[of _ Coll]
      by (auto dest:transM simp del:setclass_iff, rule_tac x="f`x" in bexI)
        (auto simp del:setclass_iff, simp)
  qed
  moreover
    ― ‹Interesting case: Countably infinite sequences.›
  have "fM. f  ω <→⇗M(Coll,converse(Colleq)) 
                  (qM. q  Coll  (αM. α  ω  q, f ` α  Colleq))"
  proof(intro ballI impI)
    fix f
    let ?rnf="f``ω"
    assume "fM" "f  ω <→⇗M(Coll,converse(Colleq))"
    moreover from this
    have "fω < (Coll,converse(Colleq))" "fω  Coll"
      using mono_seqspace_rel_char mono_mapD(2) nat_in_M
      by auto
    moreover from this
    have "countable⇗M⇖(f`x)" if "xω" for x
      using that Fn_rel_is_function countable_iff_lesspoll_rel_Aleph_rel_one
      by auto
    moreover from calculation
    have "?rnf  M" "fω×Coll"
      using nat_in_M image_closed Pi_iff
      by simp_all
    moreover from calculation
    have 1:"d?rnf. d  h  d  g" if "h  ?rnf" "g  ?rnf" for h g
    proof -
      from calculation
      have "?rnf={f`x . xω}"
        using  image_function[of f ω] Pi_iff domain_of_fun
        by auto
      from ?rnf=_ that
      obtain m n where eq:"h=f`m" "g=f`n" "nω" "mω"
        by auto
      then
      have "mnω" "mmn" "nmn"
        using Un_upper1_le Un_upper2_le nat_into_Ord by simp_all
      with calculation eq ?rnf=_
      have "f`(mn)?rnf" "f`(mn)  h" "f`(mn)  g"
        using Fnle_relD mono_map_lt_le_is_mono converse_refl[OF Colleq_refl]
        by auto
      then
      show ?thesis
        by auto
    qed
    moreover from calculation
    have "?rnf  (ℵ⇘1⇙⇗M⇖ ⇀⇗##M(nat →⇗M2))"
      using subset_trans[OF image_subset[OF f_,of ω] Fn_rel_subset_PFun_rel]
      by simp
    moreover
    have " ?rnf  (ℵ⇘1⇙⇗M⇖ ⇀⇗##M(nat →⇗M2))"
      using pfun_Un_filter_closed'[OF ?rnf_ 1]  ?rnfM
      by simp
    moreover from calculation
    have "?rnf ≺⇗M⇖ ℵ⇘1⇙⇗M⇖"
      using countable_fun_imp_countable_image[of f]
        mem_function_space_rel_abs[simplified,OF nat_in_M Coll_in_M fM]
        countableI[OF lepoll_rel_refl]
        countable_iff_lesspoll_rel_Aleph_rel_one[of "?rnf"]
      by auto
    moreover from calculation
    have "?rnfColl"
      unfolding Fn_rel_def
      by simp
    moreover from calculation
    have "?rnf  f ` α " if "αω" for α
      using that image_function[OF fun_is_function] domain_of_fun
      by auto
    ultimately
    show "qM. q  Coll  (αM. α  ω  q, f ` α  Colleq)"
      using Fn_rel_is_function Fnle_relI
      by auto
  qed
  ultimately
  show ?thesis
    unfolding kappa_closed_rel_def by (auto elim!:leE dest:ltD)
qed

end ― ‹localeM_ctm2_AC

locale collapse_CH = G_generic3_AC_CH "Fn⇗M⇖(ℵ⇘1⇙⇗##M, ℵ⇘1⇙⇗M, ω →⇗M2)" "Fnle⇗M⇖(ℵ⇘1⇙⇗##M, ℵ⇘1⇙⇗M, ω →⇗M2)" 0

sublocale collapse_CH  forcing_notion "Coll" "Colleq" 0
  using zero_lt_Aleph_rel1 by unfold_locales

context collapse_CH
begin

notation Leq (infixl "" 50)
notation Incompatible (infixl "" 50)

abbreviation
  f_G :: "i" (fG) where
  "fG  G"

lemma f_G_in_MG[simp]:
  shows "fG  M[G]"
  using G_in_MG by simp

abbreviation
  dom_dense :: "ii" where
  "dom_dense(x)  { pColl . x  domain(p) }"

lemma dom_dense_closed[intro,simp]: "xM  dom_dense(x)  M"
  using separation_in_domain[of x]
  by simp

lemma domain_f_G: assumes "x  ℵ⇘1⇙⇗M⇖"
  shows "x  domain(fG)"
proof -
  have "(λnω. 0)  ω →⇗M2"
    using function_space_rel_nonempty[of 0 2 ω]
    by auto
  with assms
  have "dense(dom_dense(x))" "xM"
    using dense_dom_dense InfCard_rel_Aleph_rel[of 1] transitivity[OF _
       Aleph_rel_closed[of 1,THEN setclass_iff[THEN iffD1]]]
    unfolding dense_def
     by auto
  with assms
  obtain p where "pdom_dense(x)" "pG"
    using M_generic_denseD[of "dom_dense(x)"]
    by auto
  then
  show "x  domain(fG)" by blast
qed

lemma Un_filter_is_function:
  assumes "filter(G)"
  shows "function(G)"
proof -
  have "Coll  ℵ⇘1⇙⇗M⇖ ⇀⇗##M(ω →⇗M2)"
    using Fn_rel_subset_PFun_rel
    by simp
  moreover
  have " d  Coll. d  f  d  g" if "fG" "gG" for f g
    using filter_imp_compat[OF assms fG gG] filterD[OF assms]
    unfolding compat_def compat_in_def
    by auto
  ultimately
  have "d  ℵ⇘1⇙⇗M⇖ ⇀⇗##M(ω →⇗M2). d  f  d  g" if "fG" "gG" for f g
    using rex_mono[of Coll] that by simp
  moreover
  have "GColl"
    using assms
    unfolding filter_def
    by simp
  moreover from this
  have "G  ℵ⇘1⇙⇗M⇖ ⇀⇗##M(ω →⇗M2)"
    using assms unfolding Fn_rel_def
    by auto
  ultimately
  show ?thesis
    using pfun_Un_filter_closed[of G]
    by simp
qed

lemma f_G_funtype:
  shows "fG : ℵ⇘1⇙⇗M ω →⇗M[G]2"
proof -
  have "x  B  B  G  x  ℵ⇘1⇙⇗M× (ω →⇗M[G]2)" for B x
  proof -
    assume "xB" "BG"
    moreover from this
    have "x  M[G]"
      by (auto dest!: ext.transM simp add:G_in_MG)
    moreover from calculation
    have "x  ℵ⇘1⇙⇗M× (ω  2)"
      using Fn_rel_subset_Pow[of "ℵ⇘1⇙⇗M⇖" "ℵ⇘1⇙⇗M⇖" "ω →⇗M2",
          OF _ _ function_space_rel_closed] function_space_rel_char
      by (auto dest!: M_genericD)
    moreover from this
    obtain z w where "x=z,w" "zℵ⇘1⇙⇗M⇖" "w:ω  2" by auto
    moreover from calculation
    have "w  M[G]" by (auto dest:ext.transM)
    ultimately
    show ?thesis using ext.function_space_rel_char by auto
  qed
  moreover
  have "function(fG)"
    using Un_filter_is_function generic
    by fast
  ultimately
  show ?thesis
    using generic domain_f_G Pi_iff by auto
qed

abbreviation
  surj_dense :: "ii" where
  "surj_dense(x)  { pColl . x  range(p) }"

lemma surj_dense_closed[intro,simp]:
  "x  ω →⇗M2  surj_dense(x)  M"
  using separation_in_range transM[of x] by simp

lemma reals_sub_image_f_G:
  assumes "x  ω →⇗M2"
  shows "αℵ⇘1⇙⇗M. fG ` α = x"
proof -
  from assms
  have "dense(surj_dense(x))"
    using dense_surj_dense lepoll_rel_refl InfCard_rel_Aleph_rel
    unfolding dense_def
    by auto
  with x  ω →⇗M2
  obtain p where "psurj_dense(x)" "pG"
    using M_generic_denseD[of "surj_dense(x)"]
    by blast
  then
  show ?thesis
    using succ_omega_closed_Coll f_G_funtype function_apply_equality[of _ x f_G]
      succ_omega_closed_imp_no_new_reals[symmetric]
    by (auto, rule_tac bexI) (auto simp:Pi_def)
qed

lemma f_G_surj_Aleph_rel1_reals: "fG  surj⇗M[G]⇖(ℵ⇘1⇙⇗M, ω →⇗M[G]2)"
  using Aleph_rel_sub_closed
proof (intro ext.mem_surj_abs[THEN iffD2],simp_all)
  show "fG  surj(ℵ⇘1⇙⇗M, ω →⇗M[G]2)"
    using f_G_funtype G_in_MG ext.nat_into_M f_G_in_MG
      reals_sub_image_f_G succ_omega_closed_Coll
      succ_omega_closed_imp_no_new_reals
    unfolding surj_def
    by auto
qed

lemma continuum_rel_le_Aleph1_extension:
  includes G_generic1_lemmas
  shows "2⇗↑ℵ⇘0⇙⇗M[G],M[G] ℵ⇘1⇙⇗M[G]⇖"
proof -
  have "ℵ⇘1⇙⇗M M[G]" "Ord(ℵ⇘1⇙⇗M)"
    using Card_rel_is_Ord by auto
  moreover from this
  have "ω →⇗M[G]2 ≲⇗M[G]⇖ ℵ⇘1⇙⇗M⇖"
    using ext.surj_rel_implies_inj_rel[OF f_G_surj_Aleph_rel1_reals]
      f_G_in_MG unfolding lepoll_rel_def by auto
  with Ord(ℵ⇘1⇙⇗M)
  have "|ω →⇗M[G]2|⇗M[G] |ℵ⇘1⇙⇗M⇖|⇗M[G]⇖"
    using M_subset_MG[OF one_in_G] Aleph_rel_closed[of 1]
    by (rule_tac ext.lepoll_rel_imp_cardinal_rel_le) simp_all
  ultimately
  have "2⇗↑ℵ⇘0⇙⇗M[G],M[G] |ℵ⇘1⇙⇗M[G]⇖|⇗M[G]⇖"
    using ext.lepoll_rel_imp_cardinal_rel_le[of "ℵ⇘1⇙⇗M⇖" "ω →⇗M[G]2"]
      ext.Aleph_rel_zero succ_omega_closed_Coll
      succ_omega_closed_imp_Aleph_1_preserved
    unfolding cexp_rel_def by simp
  then
  show "2⇗↑ℵ⇘0⇙⇗M[G],M[G] ℵ⇘1⇙⇗M[G]⇖" by simp
qed

theorem CH: "ℵ⇘1⇙⇗M[G]= 2⇗↑ℵ⇘0⇙⇗M[G],M[G]⇖"
  using continuum_rel_le_Aleph1_extension ext.Aleph_rel_succ[of 0]
    ext.Aleph_rel_zero ext.csucc_rel_le[of "2⇗↑ℵ⇘0⇙⇗M[G],M[G]⇖" ω]
    ext.Card_rel_cexp_rel ext.cantor_cexp_rel[of ω] ext.Card_rel_nat
    le_anti_sym
  by auto

end ― ‹localecollapse_CH

subsection‹Models of fragments of $\ZFC + \CH$›

theorem ctm_of_CH:
  assumes
    "M  ω" "Transset(M)"
    "M  ZC  {⋅Replacement(p)⋅ . p  overhead_CH}"
    "Φ  formula" "M  { ⋅Replacement(ground_repl_fm(φ))⋅ . φ  Φ}"
  shows
    "N.
      M  N  N  ω  Transset(N)  N  ZC  {⋅CH⋅}  { ⋅Replacement(φ)⋅ . φ  Φ} 
      (α. Ord(α)  (α  M  α  N))"
proof -
  from M  ZC  {⋅Replacement(p)⋅ . p  overhead_CH}
  interpret M_ZFC3 M
    using M_satT_overhead_imp_M_ZF3 unfolding overhead_CH_def overhead_notCH_def by auto
  from M  ZC  {⋅Replacement(p)⋅ . p  overhead_CH} Transset(M)
  interpret M_ZF_ground_CH_trans M
    using M_satT_imp_M_ZF_ground_CH_trans
    unfolding ZC_def by auto
  from M  ω
  obtain enum where "enum  bij(ω,M)"
    using eqpoll_sym unfolding eqpoll_def by blast
  then
  interpret M_ctm2_AC_CH M enum by unfold_locales
  interpret forcing_data1 "Coll" "Colleq" 0 M enum
    using zero_in_Fn_rel[of "ℵ⇘1⇙⇗M⇖" "ℵ⇘1⇙⇗M⇖" "ω →⇗M2"]
      zero_top_Fn_rel[of _ "ℵ⇘1⇙⇗M⇖" "ℵ⇘1⇙⇗M⇖" "ω →⇗M2"]
      preorder_on_Fnle_rel[of "ℵ⇘1⇙⇗M⇖" "ℵ⇘1⇙⇗M⇖" "ω →⇗M2"]
      zero_lt_Aleph_rel1
    by unfold_locales simp_all
  obtain G where "M_generic(G)"
    using generic_filter_existence[OF one_in_P]
    by auto
  moreover from this
  interpret collapse_CH M enum G by unfold_locales
  have "ℵ⇘1⇙⇗M[G]= 2⇗↑ℵ⇘0⇙⇗M[G],M[G]⇖"
    using CH .
  then
  have "M[G], []  ⋅CH⋅"
    using ext.is_ContHyp_iff
    by (simp add:ContHyp_rel_def)
  then
  have "M[G]  ZC  {⋅CH⋅}"
    using ext.M_satT_ZC by auto
  moreover
  have "Transset(M[G])" using Transset_MG .
  moreover
  have "M  M[G]" using M_subset_MG[OF one_in_G] generic by simp
  moreover
  note M  { ⋅Replacement(ground_repl_fm(φ))⋅ . φ  Φ} Φ  formula
  ultimately
  show ?thesis
    using Ord_MG_iff MG_eqpoll_nat satT_ground_repl_fm_imp_satT_ZF_replacement_fm[of Φ]
    by (rule_tac x="M[G]" in exI,blast)
qed

corollary ctm_ZFC_imp_ctm_CH:
  assumes
    "M  ω" "Transset(M)" "M  ZFC"
  shows
    "N.
      M  N  N  ω  Transset(N)  N  ZFC  {⋅CH⋅} 
      (α. Ord(α)  (α  M  α  N))"
proof -
  from assms
  have "N.
      M  N 
        N  ω 
        Transset(N) 
        N  ZC  N  {⋅CH⋅}  N  {⋅Replacement(x)⋅ . x  formula}  (α. Ord(α)  α  M  α  N)"
    using ctm_of_CH[of M formula] satT_ZFC_imp_satT_ZC[of M]
      satT_mono[OF _ ground_repl_fm_sub_ZFC, of M]
      satT_mono[OF _ ZF_replacement_overhead_CH_sub_ZFC, of M]
      satT_mono[OF _ ZF_replacement_fms_sub_ZFC, of M]
    by (simp add: satT_Un_iff)
  then
  obtain N where "N  ZC" "N  {⋅CH⋅}" "N  {⋅Replacement(x)⋅ . x  formula}"
    "M  N" "N  ω" "Transset(N)" "(α. Ord(α)  α  M  α  N)"
    by auto
  moreover from this
  have "N  ZFC"
    using satT_ZC_ZF_replacement_imp_satT_ZFC
    by auto
  moreover from this and N  {⋅CH⋅}
  have "N  ZFC  {⋅CH⋅}"
    using satT_ZC_ZF_replacement_imp_satT_ZFC
    by auto
  ultimately
  show ?thesis
    by auto
qed

end