Theory Kappa_Closed_Notions
section‹Preservation results for $\kappa$-closed forcing notions›
theory Kappa_Closed_Notions
imports
Not_CH
begin
definition
lerel :: "i⇒i" where
"lerel(α) ≡ Memrel(α) ∪ id(α)"
lemma lerelI[intro!]: "x≤y ⟹ y∈α ⟹ Ord(α) ⟹ ⟨x,y⟩ ∈ lerel(α)"
using Ord_trans[of x y α] ltD unfolding lerel_def by auto
lemma lerelD[dest]: "⟨x,y⟩ ∈ lerel(α) ⟹ Ord(α) ⟹ x≤y"
using ltI[THEN leI] Ord_in_Ord unfolding lerel_def by auto
definition
mono_seqspace :: "[i,i,i] ⇒ i" (‹_ ⇩<→ '(_,_')› [61] 60) where
"α ⇩<→ (P,leq) ≡ mono_map(α,Memrel(α),P,leq)"
relativize functional "mono_seqspace" "mono_seqspace_rel"
relationalize "mono_seqspace_rel" "is_mono_seqspace"
synthesize "is_mono_seqspace" from_definition assuming "nonempty"
context M_ZF_library
begin
rel_closed for "mono_seqspace"
unfolding mono_seqspace_rel_def mono_map_rel_def
using separation_closed separation_ball separation_imp separation_in
lam_replacement_fst lam_replacement_snd lam_replacement_hcomp lam_replacement_constant
lam_replacement_product
lam_replacement_apply2[THEN[5] lam_replacement_hcomp2]
by simp_all
end
abbreviation
mono_seqspace_r (‹_ ⇩<→⇗_⇖ '(_,_')› [61] 60) where
"α ⇩<→⇗M⇖ (P,leq) ≡ mono_seqspace_rel(M,α,P,leq)"
abbreviation
mono_seqspace_r_set (‹_ ⇩<→⇗_⇖ '(_,_')› [61] 60) where
"α ⇩<→⇗M⇖ (P,leq) ≡ mono_seqspace_rel(##M,α,P,leq)"
lemma mono_seqspaceI[intro!]:
includes mono_map_rules
assumes "f: A→P" "⋀x y. x∈A ⟹ y∈A ⟹ x<y ⟹ ⟨f`x, f`y⟩ ∈ leq" "Ord(A)"
shows "f: A ⇩<→ (P,leq)"
using ltI[OF _ Ord_in_Ord[of A], THEN [3] assms(2)] assms(1,3)
unfolding mono_seqspace_def by auto
lemma (in M_ZF_library) mono_seqspace_rel_char:
assumes "M(A)" "M(P)" "M(leq)"
shows "A ⇩<→⇗M⇖ (P,leq) = {f∈A ⇩<→ (P,leq). M(f)}"
using assms mono_map_rel_char
unfolding mono_seqspace_def mono_seqspace_rel_def by simp
lemma (in M_ZF_library) mono_seqspace_relI[intro!]:
assumes "f: A→⇗M⇖ P" "⋀x y. x∈A ⟹ y∈A ⟹ x<y ⟹ ⟨f`x, f`y⟩ ∈ leq"
"Ord(A)" "M(A)" "M(P)" "M(leq)"
shows "f: A ⇩<→⇗M⇖ (P,leq)"
using mono_seqspace_rel_char function_space_rel_char assms by auto
lemma mono_seqspace_is_fun[dest]:
includes mono_map_rules
shows "j: A ⇩<→ (P,leq) ⟹ j: A→ P"
unfolding mono_seqspace_def by auto
lemma mono_map_lt_le_is_mono[dest]:
includes mono_map_rules
assumes "j: A ⇩<→ (P,leq)" "a∈A" "c∈A" "a≤c" "Ord(A)" "refl(P,leq)"
shows "⟨j`a,j`c⟩ ∈ leq"
using assms mono_map_increasing unfolding mono_seqspace_def refl_def
by (cases "a=c") (auto dest:ltD)
lemma (in M_ZF_library) mem_mono_seqspace_abs[absolut]:
assumes "M(f)" "M(A)" "M(P)" "M(leq)"
shows "f:A ⇩<→⇗M⇖ (P,leq) ⟷ f: A ⇩<→ (P,leq)"
using assms mono_map_rel_char unfolding mono_seqspace_def mono_seqspace_rel_def
by (simp)
definition
mono_map_lt_le :: "[i,i] ⇒ i" (infixr ‹⇩<→⇩≤› 60) where
"α ⇩<→⇩≤ β ≡ α ⇩<→ (β,lerel(β))"
lemma mono_map_lt_leI[intro!]:
includes mono_map_rules
assumes "f: A→B" "⋀x y. x∈A ⟹ y∈A ⟹ x<y ⟹ f`x ≤ f`y" "Ord(A)" "Ord(B)"
shows "f: A ⇩<→⇩≤ B"
using assms
unfolding mono_map_lt_le_def by auto
definition
kappa_closed :: "[i,i,i] ⇒ o" (‹_-closed'(_,_')›) where
"κ-closed(P,leq) ≡ ∀δ. δ<κ ⟶ (∀f∈δ ⇩<→ (P,converse(leq)). ∃q∈P. ∀α∈δ. ⟨q,f`α⟩∈leq)"
relativize functional "kappa_closed" "kappa_closed_rel"
relationalize "kappa_closed_rel" "is_kappa_closed"
synthesize "is_kappa_closed" from_definition assuming "nonempty"
abbreviation
kappa_closed_r (‹_-closed⇗_⇖'(_,_')› [61] 60) where
"κ-closed⇗M⇖(P,leq) ≡ kappa_closed_rel(M,κ,P,leq)"
abbreviation
kappa_closed_r_set (‹_-closed⇗_⇖'(_,_')› [61] 60) where
"κ-closed⇗M⇖(P,leq) ≡ kappa_closed_rel(##M,κ,P,leq)"
lemma (in forcing_data3) forcing_a_value:
assumes "p ⊩ ⋅0:1→2⋅ [f_dot, A⇧v, B⇧v]" "a ∈ A"
"q ≼ p" "q ∈ ℙ" "p∈ℙ" "f_dot ∈ M" "A∈M" "B∈M"
shows "∃d∈ℙ. ∃b∈B. d ≼ q ∧ d ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, b⇧v]"
proof -
from assms
have "q ⊩ ⋅0:1→2⋅ [f_dot, A⇧v, B⇧v]"
using strengthening_lemma[of p "⋅0:1→2⋅" q "[f_dot, A⇧v, B⇧v]"]
typed_function_type arity_typed_function_fm
by (auto simp: union_abs2 union_abs1)
from ‹a∈A› ‹A∈M›
have "a∈M" by (auto dest:transitivity)
from ‹q∈ℙ›
text‹Here we're using countability (via the existence of generic filters)
of \<^term>‹M› as a shortcut, to avoid a further density argument.›
obtain G where "M_generic(G)" "q∈G"
using generic_filter_existence by blast
then
interpret G_generic3_AC _ _ _ _ _ G by unfold_locales
include G_generic1_lemmas
note ‹q∈G›
moreover
note ‹q ⊩ ⋅0:1→2⋅ [f_dot, A⇧v, B⇧v]› ‹M_generic(G)›
moreover
note ‹q∈ℙ› ‹f_dot∈M› ‹B∈M› ‹A∈M›
moreover from this
have "map(val( G), [f_dot, A⇧v, B⇧v]) ∈ list(M[G])" by simp
moreover from calculation
have "val(G,f_dot) : A →⇗M[G]⇖ B"
using truth_lemma[of "⋅0:1→2⋅" "[f_dot, A⇧v, B⇧v]", THEN iffD1]
typed_function_type arity_typed_function_fm val_check[OF one_in_G one_in_P]
by (auto simp: union_abs2 union_abs1 ext.mem_function_space_rel_abs)
moreover
note ‹a ∈ M›
moreover from calculation and ‹a∈A›
have "val(G,f_dot) ` a ∈ B" (is "?b ∈ B")
by (simp add: ext.mem_function_space_rel_abs)
moreover from calculation
have "?b ∈ M" by (auto dest:transitivity)
moreover from calculation
have "M[G], map(val(G), [f_dot, a⇧v, ?b⇧v]) ⊨ ⋅0`1 is 2⋅"
by simp
ultimately
obtain r where "r ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, ?b⇧v]" "r∈G" "r∈ℙ"
using truth_lemma[of "⋅0`1 is 2⋅" "[f_dot, a⇧v, ?b⇧v]", THEN iffD2]
fun_apply_type arity_fun_apply_fm val_check[OF one_in_G one_in_P]
G_subset_P
by (auto simp: union_abs2 union_abs1 ext.mem_function_space_rel_abs)
moreover from this and ‹q∈G›
obtain d where "d≼q" "d≼r" "d∈ℙ" by force
moreover
note ‹f_dot∈M› ‹a∈M› ‹?b∈B› ‹B∈M›
moreover from calculation
have "d ≼ q ∧ d ⊩ ⋅0`1 is 2⋅ [f_dot, a⇧v, ?b⇧v]"
using fun_apply_type arity_fun_apply_fm
strengthening_lemma[of r "⋅0`1 is 2⋅" d "[f_dot, a⇧v, ?b⇧v]"]
by (auto dest:transitivity simp add: union_abs2 union_abs1)
ultimately
show ?thesis by auto
qed
locale M_master_CH = M_master + M_library_DC
sublocale M_ZFC2_ground_CH_trans ⊆ M_master_CH "##M"
using replacement_dcwit_repl_body
by unfold_locales (simp_all add:sep_instances del:setclass_iff
add: transrec_replacement_def wfrec_replacement_def dcwit_repl_body_def)
context G_generic3_AC_CH begin
context
includes G_generic1_lemmas
begin
lemma separation_check_snd_aux:
assumes "f_dot∈M" "τ∈M" "χ∈formula" "arity(χ) ≤ 7"
shows "separation(##M, λr. M, [fst(r), ℙ, leq, 𝟭, f_dot, τ, snd(r)⇧v] ⊨ χ)"
proof -
let ?f_fm="fst_fm(1,0)"
let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
note assms
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
using fst_abs snd_abs sats_snd_fm sats_check_fm check_abs
unfolding hcomp_fm_def
by simp
qed
lemma separation_check_fst_snd_aux :
assumes "f_dot∈M" "r∈M" "χ∈formula" "arity(χ) ≤ 7"
shows "separation(##M, λp. M, [r, ℙ, leq, 𝟭, f_dot, fst(p)⇧v, snd(p)⇧v] ⊨ χ)"
proof -
let ?ρ="λz. [r, ℙ, leq, 𝟭, f_dot, fst(z)⇧v, snd(z)⇧v]"
let ?ρ'="λz. [fst(z)⇧v, ℙ, leq, 𝟭, f_dot, r, snd(z)⇧v]"
let ?φ=" (⋅∃(⋅∃(⋅∃(⋅∃(⋅∃(⋅∃⋅⋅0 = 11⋅ ∧ ⋅⋅1 = 7⋅ ∧ ⋅⋅2 = 8⋅ ∧ ⋅⋅3 = 9⋅ ∧ ⋅⋅4 = 10⋅ ∧ ⋅⋅5 = 6⋅ ∧
(λp. incr_bv(p)`6)^6 (χ) ⋅⋅⋅⋅⋅⋅⋅)⋅)⋅)⋅)⋅)⋅)"
let ?f_fm="hcomp_fm(check_fm(5),fst_fm,1,0)"
let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
note assms
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)
moreover from assms
have fm:"?φ∈formula" by simp
moreover from ‹χ ∈ formula› ‹arity(χ) ≤ 7›
have "arity(χ) = 0 ∨ arity(χ) = 1 ∨ arity(χ) = 2 ∨ arity(χ) = 3
∨ arity(χ) = 4 ∨ arity(χ) = 5 ∨ arity(χ) = 6 ∨ arity(χ) = 7"
unfolding lt_def by auto
with calculation and ‹χ ∈ formula›
have ar:"arity(?φ) ≤ 7"
using arity_incr_bv_lemma by safe (simp_all add: arity ord_simp_union)
moreover from calculation
have sep:"separation(##M,λz. M,?ρ'(z)⊨?φ)"
using separation_sat_after_function sats_check_fm check_abs
fst_abs snd_abs
unfolding hcomp_fm_def
by simp
moreover from assms
have "?ρ(z) ∈ list(M)" if "(##M)(z)" for z
using that by simp
moreover from calculation and ‹r ∈ M› ‹χ ∈ formula›
have "(M,?ρ(z) ⊨ χ) ⟷ (M,?ρ'(z)⊨?φ)" if "(##M)(z)" for z
using that sats_incr_bv_iff[of _ _ M _ "[_,_,_,_,_,_]"]
by simp
ultimately
show ?thesis
using separation_cong[THEN iffD1,OF _ sep]
by simp
qed
lemma separation_leq_and_forces_apply_aux:
assumes "f_dot∈M" "B∈M"
shows "∀n∈M. separation(##M, λx. snd(x) ≼ fst(x) ∧
(∃b∈B. M, [snd(x), ℙ, leq, 𝟭, f_dot, (⋃(n))⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ )))"
proof -
have pred_nat_closed: "pred(n)∈M" if "n∈M" for n
using nat_case_closed that
unfolding pred_def
by auto
have "separation(##M, λz. M, [snd(fst(z)), ℙ, leq, 𝟭, f_dot, τ, snd(z)⇧v] ⊨ χ)"
if "χ∈formula" "arity(χ) ≤ 7" "τ∈M" for χ τ
proof -
let ?f_fm="hcomp_fm(snd_fm,fst_fm,1,0)"
let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
note assms
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 sats_check_fm check_abs fst_abs snd_abs that
unfolding hcomp_fm_def
by simp
qed
with assms
show ?thesis
using separation_in lam_replacement_constant lam_replacement_snd lam_replacement_fst
lam_replacement_product pred_nat_closed
arity_forces[of " ⋅0`1 is 2⋅"] arity_fun_apply_fm[of 0 1 2] ord_simp_union
by(clarify,rule_tac separation_conj,simp_all,rule_tac separation_bex,simp_all)
qed
lemma separation_leq_and_forces_apply_aux':
assumes "f_dot∈M" "p∈M" "B∈M"
shows "separation
(##M, λp . snd(snd(p)) ≼ fst(snd(p)) ∧
(∃b∈B. M, [snd(snd(p)), ℙ, leq, 𝟭, f_dot, (⋃fst(p))⇧v, b⇧v] ⊨ forces(⋅0`1 is 2⋅ )))"
proof -
have "separation(##M, λz. M, [snd(snd(fst(z))), ℙ, leq, 𝟭, f_dot, (⋃fst(fst(z)))⇧v, snd(z)⇧v] ⊨ χ)"
if "χ∈formula" "arity(χ) ≤ 7" for χ
proof -
let ?f_fm="hcomp_fm(snd_fm,hcomp_fm(snd_fm,fst_fm),1,0)"
let ?g="λz . (⋃(fst(fst(z))))⇧v"
let ?g_fm="hcomp_fm(check_fm(6),hcomp_fm(big_union_fm,hcomp_fm(fst_fm,fst_fm)),2,0)"
let ?h_fm="hcomp_fm(check_fm(7),snd_fm,3,0)"
note assms
moreover
have f_fm_facts:"?f_fm ∈ formula" "arity(?f_fm) ≤ 6"
using ord_simp_union
unfolding hcomp_fm_def
by (simp_all add:arity)
moreover from assms
have "?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[OF _ _ _ f_fm_facts] check_abs
sats_check_fm that fst_abs snd_abs sats_fst_fm sats_snd_fm
unfolding hcomp_fm_def
by simp
qed
with assms
show ?thesis
using
separation_conj separation_bex
lam_replacement_constant lam_replacement_hcomp
lam_replacement_fst lam_replacement_snd
arity_forces[of " ⋅0`1 is 2⋅"] arity_fun_apply_fm[of 0 1 2] ord_simp_union
separation_in[OF _ lam_replacement_product]
by simp
qed
lemma separation_closed_leq_and_forces_eq_check_aux :
assumes "A∈M" "r∈G" "τ ∈ M"
shows "(##M)({q∈ℙ. ∃h∈A. q ≼ r ∧ q ⊩ ⋅0 = 1⋅ [τ, h⇧v]})"
proof -
have "separation(##M, λz. M, [fst(z), ℙ, leq, 𝟭, τ, snd(z)⇧v] ⊨ χ)" if
"χ∈formula" "arity(χ) ≤ 6" for χ
proof -
let ?f_fm="fst_fm(1,0)"
let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
note assms
moreover
have "?f_fm ∈ formula" "arity(?f_fm) ≤ 6" "?g_fm ∈ formula" "arity(?g_fm) ≤ 7"
using ord_simp_union
unfolding hcomp_fm_def
by (simp_all add:arity)
ultimately
show ?thesis
using separation_sat_after_function_1 sats_fst_fm that
fst_abs snd_abs sats_snd_fm sats_check_fm check_abs
unfolding hcomp_fm_def
by simp
qed
with assms
show ?thesis
using separation_conj separation_in G_subset_M[THEN subsetD]
lam_replacement_constant lam_replacement_fst lam_replacement_product
arity_forces[of "⋅0 = 1⋅",simplified] ord_simp_union
by(rule_tac separation_closed[OF separation_bex],simp_all)
qed
lemma separation_closed_forces_apply_aux:
assumes "B∈M" "f_dot∈M" "r∈M"
shows "(##M)({⟨n,b⟩ ∈ ω × B. r ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b⇧v]})"
using nat_in_M assms transitivity[OF _ ‹B∈M›] nat_into_M separation_check_fst_snd_aux
arity_forces[of " ⋅0`1 is 2⋅"] arity_fun_apply_fm[of 0 1 2] ord_simp_union
unfolding split_def
by simp_all
lemma kunen_IV_6_9_function_space_rel_eq:
assumes "⋀p τ. p ⊩ ⋅0:1→2⋅ [τ, A⇧v, B⇧v] ⟹ p∈ℙ ⟹ τ ∈ M ⟹
∃q∈ℙ. ∃h∈A →⇗M⇖ B. q ≼ p ∧ q ⊩ ⋅0 = 1⋅ [τ, h⇧v]" "A∈M" "B∈M"
shows
"A →⇗M⇖ B = A →⇗M[G]⇖ B"
proof (intro equalityI; clarsimp simp add:
assms function_space_rel_char ext.function_space_rel_char)
fix f
assume "f ∈ A → B" "f ∈ M[G]"
moreover from this
obtain τ where "val(G,τ) = f" "τ ∈ M"
using GenExtD by force
moreover from calculation and ‹A∈M› ‹B∈M›
obtain r where "r ⊩ ⋅0:1→2⋅ [τ, A⇧v, B⇧v]" "r∈G"
using truth_lemma[of "⋅0:1→2⋅" "[τ, A⇧v, B⇧v]"]
typed_function_type arity_typed_function_fm val_check[OF one_in_G one_in_P]
by (auto simp: union_abs2 union_abs1)
moreover from ‹A∈M› ‹B∈M› ‹r∈G› ‹τ ∈ M›
have "{q∈ℙ. ∃h∈A →⇗M⇖ B. q ≼ r ∧ q ⊩ ⋅0 = 1⋅ [τ, h⇧v]} ∈ M" (is "?D ∈ M")
using separation_closed_leq_and_forces_eq_check_aux by auto
moreover from calculation and assms(2-)
have "dense_below(?D, r)"
using strengthening_lemma[of r "⋅0:1→2⋅" _ "[τ, A⇧v, B⇧v]", THEN assms(1)[of _ τ]]
leq_transD generic_dests(1)[of r]
by (auto simp: union_abs2 union_abs1 typed_function_type arity_typed_function_fm) blast
moreover from calculation
obtain q h where "h∈A →⇗M⇖ B" "q ⊩ ⋅0 = 1⋅ [τ, h⇧v]" "q ≼ r" "q∈ℙ" "q∈G"
using generic_inter_dense_below[of ?D r] by blast
note ‹q ⊩ ⋅0 = 1⋅ [τ, h⇧v]› ‹τ∈M› ‹h∈A →⇗M⇖ B› ‹A∈M› ‹B∈M› ‹q∈G›
moreover from this
have "map(val(G), [τ, h⇧v]) ∈ list(M[G])" "h∈M"
by (auto dest:transitivity)
ultimately
have "h = f"
using truth_lemma[of "⋅0=1⋅" "[τ, h⇧v]"] val_check[OF one_in_G one_in_P]
by (auto simp: ord_simp_union)
with ‹h∈M›
show "f ∈ M" by simp
qed
subsection‹$(\omega+1)$-Closed notions preserve countable sequences›
lemma succ_omega_closed_imp_no_new_nat_sequences:
assumes "succ(ω)-closed⇗M⇖(ℙ,leq)" "f : ω → B" "f∈M[G]" "B∈M"
shows "f∈M"
proof -
text‹The next long block proves that the assumptions of Lemma
@{thm [source] kunen_IV_6_9_function_space_rel_eq} are satisfied.›
{
fix p f_dot
assume "p ⊩ ⋅0:1→2⋅ [f_dot, ω⇧v, B⇧v]" "p∈ℙ" "f_dot∈M"
let ?subp="{q∈ℙ. q ≼ p}"
from ‹p∈ℙ›
have "?subp ∈ M"
using first_section_closed[of ℙ p "converse(leq)"]
by (auto dest:transitivity)
define S where "S ≡ λn∈nat.
{⟨q,r⟩ ∈ ?subp×?subp. r ≼ q ∧ (∃b∈B. r ⊩ ⋅0`1 is 2⋅ [f_dot, (⋃(n))⇧v, b⇧v])}"
(is "S ≡ λn∈nat. ?Y(n)")
define S' where "S' ≡ λn∈nat.
{⟨q,r⟩ ∈ ?subp×?subp. r ≼ q ∧ (∃b∈B. r ⊩ ⋅0`1 is 2⋅ [f_dot, (pred(n))⇧v, b⇧v])}"
moreover
have "S = S'"
unfolding S_def S'_def using pred_nat_eq lam_cong by auto
moreover from ‹B∈M› ‹?subp∈M› ‹f_dot∈M›
have "{r ∈ ?subp. ∃b∈B. r ⊩ ⋅0`1 is 2⋅ [f_dot, (⋃(n))⇧v, b⇧v]} ∈ M" (is "?X(n) ∈ M")
if "n∈ω" for n
using that separation_check_snd_aux nat_into_M ord_simp_union
arity_forces[of " ⋅0`1 is 2⋅"] arity_fun_apply_fm
by(rule_tac separation_closed[OF separation_bex,simplified], simp_all)
moreover
have "?Y(n) = (?subp × ?X(n)) ∩ converse(leq)" for n
by (intro equalityI) auto
moreover
note ‹?subp ∈ M› ‹B∈M› ‹p∈ℙ› ‹f_dot∈M›
moreover from calculation
have "n ∈ ω ⟹ ?Y(n) ∈ M" for n
using nat_into_M by simp
moreover from calculation
have "S ∈ M"
using separation_leq_and_forces_apply_aux separation_leq_and_forces_apply_aux'
transitivity[OF ‹p∈ℙ›]
unfolding S_def split_def
by(rule_tac lam_replacement_Collect'[THEN lam_replacement_imp_lam_closed,simplified], simp_all)
ultimately
have "S' ∈ M"
by simp
from ‹p∈ℙ› ‹f_dot∈M› ‹p ⊩ ⋅0:1→2⋅ [f_dot, ω⇧v, B⇧v]› ‹B∈M›
have exr:"∃r∈ℙ. r ≼ q ∧ (∃b∈B. r ⊩ ⋅0`1 is 2⋅ [f_dot, pred(n)⇧v, b⇧v])"
if "q ≼ p" "q∈ℙ" "n∈ω" for q n
using that forcing_a_value by (auto dest:transitivity)
have "∀q∈?subp. ∀n∈ω. ∃r∈?subp. ⟨q,r⟩ ∈ S'`n"
proof -
{
fix q n
assume "q ∈ ?subp" "n∈ω"
moreover from this
have "q ≼ p" "q ∈ ℙ" "pred(n) = ⋃n"
using pred_nat_eq by simp_all
moreover from calculation and exr
obtain r where MM:"r ≼ q" "∃b∈B. r ⊩ ⋅0`1 is 2⋅ [f_dot, pred(n)⇧v, b⇧v]" "r∈ℙ"
by blast
moreover from calculation ‹q ≼ p› ‹p ∈ ℙ›
have "r ≼ p"
using leq_transD[of r q p] by auto
ultimately
have "∃r∈?subp. r ≼ q ∧ (∃b∈B. r ⊩ ⋅0`1 is 2⋅ [f_dot, (pred(n))⇧v, b⇧v])"
by auto
}
then
show ?thesis
unfolding S'_def by simp
qed
with ‹p∈ℙ› ‹?subp ∈ M› ‹S' ∈ M›
obtain g where "g ∈ ω →⇗M⇖ ?subp" "g`0 = p" "∀n ∈ nat. ⟨g`n,g`succ(n)⟩∈S'`succ(n)"
using sequence_DC[simplified] refl_leq[of p] by blast
moreover from this and ‹?subp ∈ M›
have "g : ω → ℙ" "g ∈ M"
using fun_weaken_type[of g ω ?subp ℙ] function_space_rel_char by auto
ultimately
have "g : ω ⇩<→⇗M⇖ (ℙ,converse(leq))"
using decr_succ_decr[of g] leq_preord
unfolding S'_def by (auto simp:absolut intro:leI)
moreover from ‹succ(ω)-closed⇗M⇖(ℙ,leq)› and this
have "∃q∈M. q ∈ ℙ ∧ (∀α∈M. α ∈ ω ⟶ q ≼ g ` α)"
using transitivity[simplified, of g] mono_seqspace_rel_closed[of ω _ "converse(leq)"]
unfolding kappa_closed_rel_def
by auto
ultimately
obtain r where "r∈ℙ" "r∈M" "∀n∈ω. r ≼ g`n"
using nat_into_M by auto
with ‹g`0 = p›
have "r ≼ p"
by blast
let ?h="{⟨n,b⟩ ∈ ω × B. r ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b⇧v]}"
have "function(?h)"
proof (rule_tac functionI, rule_tac ccontr, auto simp del: app_Cons)
fix n b b'
assume "n ∈ ω" "b ≠ b'" "b ∈ B" "b' ∈ B"
moreover
assume "r ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b⇧v]" "r ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b'⇧v]"
moreover
note ‹r ∈ ℙ›
moreover from this
have "¬ r ⊥ r"
by (auto intro!:refl_leq)
moreover
note ‹f_dot∈M› ‹B∈M›
ultimately
show False
using forces_neq_apply_imp_incompatible[of r f_dot "n⇧v" b r b']
transitivity[of _ B] by (auto dest:transitivity)
qed
moreover
have "range(?h) ⊆ B"
by auto
moreover
have "domain(?h) = ω"
proof -
{
fix n
assume "n ∈ ω"
moreover from this
have 1:"(⋃(n)) = pred(n)"
using pred_nat_eq by simp
moreover from calculation and ‹∀n ∈ nat. ⟨g`n,g`succ(n)⟩∈S'`succ(n)›
obtain b where "g`(succ(n)) ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b⇧v]" "b∈B"
unfolding S'_def by auto
moreover from ‹B∈M› and calculation
have "b ∈ M" "n ∈ M"
by (auto dest:transitivity)
moreover
note ‹g : ω → ℙ› ‹∀n∈ω. r ≼ g`n› ‹r∈ℙ› ‹f_dot∈M›
moreover from calculation
have "r ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b⇧v]"
using fun_apply_type arity_fun_apply_fm
strengthening_lemma[of "g`succ(n)" "⋅0`1 is 2⋅" r "[f_dot, n⇧v, b⇧v]"]
by (simp add: union_abs2 union_abs1)
ultimately
have "∃b∈B. r ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b⇧v]"
by auto
}
then
show ?thesis
by force
qed
moreover
have "relation(?h)"
unfolding relation_def by simp
moreover from ‹f_dot∈M› ‹r∈M› ‹B∈M›
have "?h ∈ M"
using separation_closed_forces_apply_aux by simp
moreover
note ‹B ∈ M›
ultimately
have "?h: ω →⇗M⇖ B"
using function_imp_Pi[THEN fun_weaken_type[of ?h _ "range(?h)" B]]
function_space_rel_char by simp
moreover
note ‹p ⊩ ⋅0:1→2⋅ [f_dot, ω⇧v, B⇧v]› ‹r ≼ p› ‹r∈ℙ› ‹p∈ℙ› ‹f_dot∈M› ‹B∈M›
moreover from this
have "r ⊩ ⋅0:1→2⋅ [f_dot, ω⇧v, B⇧v]"
using strengthening_lemma[of p "⋅0:1→2⋅" r "[f_dot, ω⇧v, B⇧v]"]
typed_function_type arity_typed_function_fm
by (auto simp: union_abs2 union_abs1)
moreover
note ‹?h∈M›
moreover from calculation
have "r ⊩ ⋅0 = 1⋅ [f_dot, ?h⇧v]"
proof (intro definition_of_forcing[THEN iffD2] allI impI,
simp_all add:union_abs2 union_abs1 del:app_Cons)
fix H
let ?f="val(H,f_dot)"
assume "M_generic(H) ∧ r ∈ H"
moreover from this
interpret g:G_generic1 _ _ _ _ _ H
by unfold_locales simp
note ‹r∈ℙ› ‹f_dot∈M› ‹B∈M›
moreover from calculation
have "map(val(H), [f_dot, ω⇧v, B⇧v]) ∈ list(M[H])" "r∈H"
by simp_all
moreover from calculation and ‹r∈H› and ‹r ⊩ ⋅0:1→2⋅ [f_dot, ω⇧v, B⇧v]›
have "?f : ω → B"
using g.truth_lemma[of "⋅0:1→2⋅" "[f_dot, ω⇧v, B⇧v]",THEN iffD1] g.one_in_G one_in_P
typed_function_type arity_typed_function_fm val_check
by (auto simp: union_abs2 union_abs1)
moreover
have "?h`n = ?f`n" if "n ∈ ω" for n
proof -
note ‹n ∈ ω› ‹domain(?h) = ω›
moreover from this
have "n∈domain(?h)"
by simp
moreover from this
obtain b where "r ⊩ ⋅0`1 is 2⋅ [f_dot, n⇧v, b⇧v]" "b∈B"
by force
moreover
note ‹function(?h)›
moreover from calculation
have "b = ?h`n"
using function_apply_equality by simp
moreover
note ‹B ∈ M›
moreover from calculation
have "?h`n ∈ M"
by (auto dest:transitivity)
moreover
note ‹f_dot ∈ M› ‹r ∈ ℙ› ‹M_generic(H) ∧ r ∈ H› ‹map(val(H), [f_dot, ω⇧v, B⇧v]) ∈ list(M[H])›
moreover from calculation
have "[?f, n, ?h`n] ∈ list(M[H])"
using M_subset_MG nat_into_M[of n] g.one_in_G by (auto dest:transitivity)
ultimately
show ?thesis
using definition_of_forcing[of r "⋅0`1 is 2⋅" "[f_dot, n⇧v, b⇧v]",
THEN iffD1, rule_format, of H]
val_check g.one_in_G one_in_P nat_into_M
by (auto dest:transitivity simp add:fun_apply_type
arity_fun_apply_fm union_abs2 union_abs1)
qed
with calculation and ‹B∈M› ‹?h: ω →⇗M⇖ B›
have "?h = ?f"
using function_space_rel_char
by (rule_tac fun_extension[of ?h ω "λ_.B" ?f]) auto
ultimately
show "?f = val(H, ?h⇧v)"
using val_check g.one_in_G one_in_P generic by simp
qed
ultimately
have "∃r∈ℙ. ∃h∈ω →⇗M⇖ B. r ≼ p ∧ r ⊩ ⋅0 = 1⋅ [f_dot, h⇧v]"
by blast
}
moreover
note ‹B ∈ M› assms
moreover from calculation
have "f : ω →⇗M⇖ B"
using kunen_IV_6_9_function_space_rel_eq function_space_rel_char
ext.mem_function_space_rel_abs by auto
ultimately
show ?thesis
by (auto dest:transitivity)
qed
declare mono_seqspace_rel_closed[rule del]
lemma succ_omega_closed_imp_no_new_reals:
assumes "succ(ω)-closed⇗M⇖(ℙ,leq)"
shows "ω →⇗M⇖ 2 = ω →⇗M[G]⇖ 2"
proof -
from assms
have "ω →⇗M[G]⇖ 2 ⊆ ω →⇗M⇖ 2"
using succ_omega_closed_imp_no_new_nat_sequences function_space_rel_char
ext.function_space_rel_char Aleph_rel_succ Aleph_rel_zero
by auto
then
show ?thesis
using function_space_rel_transfer by (intro equalityI) auto
qed
lemma succ_omega_closed_imp_Aleph_1_preserved:
assumes "succ(ω)-closed⇗M⇖(ℙ,leq)"
shows "ℵ⇘1⇙⇗M⇖ = ℵ⇘1⇙⇗M[G]⇖"
proof -
have "ℵ⇘1⇙⇗M[G]⇖ ≤ ℵ⇘1⇙⇗M⇖"
proof (rule ccontr)
assume "¬ ℵ⇘1⇙⇗M[G]⇖ ≤ ℵ⇘1⇙⇗M⇖"
then
have "ℵ⇘1⇙⇗M⇖ < ℵ⇘1⇙⇗M[G]⇖"
using Card_rel_is_Ord ext.Card_rel_is_Ord
not_le_iff_lt[THEN iffD1] by auto
then
have "|ℵ⇘1⇙⇗M⇖|⇗M[G]⇖ ≤ ω"
using ext.Card_rel_lt_csucc_rel_iff ext.Aleph_rel_zero
ext.Aleph_rel_succ ext.Card_rel_nat
by (auto intro!:ext.lt_csucc_rel_iff[THEN iffD1]
intro:Card_rel_Aleph_rel[THEN Card_rel_is_Ord, of 1])
then
obtain f where "f ∈ inj(ℵ⇘1⇙⇗M⇖,ω)" "f ∈ M[G]"
using ext.countable_rel_iff_cardinal_rel_le_nat[of "ℵ⇘1⇙⇗M⇖", THEN iffD2]
unfolding countable_rel_def lepoll_rel_def
by auto
then
obtain g where "g ∈ surj⇗M[G]⇖(ω, ℵ⇘1⇙⇗M⇖)"
using ext.inj_rel_imp_surj_rel[of f _ ω, OF _ zero_lt_Aleph_rel1[THEN ltD]]
by auto
moreover from this
have "g : ω → ℵ⇘1⇙⇗M⇖" "g ∈ M[G]"
using ext.surj_rel_char surj_is_fun by simp_all
moreover
note ‹succ(ω)-closed⇗M⇖(ℙ,leq)›
ultimately
have "g ∈ surj⇗M⇖(ω, ℵ⇘1⇙⇗M⇖)" "g ∈ M"
using succ_omega_closed_imp_no_new_nat_sequences
mem_surj_abs ext.mem_surj_abs by simp_all
then
show False
using surj_rel_implies_cardinal_rel_le[of g ω "ℵ⇘1⇙⇗M⇖"]
Card_rel_nat[THEN Card_rel_cardinal_rel_eq] Card_rel_is_Ord
not_le_iff_lt[THEN iffD2, OF _ _ nat_lt_Aleph_rel1]
by simp
qed
then
show ?thesis
using Aleph_rel_le_Aleph_rel
by (rule_tac le_anti_sym) simp
qed
end
end
end