Quelle  Forcing_Main.thy

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›
(*
\<comment> \<open>Useful missing lemma\<close>
lemma surj_imp_well_ord:
  assumes "well_ord(A,r)" "h \<in> surj(A,B)"
  shows "\<exists>s. well_ord(B,r)" 
*)

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)+ ― ‹why the heck auto-tools don't solve this?›
  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