Theory Forcing_Main

section‹The existence of generic extensions›

theory Forcing_Main
  imports
    Ordinals_In_MG
    Choice_Axiom
    Succession_Poset

begin

subsection‹The generic extension is countable›

lemma (in forcing_data1) surj_nat_MG : "∃f. f ∈ surj(ω,M[G])"
proof -
  let ?f="λn∈ω. val(G,enum`n)"
  have "x ∈ ω ⟹ val(G, enum ` x)∈ M[G]" for x
    using GenExtI bij_is_fun[OF M_countable]
    by simp
  then
  have "?f: ω → M[G]"
    using lam_type[of ω "λn. val(G,enum`n)" "λ_.M[G]"] by simp
  moreover
  have "∃n∈ω. ?f`n = x" if "x∈M[G]" for x
    using that GenExt_iff[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_generic1) MG_eqpoll_nat: "M[G] ≈ ω"
proof -
  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 ext.nat_into_M subset_imp_lepoll by (auto del:lepollI)
  ultimately
  show ?thesis
    using eqpollI by simp
qed

subsection‹Extensions of ctms of fragments of $\ZFC$›

context G_generic1
begin

lemma sats_ground_repl_fm_imp_sats_ZF_replacement_fm:
  assumes
    "φ∈formula" "M, [] ⊨ ⋅Replacement(ground_repl_fm(φ))⋅"
  shows
    "M[G], [] ⊨ ⋅Replacement(φ)⋅"
  using assms sats_ZF_replacement_fm_iff
  by (auto simp:replacement_assm_def ground_replacement_assm_def
      intro:strong_replacement_in_MG[simplified])

lemma satT_ground_repl_fm_imp_satT_ZF_replacement_fm:
  assumes
    "Φ ⊆ formula" "M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}"
  shows
    "M[G] ⊨ { ⋅Replacement(φ)⋅ . φ ∈ Φ}"
  using assms sats_ground_repl_fm_imp_sats_ZF_replacement_fm
  by auto

end ― ‹\<^locale>‹G_generic1››

theorem extensions_of_ctms:
  assumes
    "M ≈ ω" "Transset(M)"
    "M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ overhead}"
    "Φ ⊆ formula" "M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}"
  shows
    "∃N.
      M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ M≠N ∧
      (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N)) ∧
      ((M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅) ∧ N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ Φ}"
proof -
  from ‹M ⊨ ⋅Z⋅ ∪ _› ‹Transset(M)›
  interpret M_ZF_ground_trans M
    using M_satT_imp_M_ZF_ground_trans
    by simp
  from ‹M ≈ ω›
  obtain enum where "enum ∈ bij(ω,M)"
    using eqpoll_sym unfolding eqpoll_def by blast
  then
  interpret M_ctm1 M enum by unfold_locales
  interpret forcing_data1 "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[G]"
    using cohen_extension_is_proper
    by blast
  text‹Recall that \<^term>‹M[G]› denotes the generic extension
  of \<^term>‹M› using the poset of sequences \<^term>‹2⇗<ω⇖›.›
  then
  interpret G_generic1 "2⇗<ω⇖" seqle 0 _ enum G by unfold_locales
  interpret MG: M_Z_basic "M[G]"
    using generic pairing_in_MG
      Union_MG  extensionality_in_MG power_in_MG
      foundation_in_MG replacement_assm_MG
      separation_in_MG infinity_in_MG replacement_ax1
    by unfold_locales simp
  have "M, []⊨ ⋅AC⋅ ⟹ M[G], [] ⊨ ⋅AC⋅"
  proof -
    assume "M, [] ⊨ ⋅AC⋅"
    then
    have "choice_ax(##M)"
      unfolding ZF_choice_fm_def using ZF_choice_auto by simp
    then
    have "choice_ax(##M[G])" using choice_in_MG by simp
    then
    show "M[G], [] ⊨ ⋅AC⋅"
      using ZF_choice_auto sats_ZFC_iff_sats_ZF_AC
      unfolding ZF_choice_fm_def by simp
  qed
  moreover
  note ‹M ≠ M[G]› ‹M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}› ‹Φ ⊆ formula›
  moreover
  have "Transset(M[G])" using Transset_MG .
  moreover
  have "M ⊆ M[G]" using M_subset_MG[OF one_in_G] generic by simp
  ultimately
  show ?thesis
    using Ord_MG_iff MG_eqpoll_nat ext.M_satT_Zermelo_fms
      satT_ground_repl_fm_imp_satT_ZF_replacement_fm[of Φ]
    by (rule_tac x="M[G]" in exI, auto)
qed

lemma ZF_replacement_overhead_sub_ZF: "{⋅Replacement(p)⋅ . p ∈ overhead} ⊆ ZF"
  using instances1_fms_type instances_ground_fms_type
  unfolding overhead_def ZF_def ZF_schemes_def by auto

theorem extensions_of_ctms_ZF:
  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 assms
  have "∃N.
      M ⊆ N ∧ N ≈ ω ∧ Transset(N) ∧ M≠N ∧
      (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N)) ∧
      ((M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅) ∧ N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ formula}"
    using extensions_of_ctms[of M formula] satT_ZF_imp_satT_Z[of M]
      satT_mono[OF _ ground_repl_fm_sub_ZF, of M]
      satT_mono[OF _ ZF_replacement_overhead_sub_ZF, of M]
    by (auto simp: satT_Un_iff)
  then
  obtain N where "N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ formula}" "M ⊆ N" "N ≈ ω" "Transset(N)"
    "M ≠ N" "(∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)"
    "(M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅"
    by blast
  moreover from ‹N ⊨ ⋅Z⋅ ∪ { ⋅Replacement(φ)⋅ . φ ∈ formula}›
  have "N ⊨ ZF"
    using satT_Z_ZF_replacement_imp_satT_ZF by auto
  moreover from this and ‹(M, []⊨ ⋅AC⋅) ⟶ N, [] ⊨ ⋅AC⋅›
  have "(M, []⊨ ⋅AC⋅) ⟶ N ⊨ ZFC"
    using sats_ZFC_iff_sats_ZF_AC by simp
  ultimately
  show ?thesis
    by auto
qed

end