Theory Not_CH
section‹Model of the negation of the Continuum Hypothesis›
theory Not_CH
imports
Cardinal_Preservation
begin
text‹We are taking advantage that the poset of finite functions is absolute,
and thus we work with the unrelativized \<^term>‹Fn›. But it would have been more
appropriate to do the following using the relative \<^term>‹Fn_rel›. As it turns
out, the present theory was developed prior to having \<^term>‹Fn› relativized!
We also note that \<^term>‹Fn(ω,κ×ω,2)› is separative, i.e. each \<^term>‹X ∈ Fn(ω,κ×ω,2)›
has two incompatible extensions; therefore we may recover part of our previous theorem
@{thm [source] extensions_of_ctms_ZF}. But that result also included the possibility
of not having $\AC$ in the ground model, which would not be sensible in a context
where the cardinality of the continuum is under discussion. It is also the case that
@{thm [source] extensions_of_ctms_ZF} was historically our first formalized result
(with a different proof) that showed the forcing machinery had all of its elements
in place.›
abbreviation
Add_subs :: "i ⇒ i" where
"Add_subs(κ) ≡ Fn(ω,κ×ω,2)"
abbreviation
Add_le :: "i ⇒ i" where
"Add_le(κ) ≡ Fnle(ω,κ × ω,2)"
lemma (in M_aleph) Aleph_rel2_closed[intro,simp]: "M(ℵ⇘2⇙⇗M⇖)"
using nat_into_Ord by simp
locale M_master = M_cohen + M_library +
assumes
UN_lepoll_assumptions:
"M(A) ⟹ M(b) ⟹ M(f) ⟹ M(A') ⟹ separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x∈if_range_F_else_F((`)(A), b, f, i)⟩)"
subsection‹Non-absolute concepts between extensions›
sublocale M_master ⊆ M_Pi_replacement
by unfold_locales
locale M_master_sub = M_master + N:M_aleph N for N +
assumes
M_imp_N: "M(x) ⟹ N(x)" and
Ord_iff: "Ord(x) ⟹ M(x) ⟷ N(x)"
sublocale M_master_sub ⊆ M_N_Perm
using M_imp_N by unfold_locales
context M_master_sub
begin
lemma cardinal_rel_le_cardinal_rel: "M(X) ⟹ |X|⇗N⇖ ≤ |X|⇗M⇖"
using M_imp_N N.lepoll_rel_cardinal_rel_le[OF lepoll_rel_transfer Card_rel_is_Ord]
cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym, THEN eqpoll_rel_imp_lepoll_rel]
by simp
lemma Aleph_rel_sub_closed: "Ord(α) ⟹ M(α) ⟹ N(ℵ⇘α⇙⇗M⇖)"
using Ord_iff[THEN iffD1, OF Card_rel_Aleph_rel[THEN Card_rel_is_Ord]]
by simp
lemma Card_rel_imp_Card_rel: "Card⇗N⇖(κ) ⟹ M(κ) ⟹ Card⇗M⇖(κ)"
using N.Card_rel_is_Ord[of κ] M_imp_N Ord_cardinal_rel_le[of κ]
cardinal_rel_le_cardinal_rel[of κ] le_anti_sym
unfolding Card_rel_def by auto
lemma csucc_rel_le_csucc_rel:
assumes "Ord(κ)" "M(κ)"
shows "(κ⇧+)⇗M⇖ ≤ (κ⇧+)⇗N⇖"
proof -
note assms
moreover from this
have "N(L) ∧ Card⇗N⇖(L) ∧ κ < L ⟹ M(L) ∧ Card⇗M⇖(L) ∧ κ < L"
(is "?P(L) ⟹ ?Q(L)") for L
using M_imp_N Ord_iff[THEN iffD2, of L] N.Card_rel_is_Ord lt_Ord
Card_rel_imp_Card_rel by auto
moreover from assms
have "N((κ⇧+)⇗N⇖)" "Card⇗N⇖((κ⇧+)⇗N⇖)" "κ < (κ⇧+)⇗N⇖"
using N.lt_csucc_rel[of κ] N.Card_rel_csucc_rel[of κ] M_imp_N by simp_all
ultimately
show ?thesis
using M_imp_N Least_antitone[of _ ?P ?Q] unfolding csucc_rel_def by blast
qed
lemma Aleph_rel_le_Aleph_rel: "Ord(α) ⟹ M(α) ⟹ ℵ⇘α⇙⇗M⇖ ≤ ℵ⇘α⇙⇗N⇖"
proof (induct rule:trans_induct3)
case 0
then
show ?case
using Aleph_rel_zero N.Aleph_rel_zero by simp
next
case (succ x)
then
have "ℵ⇘x⇙⇗M⇖ ≤ ℵ⇘x⇙⇗N⇖" "Ord(x)" "M(x)" by simp_all
moreover from this
have "(ℵ⇘x⇙⇗M⇖⇧+)⇗M⇖ ≤ (ℵ⇘x⇙⇗N⇖⇧+)⇗M⇖"
using M_imp_N Ord_iff[THEN iffD2, OF N.Card_rel_is_Ord]
by (intro csucc_rel_le_mono) simp_all
moreover from calculation
have "(ℵ⇘x⇙⇗N⇖⇧+)⇗M⇖ ≤ (ℵ⇘x⇙⇗N⇖⇧+)⇗N⇖"
using M_imp_N N.Card_rel_is_Ord Ord_iff[THEN iffD2, OF N.Card_rel_is_Ord]
by (intro csucc_rel_le_csucc_rel) auto
ultimately
show ?case
using M_imp_N Aleph_rel_succ N.Aleph_rel_succ csucc_rel_le_csucc_rel
le_trans by auto
next
case (limit x)
then
show ?case
using M_imp_N Aleph_rel_limit N.Aleph_rel_limit
by simp (blast dest: transM intro!:le_implies_UN_le_UN)
qed
end
lemmas (in M_ZF2_trans) sep_instances =
separation_ifrangeF_body separation_ifrangeF_body2 separation_ifrangeF_body3
separation_ifrangeF_body4 separation_ifrangeF_body5 separation_ifrangeF_body6
separation_ifrangeF_body7 separation_cardinal_rel_lesspoll_rel
separation_is_dcwit_body separation_cdltgamma separation_cdeqgamma
lemmas (in M_ZF2_trans) repl_instances = lam_replacement_inj_rel
sublocale M_ZFC2_ground_notCH_trans ⊆ M_master "##M"
using replacement_trans_apply_image
by unfold_locales (simp_all add:repl_instances sep_instances del:setclass_iff
add: transrec_replacement_def wfrec_replacement_def)
sublocale M_ZFC2_trans ⊆ M_Pi_replacement "##M"
by unfold_locales
subsection‹Cohen forcing is ccc›
context M_ctm2_AC
begin
lemma ccc_Add_subs_Aleph_2: "ccc⇗M⇖(Add_subs(ℵ⇘2⇙⇗M⇖),Add_le(ℵ⇘2⇙⇗M⇖))"
proof -
interpret M_add_reals "##M" "ℵ⇘2⇙⇗M⇖ × ω"
by unfold_locales blast
show ?thesis
using ccc_rel_Fn_nat by fast
qed
end
sublocale G_generic3_AC ⊆ M_master_sub "##M" "##(M[G])"
using M_subset_MG[OF one_in_G] generic Ord_MG_iff
by unfold_locales auto
lemma (in M_trans) mem_F_bound4:
fixes F A
defines "F ≡ (`)"
shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ domain(A))"
using apply_0 unfolding F_def
by (cases "M(c)", auto simp:F_def)
lemma (in M_trans) mem_F_bound5:
fixes F A
defines "F ≡ λ_ x. A`x "
shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ domain(A))"
using apply_0 unfolding F_def
by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)
sublocale M_ctm2_AC ⊆ M_replacement_lepoll "##M" "(`)"
using UN_lepoll_assumptions lam_replacement_apply lam_replacement_inj_rel
mem_F_bound4 apply_0 lam_replacement_minimum
unfolding lepoll_assumptions_defs
proof (unfold_locales,
rule_tac [3] lam_Least_assumption_general[where U=domain, OF _ mem_F_bound4], simp_all)
fix A i x
assume "A ∈ M" "x ∈ M" "x ∈ A ` i"
then
show "i ∈ M"
using apply_0[of i A] transM[of _ "domain(A)", simplified]
by force
qed
context G_generic3_AC begin
context
includes G_generic1_lemmas
begin
lemma G_in_MG: "G ∈ M[G]"
using G_in_Gen_Ext
by blast
lemma ccc_preserves_Aleph_succ:
assumes "ccc⇗M⇖(ℙ,leq)" "Ord(z)" "z ∈ M"
shows "Card⇗M[G]⇖(ℵ⇘succ(z)⇙⇗M⇖)"
proof (rule ccontr)
assume "¬ Card⇗M[G]⇖(ℵ⇘succ(z)⇙⇗M⇖)"
moreover
note ‹z ∈ M› ‹Ord(z)›
moreover from this
have "Ord(ℵ⇘succ(z)⇙⇗M⇖)"
using Card_rel_is_Ord by fastforce
ultimately
obtain α f where "α < ℵ⇘succ(z)⇙⇗M⇖" "f ∈ surj⇗M[G]⇖(α, ℵ⇘succ(z)⇙⇗M⇖)"
using ext.lt_surj_rel_empty_imp_Card_rel M_subset_MG[OF one_in_G]
by force
moreover from this and ‹z∈M› ‹Ord(z)›
have "α ∈ M" "f ∈ M[G]"
using ext.trans_surj_rel_closed
by (auto dest:transM ext.transM dest!:ltD)
moreover
note ‹ccc⇗M⇖(ℙ,leq)› ‹z∈M›
ultimately
obtain F where "F:α→Pow⇗M⇖(ℵ⇘succ(z)⇙⇗M⇖)" "∀β∈α. f`β ∈ F`β" "∀β∈α. |F`β|⇗M⇖ ≤ ω"
"F ∈ M"
using ccc_fun_approximation_lemma[of α "ℵ⇘succ(z)⇙⇗M⇖" f]
ext.mem_surj_abs[of f α "ℵ⇘succ(z)⇙⇗M⇖"] ‹Ord(z)›
surj_is_fun[of f α "ℵ⇘succ(z)⇙⇗M⇖"] by auto
then
have "β ∈ α ⟹ |F`β|⇗M⇖ ≤ ℵ⇘0⇙⇗M⇖" for β
using Aleph_rel_zero by simp
have "w ∈ F ` x ⟹ x ∈ M" for w x
proof -
fix w x
assume "w ∈ F`x"
then
have "x ∈ domain(F)"
using apply_0 by auto
with ‹F:α→Pow⇗M⇖(ℵ⇘succ(z)⇙⇗M⇖)› ‹α ∈ M›
show "x ∈ M" using domain_of_fun
by (auto dest:transM)
qed
with ‹α ∈ M› ‹F:α→Pow⇗M⇖(ℵ⇘succ(z)⇙⇗M⇖)› ‹F∈M›
interpret M_cardinal_UN_lepoll "##M" "λβ. F`β" α
using UN_lepoll_assumptions lepoll_assumptions
lam_replacement_apply lam_replacement_inj_rel lam_replacement_minimum
proof (unfold_locales, auto dest:transM simp del:if_range_F_else_F_def)
fix f b
assume "b∈M" "f∈M"
with ‹F∈M›
show "lam_replacement(##M, λx. μ i. x ∈ if_range_F_else_F((`)(F), b, f, i))"
using UN_lepoll_assumptions mem_F_bound5
by (rule_tac lam_Least_assumption_general[where U="domain", OF _ mem_F_bound5])
simp_all
qed
from ‹α < ℵ⇘succ(z)⇙⇗M⇖› ‹α ∈ M› ‹Ord(z)› ‹z∈M›
have "α ≲⇗M⇖ ℵ⇘z⇙⇗M⇖"
using
cardinal_rel_lt_csucc_rel_iff[of "ℵ⇘z⇙⇗M⇖" α]
le_Card_rel_iff[of "ℵ⇘z⇙⇗M⇖" α]
Aleph_rel_succ[of z] Card_rel_lt_iff[of α "ℵ⇘succ(z)⇙⇗M⇖"]
lt_Ord[of α "ℵ⇘succ(z)⇙⇗M⇖"]
Card_rel_csucc_rel[of "ℵ⇘z⇙⇗M⇖"]
Card_rel_Aleph_rel[THEN Card_rel_is_Ord]
by simp
with ‹α < ℵ⇘succ(z)⇙⇗M⇖› ‹∀β∈α. |F`β|⇗M⇖ ≤ ω› ‹α ∈ M› assms
have "|⋃β∈α. F`β|⇗M⇖ ≤ ℵ⇘z⇙⇗M⇖"
using InfCard_rel_Aleph_rel[of z] Aleph_rel_zero
subset_imp_lepoll_rel[THEN lepoll_rel_imp_cardinal_rel_le,
of "⋃β∈α. F`β" "ℵ⇘z⇙⇗M⇖"] Aleph_rel_succ
Aleph_rel_increasing[THEN leI, THEN [2] le_trans, of _ 0 z]
Ord_0_lt_iff[THEN iffD1, of z]
by (cases "0<z"; rule_tac lepoll_rel_imp_cardinal_rel_UN_le) (auto, force)
moreover
note ‹z∈M› ‹Ord(z)›
moreover from ‹∀β∈α. f`β ∈ F`β› ‹f ∈ surj⇗M[G]⇖(α, ℵ⇘succ(z)⇙⇗M⇖)›
‹α ∈ M› ‹f ∈ M[G]› and this
have "ℵ⇘succ(z)⇙⇗M⇖ ⊆ (⋃β∈α. F`β)"
using ext.mem_surj_abs by (force simp add:surj_def)
moreover from ‹F ∈ M› ‹α ∈ M›
have "(⋃x∈α. F ` x) ∈ M"
using j.B_replacement
by (intro Union_closed[simplified] RepFun_closed[simplified])
(auto dest:transM)
ultimately
have "ℵ⇘succ(z)⇙⇗M⇖ ≤ ℵ⇘z⇙⇗M⇖"
using subset_imp_le_cardinal_rel[of "ℵ⇘succ(z)⇙⇗M⇖" "⋃β∈α. F`β"]
le_trans by auto
with assms
show "False"
using Aleph_rel_increasing not_le_iff_lt[of "ℵ⇘succ(z)⇙⇗M⇖" "ℵ⇘z⇙⇗M⇖"]
Card_rel_Aleph_rel[THEN Card_rel_is_Ord]
by auto
qed
end
end
context M_ctm1
begin
abbreviation
Add :: "i" where
"Add ≡ Fn(ω, ℵ⇘2⇙⇗M⇖ × ω, 2)"
end
locale add_generic3 = G_generic3_AC "Fn(ω, ℵ⇘2⇙⇗##M⇖ × ω, 2)" "Fnle(ω, ℵ⇘2⇙⇗##M⇖ × ω, 2)" 0
sublocale add_generic3 ⊆ cohen_data ω "ℵ⇘2⇙⇗M⇖ × ω" 2 by unfold_locales auto
context add_generic3
begin
notation Leq (infixl ‹≼› 50)
notation Incompatible (infixl ‹⊥› 50)
lemma Add_subs_preserves_Aleph_succ: "Ord(z) ⟹ z∈M ⟹ Card⇗M[G]⇖(ℵ⇘succ(z)⇙⇗M⇖)"
using ccc_preserves_Aleph_succ ccc_Add_subs_Aleph_2
by auto
lemma Aleph_rel_nats_MG_eq_Aleph_rel_nats_M:
includes G_generic1_lemmas
assumes "z ∈ ω"
shows "ℵ⇘z⇙⇗M[G]⇖ = ℵ⇘z⇙⇗M⇖"
using assms
proof (induct)
case 0
show ?case
by(rule trans[OF ext.Aleph_rel_zero Aleph_rel_zero[symmetric]])
next
case (succ z)
then
have "ℵ⇘succ(z)⇙⇗M⇖ ≤ ℵ⇘succ(z)⇙⇗M[G]⇖"
using Aleph_rel_le_Aleph_rel nat_into_M by simp
moreover from ‹z ∈ ω›
have "ℵ⇘z⇙⇗M⇖ ∈ M[G]" "ℵ⇘succ(z)⇙⇗M⇖ ∈ M[G]"
using nat_into_M by simp_all
moreover from this and ‹ℵ⇘z⇙⇗M[G]⇖ = ℵ⇘z⇙⇗M⇖› ‹z ∈ ω›
have "ℵ⇘succ(z)⇙⇗M[G]⇖ ≤ ℵ⇘succ(z)⇙⇗M⇖"
using ext.Aleph_rel_succ nat_into_M
Add_subs_preserves_Aleph_succ[THEN ext.csucc_rel_le, of z]
Aleph_rel_increasing[of z "succ(z)"]
by simp
ultimately
show ?case using le_anti_sym by blast
qed
abbreviation
f_G :: "i" (‹f⇘G⇙›) where
"f⇘G⇙ ≡ ⋃G"
abbreviation
dom_dense :: "i ⇒ i" where
"dom_dense(x) ≡ {p ∈ Add . x ∈ domain(p) }"
declare (in M_ctm2_AC) Fn_nat_closed[simplified setclass_iff, simp, intro]
declare (in M_ctm2_AC) Fnle_nat_closed[simp del, rule del,
simplified setclass_iff, simp, intro]
declare (in M_ctm2_AC) cexp_rel_closed[simplified setclass_iff, simp, intro]
declare (in G_generic3_AC) ext.cexp_rel_closed[simplified setclass_iff, simp, intro]
lemma dom_dense_closed[intro,simp]: "x ∈ ℵ⇘2⇙⇗M⇖ × ω ⟹ dom_dense(x) ∈ M"
using separation_in_domain[of x] nat_into_M
by (rule_tac separation_closed[simplified], blast dest:transM) simp
lemma domain_f_G: assumes "x ∈ ℵ⇘2⇙⇗M⇖" "y ∈ ω"
shows "⟨x, y⟩ ∈ domain(f⇘G⇙)"
proof -
from assms
have "Add = Fn⇗M⇖(ω,ℵ⇘2⇙⇗M⇖×ω,2)"
using Fn_nat_abs by auto
moreover from this
have "Fnle(ω,ℵ⇘2⇙⇗M⇖×ω,2) = Fnle⇗M⇖(ω,ℵ⇘2⇙⇗M⇖×ω,2)"
unfolding Fnle_rel_def Fnle_def by auto
moreover from calculation assms
have "dense(dom_dense(⟨x, y⟩))"
using dense_dom_dense[of "⟨x,y⟩" "ℵ⇘2⇙⇗M⇖×ω" ω 2] InfCard_rel_nat
unfolding dense_def by auto
with assms
obtain p where "p∈dom_dense(⟨x, y⟩)" "p∈G"
using M_generic_denseD[of "dom_dense(⟨x, y⟩)"]
by auto
then
show "⟨x, y⟩ ∈ domain(f⇘G⇙)" by blast
qed
lemma f_G_funtype:
includes G_generic1_lemmas
shows "f⇘G⇙ : ℵ⇘2⇙⇗M⇖ × ω → 2"
using generic domain_f_G Pi_iff Un_filter_is_function generic
subset_trans[OF filter_subset_notion Fn_nat_subset_Pow]
by force
lemma inj_dense_closed[intro,simp]:
"w ∈ ℵ⇘2⇙⇗M⇖ ⟹ x ∈ ℵ⇘2⇙⇗M⇖ ⟹ inj_dense(ℵ⇘2⇙⇗M⇖,2,w,x) ∈ M"
using transM[OF _ Aleph_rel2_closed] separation_conj separation_bex
lam_replacement_product
separation_in lam_replacement_fst lam_replacement_snd lam_replacement_constant
lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_restrict']
separation_bex separation_conj
by simp
lemma Aleph_rel2_new_reals:
assumes "w ∈ ℵ⇘2⇙⇗M⇖" "x ∈ ℵ⇘2⇙⇗M⇖" "w ≠ x"
shows "(λn∈ω. f⇘G⇙ ` ⟨w, n⟩) ≠ (λn∈ω. f⇘G⇙ ` ⟨x, n⟩)"
proof -
have "0∈2" by auto
with assms
have "dense(inj_dense(ℵ⇘2⇙⇗M⇖,2,w,x))"
unfolding dense_def using dense_inj_dense by auto
with assms
obtain p where "p∈inj_dense(ℵ⇘2⇙⇗M⇖,2,w,x)" "p∈G"
using M_generic_denseD[of "inj_dense(ℵ⇘2⇙⇗M⇖,2,w,x)"]
by blast
then
obtain n where "n ∈ ω" "⟨⟨w, n⟩, 1⟩ ∈ p" "⟨⟨x, n⟩, 0⟩ ∈ p"
by blast
moreover from this and ‹p∈G›
have "⟨⟨w, n⟩, 1⟩ ∈ f⇘G⇙" "⟨⟨x, n⟩, 0⟩ ∈ f⇘G⇙" by auto
moreover from calculation
have "f⇘G⇙ ` ⟨w, n⟩ = 1" "f⇘G⇙ ` ⟨x, n⟩ = 0"
using f_G_funtype apply_equality
by auto
ultimately
have "(λn∈ω. f⇘G⇙ ` ⟨w, n⟩) ` n ≠ (λn∈ω. f⇘G⇙ ` ⟨x, n⟩) ` n"
by simp
then
show ?thesis by fastforce
qed
definition
h_G :: "i" (‹h⇘G⇙›) where
"h⇘G⇙ ≡ λα∈ℵ⇘2⇙⇗M⇖. λn∈ω. f⇘G⇙`⟨α,n⟩"
lemma h_G_in_MG[simp]:
includes G_generic1_lemmas
shows "h⇘G⇙ ∈ M[G]"
using ext.curry_closed[unfolded curry_def] G_in_MG
unfolding h_G_def
by simp
lemma h_G_inj_Aleph_rel2_reals: "h⇘G⇙ ∈ inj⇗M[G]⇖(ℵ⇘2⇙⇗M⇖, ω →⇗M[G]⇖ 2)"
using Aleph_rel_sub_closed f_G_funtype G_in_MG Aleph_rel_sub_closed
ext.curry_rel_exp[unfolded curry_def] ext.curry_closed[unfolded curry_def]
ext.mem_function_space_rel_abs
by (intro ext.mem_inj_abs[THEN iffD2],simp_all)
(auto simp: inj_def h_G_def dest:Aleph_rel2_new_reals)
lemma Aleph2_extension_le_continuum_rel:
includes G_generic1_lemmas
shows "ℵ⇘2⇙⇗M[G]⇖ ≤ 2⇗↑ℵ⇘0⇙⇗M[G]⇖,M[G]⇖"
proof -
have "ℵ⇘2⇙⇗M[G]⇖ ≲⇗M[G]⇖ ω →⇗M[G]⇖ 2"
using ext.def_lepoll_rel[of "ℵ⇘2⇙⇗M⇖" "ω →⇗M[G]⇖ 2"]
h_G_inj_Aleph_rel2_reals Aleph_rel_nats_MG_eq_Aleph_rel_nats_M
by auto
moreover from calculation
have "ℵ⇘2⇙⇗M[G]⇖ ≲⇗M[G]⇖ |ω →⇗M[G]⇖ 2|⇗M[G]⇖"
using ext.lepoll_rel_imp_lepoll_rel_cardinal_rel by simp
ultimately
have "|ℵ⇘2⇙⇗M[G]⇖|⇗M[G]⇖ ≤ 2⇗↑ℵ⇘0⇙⇗M[G]⇖,M[G]⇖"
using ext.lepoll_rel_imp_cardinal_rel_le[of "ℵ⇘2⇙⇗M[G]⇖" "ω →⇗M[G]⇖ 2",
OF _ _ ext.function_space_rel_closed]
ext.Aleph_rel_zero
unfolding cexp_rel_def by simp
then
show "ℵ⇘2⇙⇗M[G]⇖ ≤ 2⇗↑ℵ⇘0⇙⇗M[G]⇖,M[G]⇖"
using ext.Card_rel_Aleph_rel[of 2, THEN ext.Card_rel_cardinal_rel_eq]
by simp
qed
lemma Aleph_rel_lt_continuum_rel: "ℵ⇘1⇙⇗M[G]⇖ < 2⇗↑ℵ⇘0⇙⇗M[G]⇖,M[G]⇖"
using Aleph2_extension_le_continuum_rel
ext.Aleph_rel_increasing[of 1 2] le_trans by auto
corollary not_CH: "ℵ⇘1⇙⇗M[G]⇖ ≠ 2⇗↑ℵ⇘0⇙⇗M[G]⇖,M[G]⇖"
using Aleph_rel_lt_continuum_rel by auto
end
subsection‹Models of fragments of $\ZFC + \neg \CH$›
definition
ContHyp :: "o" where
"ContHyp ≡ ℵ⇘1⇙ = 2⇗↑ℵ⇘0⇙⇖"
relativize functional "ContHyp" "ContHyp_rel"
notation ContHyp_rel (‹CH⇗_⇖›)
relationalize "ContHyp_rel" "is_ContHyp"
context M_ZF_library
begin
is_iff_rel for "ContHyp"
using is_cexp_iff is_Aleph_iff[of 0] is_Aleph_iff[of 1]
unfolding is_ContHyp_def ContHyp_rel_def
by (auto simp del:setclass_iff) (rule rexI[of _ _ M, OF _ nonempty], auto)
end
synthesize "is_ContHyp" from_definition assuming "nonempty"
arity_theorem for "is_ContHyp_fm"
notation is_ContHyp_fm (‹⋅CH⋅›)
theorem ctm_of_not_CH:
assumes
"M ≈ ω" "Transset(M)" "M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}"
"Φ ⊆ 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_notCH}›
interpret M_ZFC3 M
using M_satT_overhead_imp_M_ZF3 unfolding overhead_notCH_def by force
from ‹M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}› ‹Transset(M)›
interpret M_ZF_ground_notCH_trans M
using M_satT_imp_M_ZF_ground_notCH_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_ctm3_AC M enum by unfold_locales
interpret cohen_data ω "ℵ⇘2⇙⇗M⇖ × ω" 2 by unfold_locales auto
have "Add ∈ M" "Add_le(ℵ⇘2⇙⇗M⇖) ∈ M"
using nat_into_M Aleph_rel_closed M_nat cartprod_closed Fn_nat_closed Fnle_nat_closed
by simp_all
then
interpret forcing_data1 "Add" "Add_le(ℵ⇘2⇙⇗M⇖)" 0 M enum
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 add_generic3 M enum G by unfold_locales
have "¬ (ℵ⇘1⇙⇗M[G]⇖ = 2⇗↑ℵ⇘0⇙⇗M[G]⇖,M[G]⇖)"
using not_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
lemma ZF_replacement_overhead_sub_ZFC: "{⋅Replacement(p)⋅ . p ∈ overhead} ⊆ ZFC"
using overhead_type unfolding ZFC_def ZF_def ZF_schemes_def by auto
lemma ZF_replacement_overhead_notCH_sub_ZFC: "{⋅Replacement(p)⋅ . p ∈ overhead_notCH} ⊆ ZFC"
using overhead_notCH_type unfolding ZFC_def ZF_def ZF_schemes_def by auto
lemma ZF_replacement_overhead_CH_sub_ZFC: "{⋅Replacement(p)⋅ . p ∈ overhead_CH} ⊆ ZFC"
using overhead_CH_type unfolding ZFC_def ZF_def ZF_schemes_def by auto
corollary ctm_ZFC_imp_ctm_not_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_not_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_notCH_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⋅⋅}"
by auto
ultimately
show ?thesis by auto
qed
end