Theory Forcing_Main
section‹The main theorem›
theory Forcing_Main
imports
Internal_ZFC_Axioms
Choice_Axiom
Ordinals_In_MG
Succession_Poset
begin
subsection‹The generic extension is countable›
definition
minimum :: "i ⇒ i ⇒ i" where
"minimum(r,B) ≡ THE b. b∈B ∧ (∀y∈B. y ≠ b ⟶ ⟨b, y⟩ ∈ r)"
lemma well_ord_imp_min:
assumes
"well_ord(A,r)" "B ⊆ A" "B ≠ 0"
shows
"minimum(r,B) ∈ B"
proof -
from ‹well_ord(A,r)›
have "wf[A](r)"
using well_ord_is_wf[OF ‹well_ord(A,r)›] by simp
with ‹B⊆A›
have "wf[B](r)"
using Sigma_mono Int_mono wf_subset unfolding wf_on_def by simp
then
have "∀ x. x ∈ B ⟶ (∃z∈B. ∀y. ⟨y, z⟩ ∈ r∩B×B ⟶ y ∉ B)"
unfolding wf_on_def using wf_eq_minimal
by blast
with ‹B≠0›
obtain z where
B: "z∈B ∧ (∀y. ⟨y,z⟩∈r∩B×B ⟶ y∉B)"
by blast
then
have "z∈B ∧ (∀y∈B. y ≠ z ⟶ ⟨z, y⟩ ∈ r)"
proof -
{
fix y
assume "y∈B" "y≠z"
with ‹well_ord(A,r)› B ‹B⊆A›
have "⟨z,y⟩∈r|⟨y,z⟩∈r|y=z"
unfolding well_ord_def tot_ord_def linear_def by auto
with B ‹y∈B› ‹y≠z›
have "⟨z,y⟩∈r"
by (cases;auto)
}
with B
show ?thesis by blast
qed
have "v = z" if "v∈B ∧ (∀y∈B. y ≠ v ⟶ ⟨v, y⟩ ∈ r)" for v
using that B by auto
with ‹z∈B ∧ (∀y∈B. y ≠ z ⟶ ⟨z, y⟩ ∈ r)›
show ?thesis
unfolding minimum_def
using the_equality2[OF ex1I[of "λx .x∈B ∧ (∀y∈B. y ≠ x ⟶ ⟨x, y⟩ ∈ r)" z]]
by auto
qed
lemma well_ord_surj_imp_lepoll:
assumes "well_ord(A,r)" "h ∈ surj(A,B)"
shows "B ≲ A"
proof -
let ?f="λb∈B. minimum(r, {a∈A. h`a=b})"
have "b ∈ B ⟹ minimum(r, {a ∈ A . h ` a = b}) ∈ {a∈A. h`a=b}" for b
proof -
fix b
assume "b∈B"
with ‹h ∈ surj(A,B)›
have "∃a∈A. h`a=b"
unfolding surj_def by blast
then
have "{a∈A. h`a=b} ≠ 0"
by auto
with assms
show "minimum(r,{a∈A. h`a=b}) ∈ {a∈A. h`a=b}"
using well_ord_imp_min by blast
qed
moreover from this
have "?f : B → A"
using lam_type[of B _ "λ_.A"] by simp
moreover
have "?f ` w = ?f ` x ⟹ w = x" if "w∈B" "x∈B" for w x
proof -
from calculation(1)[OF that(1)] calculation(1)[OF that(2)]
have "w = h ` minimum(r, {a ∈ A . h ` a = w})"
"x = h ` minimum(r, {a ∈ A . h ` a = x})"
by simp_all
moreover
assume "?f ` w = ?f ` x"
moreover from this and that
have "minimum(r, {a ∈ A . h ` a = w}) = minimum(r, {a ∈ A . h ` a = x})"
by simp_all
moreover from calculation(1,2,4)
show "w=x" by simp
qed
ultimately
show ?thesis
unfolding lepoll_def inj_def by blast
qed
lemma (in forcing_data) surj_nat_MG :
"∃f. f ∈ surj(nat,M[G])"
proof -
let ?f="λn∈nat. val(G,enum`n)"
have "x ∈ nat ⟹ val(G, enum ` x)∈ M[G]" for x
using GenExtD[THEN iffD2, of _ G] bij_is_fun[OF M_countable] by force
then
have "?f: nat → M[G]"
using lam_type[of nat "λn. val(G,enum`n)" "λ_.M[G]"] by simp
moreover
have "∃n∈nat. ?f`n = x" if "x∈M[G]" for x
using that GenExtD[of _ G] bij_is_surj[OF M_countable]
unfolding surj_def by auto
ultimately
show ?thesis
unfolding surj_def by blast
qed
lemma (in G_generic) MG_eqpoll_nat: "M[G] ≈ nat"
proof -
interpret MG: M_ZF_trans "M[G]"
using Transset_MG generic pairing_in_MG
Union_MG extensionality_in_MG power_in_MG
foundation_in_MG strong_replacement_in_MG[simplified]
separation_in_MG[simplified] infinity_in_MG
by unfold_locales simp_all
obtain f where "f ∈ surj(nat,M[G])"
using surj_nat_MG by blast
then
have "M[G] ≲ nat"
using well_ord_surj_imp_lepoll well_ord_Memrel[of nat]
by simp
moreover
have "nat ≲ M[G]"
using MG.nat_into_M subset_imp_lepoll by auto
ultimately
show ?thesis using eqpollI
by simp
qed
subsection‹The main result›
theorem extensions_of_ctms:
assumes
"M ≈ nat" "Transset(M)" "M ⊨ ZF"
shows
"∃N.
M ⊆ N ∧ N ≈ nat ∧ Transset(N) ∧ N ⊨ ZF ∧ M≠N ∧
(∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N)) ∧
(M, []⊨ AC ⟶ N ⊨ ZFC)"
proof -
from ‹M ≈ nat›
obtain enum where "enum ∈ bij(nat,M)"
using eqpoll_sym unfolding eqpoll_def by blast
with assms
interpret M_ctm M enum
using M_ZF_iff_M_satT
by intro_locales (simp_all add:M_ctm_axioms_def)
interpret ctm_separative "2^<ω" seqle 0 M enum
proof (unfold_locales)
fix f
let ?q="seq_upd(f,0)" and ?r="seq_upd(f,1)"
assume "f ∈ 2^<ω"
then
have "?q ≼s f ∧ ?r ≼s f ∧ ?q ⊥s ?r"
using upd_leI seqspace_separative by auto
moreover from calculation
have "?q ∈ 2^<ω" "?r ∈ 2^<ω"
using seq_upd_type[of f 2] by auto
ultimately
show "∃q∈2^<ω. ∃r∈2^<ω. q ≼s f ∧ r ≼s f ∧ q ⊥s r"
by (rule_tac bexI)+
next
show "2^<ω ∈ M" using nat_into_M seqspace_closed by simp
next
show "seqle ∈ M" using seqle_in_M .
qed
from cohen_extension_is_proper
obtain G where "M_generic(G)"
"M ≠ GenExt(G)" (is "M≠?N")
by blast
then
interpret G_generic "2^<ω" seqle 0 _ enum G by unfold_locales
interpret MG: M_ZF "?N"
using generic pairing_in_MG
Union_MG extensionality_in_MG power_in_MG
foundation_in_MG strong_replacement_in_MG[simplified]
separation_in_MG[simplified] infinity_in_MG
by unfold_locales simp_all
have "?N ⊨ ZF"
using M_ZF_iff_M_satT[of ?N] MG.M_ZF_axioms by simp
moreover
have "M, []⊨ AC ⟹ ?N ⊨ ZFC"
proof -
assume "M, [] ⊨ AC"
then
have "choice_ax(##M)"
unfolding ZF_choice_fm_def using ZF_choice_auto by simp
then
have "choice_ax(##?N)" using choice_in_MG by simp
with ‹?N ⊨ ZF›
show "?N ⊨ ZFC"
using ZF_choice_auto sats_ZFC_iff_sats_ZF_AC
unfolding ZF_choice_fm_def by simp
qed
moreover
note ‹M ≠ ?N›
moreover
have "Transset(?N)" using Transset_MG .
moreover
have "M ⊆ ?N" using M_subset_MG[OF one_in_G] generic by simp
ultimately
show ?thesis
using Ord_MG_iff MG_eqpoll_nat
by (rule_tac x="?N" in exI, simp)
qed
end