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. first(b,B,r)" lemma minimum_in: "⟦ well_ord(A,r); B⊆A; B≠0 ⟧ ⟹ minimum(r,B) ∈ B" using the_first_in unfolding minimum_def by simp 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 "minimum(r, {a ∈ A . h ` a = b}) ∈ {a∈A. h`a=b}" if "b∈B" for b proof - from ‹h ∈ surj(A,B)› that have "{a∈A. h`a=b} ≠ 0" unfolding surj_def by blast with ‹well_ord(A,r)› show "minimum(r,{a∈A. h`a=b}) ∈ {a∈A. h`a=b}" using minimum_in 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 that 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})" unfolding minimum_def 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(ω,M[G])" proof - let ?f="λn∈ω. val(P,G,enum`n)" have "x ∈ ω ⟹ val(P,G, enum ` x)∈ M[G]" for x using GenExtD[THEN iffD2, of _ G] bij_is_fun[OF M_countable] by force then have "?f: ω → M[G]" using lam_type[of ω "λn. val(P,G,enum`n)" "λ_.M[G]"] by simp moreover have "∃n∈ω. ?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] ≈ ω" 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(ω,M[G])" using surj_nat_MG by blast then have "M[G] ≲ ω" using well_ord_surj_imp_lepoll well_ord_Memrel[of ω] by simp moreover have "ω ≲ 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 ≈ ω" "Transset(M)" "M ⊨ ZF" shows "∃N. M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ N ⊨ ZF ∧ M≠N ∧ (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N)) ∧ (M, []⊨ AC ⟶ N ⊨ ZFC)" proof - from ‹M ⊨ ZF› interpret M_ZF M using M_ZF_iff_M_satT by simp from ‹Transset(M)› interpret M_ZF_trans M using M_ZF_iff_M_satT by unfold_locales from ‹M ≈ ω› obtain enum where "enum ∈ bij(ω,M)" using eqpoll_sym unfolding eqpoll_def by blast then interpret M_ctm M enum by unfold_locales interpret forcing_data "2⇗<ω⇖" seqle 0 M enum using nat_into_M seqspace_closed seqle_in_M by unfold_locales simp obtain G where "M_generic(G)" "M ≠ M⇗2⇗<ω⇖⇖[G]" (is "M≠?N") using cohen_extension_is_proper 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