Theory Forcing_Main

theory Forcing_Main
imports Internal_ZFC_Axioms Choice_Axiom Ordinals_In_MG Succession_Poset
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 ≠ M2[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