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⇖, ω →⇗M⇖ 2)"
abbreviation
Colleq :: "i" where
"Colleq ≡ Fnle⇗M⇖(ℵ⇘1⇙⇗M⇖, ℵ⇘1⇙⇗M⇖, ω →⇗M⇖ 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›
lemma succ_omega_closed_Coll: "succ(ω)-closed⇗M⇖(Coll,Colleq)"
proof -
have "n∈ω ⟹ ∀f ∈ n ⇩<→⇗M⇖ (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) ⇩<→⇗M⇖ (Coll,converse(Colleq)). ∀α ∈ succ(x). ⟨f`x, f ` α⟩ ∈ Colleq"
proof(intro ballI)
fix f α
assume "f∈succ(x) ⇩<→⇗M⇖ (Coll,converse(Colleq))" "α∈succ(x)"
moreover from ‹x∈ω› this
have "f∈succ(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))" "x∈succ(x)" "α∈succ(x)"
by auto
with ‹f∈succ(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 ‹f∈succ(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
have "∀f∈M. f ∈ ω ⇩<→⇗M⇖ (Coll,converse(Colleq)) ⟶
(∃q∈M. q ∈ Coll ∧ (∀α∈M. α ∈ ω ⟶ ⟨q, f ` α⟩ ∈ Colleq))"
proof(intro ballI impI)
fix f
let ?rnf="f``ω"
assume "f∈M" "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 "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 ⊆ (ℵ⇘1⇙⇗M⇖ ⇀⇗##M⇖ (nat →⇗M⇖ 2))"
using subset_trans[OF image_subset[OF ‹f⊆_›,of ω] Fn_rel_subset_PFun_rel]
by simp
moreover
have "⋃ ?rnf ∈ (ℵ⇘1⇙⇗M⇖ ⇀⇗##M⇖ (nat →⇗M⇖ 2))"
using pfun_Un_filter_closed'[OF ‹?rnf⊆_› 1] ‹?rnf∈M›
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 ‹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
locale collapse_CH = G_generic3_AC_CH "Fn⇗M⇖(ℵ⇘1⇙⇗##M⇖, ℵ⇘1⇙⇗M⇖, ω →⇗M⇖ 2)" "Fnle⇗M⇖(ℵ⇘1⇙⇗##M⇖, ℵ⇘1⇙⇗M⇖, ω →⇗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⇘G⇙›) where
"f⇘G⇙ ≡ ⋃G"
lemma f_G_in_MG[simp]:
shows "f⇘G⇙ ∈ 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 ∈ ℵ⇘1⇙⇗M⇖"
shows "x ∈ domain(f⇘G⇙)"
proof -
have "(λn∈ω. 0) ∈ ω →⇗M⇖ 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⇘G⇙)" by blast
qed
lemma Un_filter_is_function:
assumes "filter(G)"
shows "function(⋃G)"
proof -
have "Coll ⊆ ℵ⇘1⇙⇗M⇖ ⇀⇗##M⇖ (ω →⇗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 ∈ ℵ⇘1⇙⇗M⇖ ⇀⇗##M⇖ (ω →⇗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 ⊆ ℵ⇘1⇙⇗M⇖ ⇀⇗##M⇖ (ω →⇗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⇙ : ℵ⇘1⇙⇗M⇖ → ω →⇗M[G]⇖ 2"
proof -
have "x ∈ B ⟹ B ∈ G ⟹ x ∈ ℵ⇘1⇙⇗M⇖ × (ω →⇗M[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 ∈ ℵ⇘1⇙⇗M⇖ × (ω → 2)"
using Fn_rel_subset_Pow[of "ℵ⇘1⇙⇗M⇖" "ℵ⇘1⇙⇗M⇖" "ω →⇗M⇖ 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∈ℵ⇘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(f⇘G⇙)"
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 ∈ ω →⇗M⇖ 2 ⟹ surj_dense(x) ∈ M"
using separation_in_range transM[of x] by simp
lemma reals_sub_image_f_G:
assumes "x ∈ ω →⇗M⇖ 2"
shows "∃α∈ℵ⇘1⇙⇗M⇖. f⇘G⇙ ` α = 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 ∈ ω →⇗M⇖ 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⇘G⇙ ∈ surj⇗M[G]⇖(ℵ⇘1⇙⇗M⇖, ω →⇗M[G]⇖ 2)"
using Aleph_rel_sub_closed
proof (intro ext.mem_surj_abs[THEN iffD2],simp_all)
show "f⇘G⇙ ∈ 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
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⇖" "ω →⇗M⇖ 2"]
zero_top_Fn_rel[of _ "ℵ⇘1⇙⇗M⇖" "ℵ⇘1⇙⇗M⇖" "ω →⇗M⇖ 2"]
preorder_on_Fnle_rel[of "ℵ⇘1⇙⇗M⇖" "ℵ⇘1⇙⇗M⇖" "ω →⇗M⇖ 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 "ℵ⇘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