Theory Cardinal_Preservation
section‹Preservation of cardinals in generic extensions›
theory Cardinal_Preservation
imports
Forcing_Main
begin
context forcing_data1
begin
lemma antichain_abs' [absolut]:
"⟦ A∈M ⟧ ⟹ antichain⇗M⇖(ℙ,leq,A) ⟷ antichain(ℙ,leq,A)"
unfolding antichain_rel_def antichain_def compat_def
using transitivity[of _ A]
by (auto simp add:absolut)
lemma inconsistent_imp_incompatible:
assumes "p ⊩ φ env" "q ⊩ Neg(φ) env" "p∈ℙ" "q∈ℙ"
"arity(φ) ≤ length(env)" "φ ∈ formula" "env ∈ list(M)"
shows "p ⊥ q"
proof
assume "compat(p,q)"
then
obtain d where "d ≼ p" "d ≼ q" "d ∈ ℙ" by blast
moreover
note assms
moreover from calculation
have "d ⊩ φ env" "d ⊩ Neg(φ) env"
using strengthening_lemma by simp_all
ultimately
show "False"
using Forces_Neg[of d env φ] refl_leq
by (auto dest:transitivity; drule_tac bspec; auto dest:transitivity)
qed
notation check (‹_⇧v› [101] 100)
end
locale G_generic2 = G_generic1 + forcing_data2
locale G_generic2_AC = G_generic1_AC + G_generic2
locale G_generic3 = G_generic2 + forcing_data3
locale G_generic3_AC = G_generic2_AC + G_generic3
locale G_generic3_AC_CH = G_generic3_AC + M_ZFC2_ground_CH_trans
sublocale G_generic3_AC ⊆ ext:M_ZFC2_trans "M[G]"
using ground_replacements3 replacement_assm_MG
by unfold_locales simp_all
lemma (in forcing_data1) forces_neq_apply_imp_incompatible:
assumes
"p ⊩ ⋅0`1 is 2⋅ [f,a,b⇧v]"
"q ⊩ ⋅0`1 is 2⋅ [f,a,b'⇧v]"
"b ≠ b'"
and
types:"f∈M" "a∈M" "b∈M" "b'∈M" "p∈ℙ" "q∈ℙ"
shows
"p ⊥ q"
proof -
{
fix G
assume "M_generic(G)"
then
interpret G_generic1 _ _ _ _ _ G by unfold_locales
include G_generic1_lemmas
assume "q∈G"
with assms ‹M_generic(G)›
have "M[G], map(val(G),[f,a,b'⇧v]) ⊨ ⋅0`1 is 2⋅"
using truth_lemma[of "⋅0`1 is 2⋅" "[f,a,b'⇧v]"]
by (auto simp add:ord_simp_union arity_fun_apply_fm
fun_apply_type)
with ‹b ≠ b'› types
have "M[G], map(val(G),[f,a,b⇧v]) ⊨ ⋅¬⋅0`1 is 2⋅⋅"
using GenExtI by auto
}
with types
have "q ⊩ ⋅¬⋅0`1 is 2⋅⋅ [f,a,b⇧v]"
using definition_of_forcing[where φ="⋅¬⋅0`1 is 2⋅⋅" ]
by (auto simp add:ord_simp_union arity_fun_apply_fm)
with ‹p ⊩ ⋅0`1 is 2⋅ [f,a,b⇧v]› and types
show "p ⊥ q"
using inconsistent_imp_incompatible
by (simp add:ord_simp_union arity_fun_apply_fm fun_apply_type)
qed
context M_ctm2_AC
begin
lemmas sharp_simps = Card_rel_Union Card_rel_cardinal_rel Collect_abs
Cons_abs Cons_in_M_iff Diff_closed Equal_abs Equal_in_M_iff Finite_abs
Forall_abs Forall_in_M_iff Inl_abs Inl_in_M_iff Inr_abs Inr_in_M_iff
Int_closed Inter_abs Inter_closed M_nat Member_abs Member_in_M_iff
Memrel_closed Nand_abs Nand_in_M_iff Nil_abs Nil_in_M Ord_cardinal_rel
Pow_rel_closed Un_closed Union_abs Union_closed and_abs and_closed
apply_abs apply_closed bij_rel_closed bijection_abs bool_of_o_abs
bool_of_o_closed cadd_rel_0 cadd_rel_closed cardinal_rel_0_iff_0
cardinal_rel_closed cardinal_rel_idem cartprod_abs cartprod_closed
cmult_rel_0 cmult_rel_1 cmult_rel_closed comp_closed composition_abs
cons_abs cons_closed converse_abs converse_closed csquare_lam_closed
csquare_rel_closed depth_closed domain_abs domain_closed eclose_abs
eclose_closed empty_abs field_abs field_closed finite_funspace_closed
finite_ordinal_abs fst_closed function_abs function_space_rel_closed
hd_abs image_abs image_closed inj_rel_closed injection_abs inter_abs
irreflexive_abs is_eclose_n_abs is_funspace_abs
iterates_closed length_closed lepoll_rel_refl
limit_ordinal_abs linear_rel_abs
mem_bij_abs mem_eclose_abs mem_inj_abs membership_abs
minimum_closed nat_case_abs nat_case_closed nonempty not_abs
not_closed number1_abs number2_abs number3_abs omega_abs
or_abs or_closed order_isomorphism_abs ordermap_closed
ordertype_closed ordinal_abs pair_abs pair_in_M_iff powerset_abs
pred_closed pred_set_abs quasilist_abs quasinat_abs radd_closed
rall_abs range_abs range_closed relation_abs restrict_closed
restriction_abs rex_abs rmult_closed rtrancl_abs rtrancl_closed
rvimage_closed separation_closed setdiff_abs singleton_abs
singleton_in_M_iff snd_closed strong_replacement_closed subset_abs
succ_in_M_iff successor_abs successor_ordinal_abs sum_abs sum_closed
surj_rel_closed surjection_abs tl_abs trancl_abs trancl_closed
transitive_rel_abs transitive_set_abs typed_function_abs union_abs
upair_abs upair_in_M_iff vimage_abs vimage_closed well_ord_abs
nth_closed Aleph_rel_closed csucc_rel_closed
Card_rel_Aleph_rel
declare sharp_simps[simp del, simplified setclass_iff, simp]
lemmas sharp_intros = nat_into_M Aleph_rel_closed Card_rel_Aleph_rel
declare sharp_intros[rule del, simplified setclass_iff, intro]
end
context G_generic3_AC begin
context
includes G_generic1_lemmas
begin
lemmas mg_sharp_simps = ext.Card_rel_Union ext.Card_rel_cardinal_rel
ext.Collect_abs ext.Cons_abs ext.Cons_in_M_iff ext.Diff_closed
ext.Equal_abs ext.Equal_in_M_iff ext.Finite_abs ext.Forall_abs
ext.Forall_in_M_iff ext.Inl_abs ext.Inl_in_M_iff ext.Inr_abs
ext.Inr_in_M_iff ext.Int_closed ext.Inter_abs ext.Inter_closed
ext.M_nat ext.Member_abs ext.Member_in_M_iff ext.Memrel_closed
ext.Nand_abs ext.Nand_in_M_iff ext.Nil_abs ext.Nil_in_M
ext.Ord_cardinal_rel ext.Pow_rel_closed ext.Un_closed
ext.Union_abs ext.Union_closed ext.and_abs ext.and_closed
ext.apply_abs ext.apply_closed ext.bij_rel_closed
ext.bijection_abs ext.bool_of_o_abs ext.bool_of_o_closed
ext.cadd_rel_0 ext.cadd_rel_closed ext.cardinal_rel_0_iff_0
ext.cardinal_rel_closed ext.cardinal_rel_idem ext.cartprod_abs
ext.cartprod_closed ext.cmult_rel_0 ext.cmult_rel_1
ext.cmult_rel_closed ext.comp_closed ext.composition_abs
ext.cons_abs ext.cons_closed ext.converse_abs ext.converse_closed
ext.csquare_lam_closed ext.csquare_rel_closed ext.depth_closed
ext.domain_abs ext.domain_closed ext.eclose_abs ext.eclose_closed
ext.empty_abs ext.field_abs ext.field_closed
ext.finite_funspace_closed ext.finite_ordinal_abs
ext.fst_closed ext.function_abs ext.function_space_rel_closed
ext.hd_abs ext.image_abs ext.image_closed ext.inj_rel_closed
ext.injection_abs ext.inter_abs ext.irreflexive_abs
ext.is_eclose_n_abs ext.is_funspace_abs
ext.iterates_closed ext.length_closed
ext.lepoll_rel_refl ext.limit_ordinal_abs ext.linear_rel_abs
ext.mem_bij_abs ext.mem_eclose_abs
ext.mem_inj_abs ext.membership_abs
ext.nat_case_abs ext.nat_case_closed
ext.nonempty ext.not_abs ext.not_closed
ext.number1_abs ext.number2_abs ext.number3_abs ext.omega_abs
ext.or_abs ext.or_closed ext.order_isomorphism_abs
ext.ordermap_closed ext.ordertype_closed ext.ordinal_abs
ext.pair_abs ext.pair_in_M_iff ext.powerset_abs ext.pred_closed
ext.pred_set_abs ext.quasilist_abs ext.quasinat_abs
ext.radd_closed ext.rall_abs ext.range_abs ext.range_closed
ext.relation_abs ext.restrict_closed ext.restriction_abs
ext.rex_abs ext.rmult_closed ext.rtrancl_abs ext.rtrancl_closed
ext.rvimage_closed ext.separation_closed ext.setdiff_abs
ext.singleton_abs ext.singleton_in_M_iff ext.snd_closed
ext.strong_replacement_closed ext.subset_abs ext.succ_in_M_iff
ext.successor_abs ext.successor_ordinal_abs ext.sum_abs
ext.sum_closed ext.surj_rel_closed ext.surjection_abs ext.tl_abs
ext.trancl_abs ext.trancl_closed ext.transitive_rel_abs
ext.transitive_set_abs ext.typed_function_abs ext.union_abs
ext.upair_abs ext.upair_in_M_iff ext.vimage_abs ext.vimage_closed
ext.well_ord_abs ext.nth_closed ext.Aleph_rel_closed
ext.csucc_rel_closed ext.Card_rel_Aleph_rel
declare mg_sharp_simps[simp del, simplified setclass_iff, simp]
lemmas mg_sharp_intros = ext.nat_into_M ext.Aleph_rel_closed
ext.Card_rel_Aleph_rel
declare mg_sharp_intros[rule del, simplified setclass_iff, intro]
lemma forces_below_filter:
assumes "M[G], map(val(G),env) ⊨ φ" "p ∈ G"
"arity(φ) ≤ length(env)" "φ ∈ formula" "env ∈ list(M)"
shows "∃q∈G. q ≼ p ∧ q ⊩ φ env"
proof -
note assms
moreover from this
obtain r where "r ⊩ φ env" "r∈G"
using generic truth_lemma[of φ env]
by blast
moreover from this and ‹p∈G›
obtain q where "q ≼ p" "q ≼ r" "q ∈ G" by auto
ultimately
show ?thesis
using strengthening_lemma[of r φ _ env] by blast
qed
subsection‹Preservation by ccc forcing notions›
lemma ccc_fun_closed_lemma_aux:
assumes "f_dot∈M" "p∈M" "a∈M" "b∈M"
shows "{q ∈ ℙ . q ≼ p ∧ (M, [q, ℙ, leq, 𝟭, f_dot, a⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ ))} ∈ M"
using separation_forces[where env="[f_dot, a⇧v, b⇧v]" and φ="⋅0`1 is 2⋅",simplified]
assms G_subset_M[THEN subsetD] generic
separation_in lam_replacement_constant lam_replacement_identity
lam_replacement_product
separation_conj arity_fun_apply_fm union_abs1
by simp_all
lemma ccc_fun_closed_lemma_aux2:
assumes "B∈M" "f_dot∈M" "p∈M" "a∈M"
shows "(##M)(λb∈B. {q ∈ ℙ . q ≼ p ∧ (M, [q, ℙ, leq, 𝟭, f_dot, a⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ ))})"
proof -
have "separation(##M, λz. M, [snd(z), ℙ, leq, 𝟭, f_dot, τ, fst(z)⇧v] ⊨ forces(⋅0`1 is 2⋅ ))"
if "τ∈M" for τ
proof -
let ?f_fm="snd_fm(1,0)"
let ?g_fm="hcomp_fm(check_fm(6),fst_fm,2,0)"
note assms
moreover
have "arity(forces(⋅0`1 is 2⋅ )) ≤ 7"
using arity_fun_apply_fm union_abs1 arity_forces[of "⋅0`1 is 2⋅ "]
by simp
moreover
have "?f_fm ∈ formula" "arity(?f_fm) ≤ 7" "?g_fm ∈ formula" "arity(?g_fm) ≤ 8"
using ord_simp_union
unfolding hcomp_fm_def
by (simp_all add:arity)
ultimately
show ?thesis
using separation_sat_after_function assms that sats_fst_fm
snd_abs sats_snd_fm sats_check_fm check_abs fst_abs
unfolding hcomp_fm_def
by simp
qed
with assms
show ?thesis
using lam_replacement_imp_lam_closed separation_conj separation_in
lam_replacement_product lam_replacement_constant transitivity[of _ B]
lam_replacement_snd lam_replacement_Collect' ccc_fun_closed_lemma_aux
by simp
qed
lemma ccc_fun_closed_lemma:
assumes "A∈M" "B∈M" "f_dot∈M" "p∈M"
shows "(λa∈A. {b∈B. ∃q∈ℙ. q ≼ p ∧ (q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v])}) ∈ M"
proof -
have "separation(##M, λz. M, [snd(z), ℙ, leq, 𝟭, f_dot, fst(fst(z))⇧v, snd(fst(z))⇧v] ⊨ forces(⋅0`1 is 2⋅ ))"
proof -
let ?f_fm="snd_fm(1,0)"
let ?g="λz . fst(fst(fst(z)))⇧v"
let ?g_fm="hcomp_fm(check_fm(6),hcomp_fm(fst_fm,fst_fm),2,0)"
let ?h_fm="hcomp_fm(check_fm(7),hcomp_fm(snd_fm,fst_fm),3,0)"
note assms
moreover
have "arity(forces(⋅0`1 is 2⋅ )) ≤ 7"
using arity_fun_apply_fm union_abs1 arity_forces[of "⋅0`1 is 2⋅ "]
by simp
moreover
have "?f_fm ∈ formula" "arity(?f_fm) ≤ 6" "?g_fm ∈ formula" "arity(?g_fm) ≤ 7"
"?h_fm ∈ formula" "arity(?h_fm) ≤ 8"
using ord_simp_union
unfolding hcomp_fm_def
by (simp_all add:arity)
ultimately
show ?thesis
using separation_sat_after_function3 assms sats_check_fm check_abs
fst_abs snd_abs
unfolding hcomp_fm_def
by simp
qed
moreover
have 1:"separation(##M, λz. M, [snd(z), ℙ, leq, 𝟭, f_dot, τ, fst(z)⇧v] ⊨ forces(⋅0`1 is 2⋅ ))"
if "τ∈M" for τ
proof -
let ?f_fm="snd_fm(1,0)"
let ?g_fm="hcomp_fm(check_fm(6),fst_fm,2,0)"
note assms
moreover
have "arity(forces(⋅0`1 is 2⋅ )) ≤ 7"
using arity_forces[of "⋅0`1 is 2⋅ "] arity_fun_apply_fm union_abs1
by simp
moreover
have "?f_fm ∈ formula" "arity(?f_fm) ≤ 7" "?g_fm ∈ formula" "arity(?g_fm) ≤ 8"
using ord_simp_union
unfolding hcomp_fm_def
by (simp_all add:arity)
ultimately
show ?thesis
using separation_sat_after_function that fst_abs snd_abs sats_check_fm check_abs
unfolding hcomp_fm_def
by simp
qed
moreover note assms
ultimately
show ?thesis
using lam_replacement_imp_lam_closed lam_replacement_Collect' transitivity[of _ A]
lam_replacement_constant lam_replacement_identity lam_replacement_snd
lam_replacement_product separation_conj separation_in separation_bex separation_iff'
by simp
qed
lemma ccc_fun_approximation_lemma:
notes le_trans[trans]
assumes "ccc⇗M⇖(ℙ,leq)" "A∈M" "B∈M" "f∈M[G]" "f : A → B"
shows
"∃F∈M. F : A → Pow⇗M⇖(B) ∧ (∀a∈A. f`a ∈ F`a ∧ |F`a|⇗M⇖ ≤ ω)"
proof -
from ‹f∈M[G]›
obtain f_dot where "f = val(G,f_dot)" "f_dot∈M" using GenExtD by force
with assms
obtain p where "p ⊩ ⋅0:1→2⋅ [f_dot, A⇧v, B⇧v]" "p∈G" "p∈M"
using G_subset_M truth_lemma[of "⋅0:1→2⋅" "[f_dot, A⇧v, B⇧v]"]
by (auto simp add:ord_simp_union arity_typed_function_fm
typed_function_type)
define F where "F≡λa∈A. {b∈B. ∃q∈ℙ. q ≼ p ∧ (q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v])}"
from assms ‹f_dot∈_› ‹p∈M›
have "F ∈ M"
unfolding F_def using ccc_fun_closed_lemma by simp
moreover from calculation
have "f`a ∈ F`a" if "a ∈ A" for a
proof -
note ‹f: A → B› ‹a ∈ A›
moreover from this
have "f ` a ∈ B" by simp
moreover
note ‹f∈M[G]› ‹A∈M›
moreover from calculation
have "M[G], [f, a, f`a] ⊨ ⋅0`1 is 2⋅"
by (auto dest:transitivity)
moreover
note ‹B∈M› ‹f = val(G,f_dot)›
moreover from calculation
have "a∈M" "val(G, f_dot)`a∈M"
by (auto dest:transitivity)
moreover
note ‹f_dot∈M› ‹p∈G›
ultimately
obtain q where "q ≼ p" "q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, (f`a)⇧v]" "q∈G"
using forces_below_filter[of "⋅0`1 is 2⋅" "[f_dot, a⇧v, (f`a)⇧v]" p]
by (auto simp add: ord_simp_union arity_fun_apply_fm
fun_apply_type)
with ‹f`a ∈ B›
have "f`a ∈ {b∈B . ∃q∈ℙ. q ≼ p ∧ q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v]}"
by blast
with ‹a∈A›
show ?thesis unfolding F_def by simp
qed
moreover
have "|F`a|⇗M⇖ ≤ ω ∧ F`a∈M" if "a ∈ A" for a
proof -
let ?Q="λb. {q∈ℙ. q ≼ p ∧ (q ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v])}"
from ‹F ∈ M› ‹a∈A› ‹A∈M›
have "F`a ∈ M" "a∈M"
using transitivity[OF _ ‹A∈M›] by simp_all
moreover
have 2:"⋀x. x∈F`a ⟹ x∈M"
using transitivity[OF _ ‹F`a∈M›] by simp
moreover
have 3:"⋀x. x∈F`a ⟹ (##M)(?Q(x))"
using ccc_fun_closed_lemma_aux[OF ‹f_dot∈M› ‹p∈M› ‹a∈M› 2] transitivity[of _ "F`a"]
by simp
moreover
have 4:"lam_replacement(##M,λb. {q ∈ ℙ . q ≼ p ∧ (M, [q, ℙ, leq, 𝟭, f_dot, a⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ ))})"
using ccc_fun_closed_lemma_aux2[OF _ ‹f_dot∈M› ‹p∈M› ‹a∈M›]
lam_replacement_iff_lam_closed[THEN iffD2]
ccc_fun_closed_lemma_aux[OF ‹f_dot∈M› ‹p∈M› ‹a∈M›]
by simp
ultimately
interpret M_Pi_assumptions_choice "##M" "F`a" ?Q
using Pi_replacement1[OF _ 3] lam_replacement_Sigfun[OF 4]
lam_replacement_imp_strong_replacement
ccc_fun_closed_lemma_aux[OF ‹f_dot∈M› ‹p∈M› ‹a∈M›]
lam_replacement_hcomp2[OF lam_replacement_constant 4 _ _
lam_replacement_minimum,unfolded lam_replacement_def]
by unfold_locales simp_all
from ‹F`a ∈ M›
interpret M_Pi_assumptions2 "##M" "F`a" ?Q "λ_ . ℙ"
using lam_replacement_imp_strong_replacement[OF
lam_replacement_Sigfun[OF lam_replacement_constant]]
Pi_replacement1 transitivity[of _ "F`a"]
by unfold_locales simp_all
from ‹p ⊩ ⋅0:1→2⋅ [f_dot, A⇧v, B⇧v]› ‹a∈A›
have "∃y. y ∈ ?Q(b)" if "b ∈ F`a" for b
using that unfolding F_def by auto
then
obtain q where "q ∈ Pi⇗M⇖(F`a,?Q)" "q∈M" using AC_Pi_rel by auto
moreover
note ‹F`a ∈ M›
moreover from calculation
have "q : F`a →⇗M⇖ ℙ"
using Pi_rel_weaken_type def_function_space_rel by auto
moreover from calculation
have "q : F`a → range(q)" "q : F`a → ℙ" "q : F`a →⇗M⇖ range(q)"
using mem_function_space_rel_abs range_of_fun by simp_all
moreover
have "q`b ⊥ q`c" if "b ∈ F`a" "c ∈ F`a" "b ≠ c"
for b c
proof -
from ‹b ∈ F`a› ‹c ∈ F`a› ‹q ∈ Pi⇗M⇖(F`a,?Q)› ‹q∈M›
have "q`b ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v]"
"q`c ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, c⇧v]"
using mem_Pi_rel_abs[of q] apply_type[of _ _ ?Q]
by simp_all
with ‹b ≠ c› ‹q : F`a → ℙ› ‹a∈A› ‹b∈_› ‹c∈_›
‹A∈M› ‹f_dot∈M› ‹F`a∈M›
show ?thesis
using forces_neq_apply_imp_incompatible
transitivity[of _ A] transitivity[of _ "F`a"]
by auto
qed
moreover from calculation
have "antichain(ℙ,leq,range(q))"
using Pi_range_eq[of _ _ "λ_ . ℙ"]
unfolding antichain_def compat_in_def by auto
moreover from this and ‹q∈M›
have "antichain⇗M⇖(ℙ,leq,range(q))"
by (simp add:absolut del:P_in_M)
moreover from calculation
have "q`b ≠ q`c" if "b ≠ c" "b ∈ F`a" "c ∈ F`a" for b c
using that Incompatible_imp_not_eq apply_type
mem_function_space_rel_abs by simp
ultimately
have "q ∈ inj⇗M⇖(F`a,range(q))"
using def_inj_rel by auto
with ‹F`a ∈ M› ‹q∈M›
have "|F`a|⇗M⇖ ≤ |range(q)|⇗M⇖"
using def_lepoll_rel
by (rule_tac lepoll_rel_imp_cardinal_rel_le) auto
also from ‹antichain⇗M⇖(ℙ,leq,range(q))› ‹ccc⇗M⇖(ℙ,leq)› ‹q∈M›
have "|range(q)|⇗M⇖ ≤ ω"
using def_ccc_rel by simp
finally
show ?thesis using ‹F`a∈M› by auto
qed
moreover from this
have "F`a∈M" if "a∈A" for a
using that by simp
moreover from this ‹B∈M›
have "F : A → Pow⇗M⇖(B)"
using Pow_rel_char
unfolding F_def by (rule_tac lam_type) auto
ultimately
show ?thesis by auto
qed
end
end
end