Quelle  CH.thy

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(ℵ, ℵ, ψ → 2)"

abbreviation
  Colleq :: "i" where
  "Colleq ≡ Fnle(ℵ, ℵ, ψ → 2)"

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‹ℵ››
lemma succ_omega_closed_Coll: "succ(ψ)-closed(Coll,Colleq)"
proof -
  ― ‹Case for finite sequences›
  have "n∈ψ ==> ∀f ∈ n _<→ (Coll,converse(Colleq)).
          ∃q∈M. 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 "∀f∈succ(x) <sub><</sub>→ (Coll,converse(Colleq)). ∀α ∈ succ(x). ⟨f`x, f ` α⟩ ∈ Colleq"
    proof(intro ballI)
      fix f α
      assume "f∈succ(x) <sub><</sub>→ (Coll,converse(Colleq))" "α∈succ(x)"
      moreover from ‹x∈ψ› this
      have "f∈succ(x) <sub><</sub>→ (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))" "x∈succ(x)" "α∈succ(x)"
          by auto
        with ‹f∈succ(x) <sub><</sub>→ (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 ‹f∈succ(x) <sub><</sub>→ (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) _<→ (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 "∀f∈M. f ∈ ψ <sub><</sub>→ (Coll,converse(Colleq)) ⟶
                  (∃q∈M. q ∈ Coll ∧ (∀α∈M. α ∈ ψ ⟶ ⟨q, f ` α⟩ ∈ Colleq))"
  proof(intro ballI impI)
    fix f
    let ?rnf="f``ψ"
    assume "f∈M" "f ∈ ψ _<→ (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(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 "m∪n∈ψ" "m≤m∪n" "n≤m∪n"
        using Un_upper1_le Un_upper2_le nat_into_Ord by simp_all
      with calculation eq ‹?rnf=_›
      have "f`(m∪n)∈?rnf" "f`(m∪n) 🪙 h" "f`(m∪n) 🪙 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 ⊆ (ℵ ⇀<sup>#M</sup> (nat → 2))"
      using subset_trans[OF image_subset[OF ‹f⊆_›,of ψ] Fn_rel_subset_PFun_rel]
      by simp
    moreover
    have "∪ ?rnf ∈ (ℵ ⇀<sup>#M</sup> (nat → 2))"
      using pfun_Un_filter_closed'[OF ‹?rnf⊆_› 1]  ‹?rnf∈M›
      by simp
    moreover from calculation
    have "∪?rnf ≺ ℵ"
      using countable_fun_imp_countable_image[of f]
        mem_function_space_rel_abs[simplified,OF nat_in_M Coll_in_M ‹f∈M›]
        countableI[OF lepoll_rel_refl]
        countable_iff_lesspoll_rel_Aleph_rel_one[of "∪?rnf"]
      by auto
    moreover from calculation
    have "∪?rnf∈Coll"
      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 "∃q∈M. 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 ― ‹🍋‹M_ctm2_AC››

locale collapse_CH = G_generic3_AC_CH "Fn(ℵ^#M, ℵ, ψ → 2)" "Fnle(ℵ^#M, ℵ, ψ → 2)" 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" (‹f›) where
  "f ≡ ∪G"

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

abbreviation
  dom_dense :: "i==>i" where
  "dom_dense(x) ≡ { p∈Coll . x ∈ domain(p) }"

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

lemma domain_f_G: assumes "x ∈ ℵ"
  shows "x ∈ domain(f)"
proof -
  have "(λn∈ψ. 0) ∈ ψ → 2"
    using function_space_rel_nonempty[of 0 2 ψ]
    by auto
  with assms
  have "dense(dom_dense(x))" "x∈M"
    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 "p∈dom_dense(x)" "p∈G"
    using M_generic_denseD[of "dom_dense(x)"]
    by auto
  then
  show "x ∈ domain(f)" by blast
qed

lemma Un_filter_is_function:
  assumes "filter(G)"
  shows "function(∪G)"
proof -
  have "Coll ⊆ ℵ ⇀^#M (ψ → 2)"
    using Fn_rel_subset_PFun_rel
    by simp
  moreover
  have "∃ d ∈ Coll. d 🪙 f ∧ d 🪙 g" if "f∈G" "g∈G" for f g
    using filter_imp_compat[OF assms ‹f∈G› ‹g∈G›] filterD[OF assms]
    unfolding compat_def compat_in_def
    by auto
  ultimately
  have "∃d ∈ ℵ ⇀^#M (ψ → 2). d 🪙 f ∧ d 🪙 g" if "f∈G" "g∈G" for f g
    using rex_mono[of Coll] that by simp
  moreover
  have "G⊆Coll"
    using assms
    unfolding filter_def
    by simp
  moreover from this
  have "G ⊆ ℵ ⇀^#M (ψ → 2)"
    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 "f : ℵ → ψ →^[G] 2"
proof -
  have "x ∈ B ==> B ∈ G ==> x ∈ ℵ × (ψ →^[G] 2)" for B x
  proof -
    assume "x∈B" "B∈G"
    moreover from this
    have "x ∈ M[G]"
      by (auto dest!: ext.transM simp add:G_in_MG)
    moreover from calculation
    have "x ∈ ℵ × (ψ → 2)"
      using Fn_rel_subset_Pow[of "ℵ" "ℵ" "ψ → 2",
          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∈ℵ" "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(f)"
    using Un_filter_is_function generic
    by fast
  ultimately
  show ?thesis
    using generic domain_f_G Pi_iff by auto
qed

abbreviation
  surj_dense :: "i==>i" where
  "surj_dense(x) ≡ { p∈Coll . x ∈ range(p) }"

lemma surj_dense_closed[intro,simp]:
  "x ∈ ψ → 2 ==> surj_dense(x) ∈ M"
  using separation_in_range transM[of x] by simp

lemma reals_sub_image_f_G:
  assumes "x ∈ ψ → 2"
  shows "∃α∈ℵ. f ` α = 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 ∈ ψ → 2›
  obtain p where "p∈surj_dense(x)" "p∈G"
    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: "f ∈ surj^[G](ℵ, ψ →^[G] 2)"
  using Aleph_rel_sub_closed
proof (intro ext.mem_surj_abs[THEN iffD2],simp_all)
  show "f ∈ surj(ℵ, ψ →^[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^{<up>ℵ[G],M[G]} ≤ ℵ^[G]"
proof -
  have "ℵ ∈ M[G]" "Ord(ℵ)"
    using Card_rel_is_Ord by auto
  moreover from this
  have "ψ →^[G] 2 <^[G] ℵ"
    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(ℵ)›
  have "|ψ →^[G] 2|^[G] ≤ |ℵ|^[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^{<up>ℵ[G],M[G]} ≤ |ℵ^[G]|^[G]"
    using ext.lepoll_rel_imp_cardinal_rel_le[of "ℵ" "ψ →^[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^{<up>ℵ[G],M[G]} ≤ ℵ^[G]" by simp
qed

theorem CH: "ℵ^[G] = 2^{<up>ℵ[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^{<up>ℵ[G],M[G]}" ψ]
    ext.Card_rel_cexp_rel ext.cantor_cexp_rel[of ψ] ext.Card_rel_nat
    le_anti_sym
  by auto

end ― ‹🍋‹collapse_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 "ℵ" "ℵ" "ψ → 2"]
      zero_top_Fn_rel[of _ "ℵ" "ℵ" "ψ → 2"]
      preorder_on_Fnle_rel[of "ℵ" "ℵ" "ψ → 2"]
      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 "ℵ^[G] = 2^{<up>ℵ[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