Theory Forcing_Main

section‹The main theorem›
theory Forcing_Main
  imports
  Succession_Poset
  ZF_Miscellanea
  Internal_ZFC_Axioms
  Choice_Axiom
  Ordinals_In_MG

begin

subsection‹The generic extension is countable›

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 del:lepollI)
  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