section‹The Axiom of Choice in $M[G]$›
theory Choice_Axiom
imports Powerset_Axiom Pairing_Axiom Union_Axiom Extensionality_Axiom
Foundation_Axiom Powerset_Axiom Separation_Axiom
Replacement_Axiom Interface Infinity_Axiom
begin
definition
induced_surj :: "i⇒i⇒i⇒i" where
"induced_surj(f,a,e) == f-``(range(f)-a)×{e} ∪ restrict(f,f-``a)"
lemma domain_induced_surj: "domain(induced_surj(f,a,e)) = domain(f)"
unfolding induced_surj_def using domain_restrict domain_of_prod by auto
lemma range_restrict_vimage:
assumes "function(f)"
shows "range(restrict(f,f-``a)) ⊆ a"
proof
from assms
have "function(restrict(f,f-``a))"
using function_restrictI by simp
fix y
assume "y ∈ range(restrict(f,f-``a))"
then
obtain x where "<x,y> ∈ restrict(f,f-``a)" "x ∈ f-``a" "x∈domain(f)"
using domain_restrict domainI[of _ _ "restrict(f,f-``a)"] by auto
moreover
note ‹function(restrict(f,f-``a))›
ultimately
have "y = restrict(f,f-``a)`x"
using function_apply_equality by blast
also from ‹x ∈ f-``a›
have "restrict(f,f-``a)`x = f`x"
by simp
finally
have "y=f`x" .
moreover from assms ‹x∈domain(f)›
have "<x,f`x> ∈ f"
using function_apply_Pair by auto
moreover
note assms ‹x ∈ f-``a›
ultimately
show "y∈a"
using function_image_vimage[of f a] by auto
qed
lemma induced_surj_type:
assumes
"function(f)"
shows
"induced_surj(f,a,e): domain(f) → {e} ∪ a"
and
"x ∈ f-``a ⟹ induced_surj(f,a,e)`x = f`x"
proof -
let ?f1="f-``(range(f)-a) × {e}" and ?f2="restrict(f, f-``a)"
have "domain(?f2) = domain(f) ∩ f-``a"
using domain_restrict by simp
moreover from assms
have 1: "domain(?f1) = f-``(range(f))-f-``a"
using domain_of_prod function_vimage_Diff by simp
ultimately
have "domain(?f1) ∩ domain(?f2) = 0"
by auto
moreover
have "function(?f1)" "relation(?f1)" "range(?f1) ⊆ {e}"
unfolding function_def relation_def range_def by auto
moreover from this and assms
have "?f1: domain(?f1) → range(?f1)"
using function_imp_Pi by simp
moreover from assms
have "?f2: domain(?f2) → range(?f2)"
using function_imp_Pi[of "restrict(f, f -`` a)"] function_restrictI by simp
moreover from assms
have "range(?f2) ⊆ a"
using range_restrict_vimage by simp
ultimately
have "induced_surj(f,a,e): domain(?f1) ∪ domain(?f2) → {e} ∪ a"
unfolding induced_surj_def using fun_is_function fun_disjoint_Un fun_weaken_type by simp
moreover
have "domain(?f1) ∪ domain(?f2) = domain(f)"
using domain_restrict domain_of_prod by auto
ultimately
show "induced_surj(f,a,e): domain(f) → {e} ∪ a"
by simp
assume "x ∈ f-``a"
then
have "?f2`x = f`x"
using restrict by simp
moreover from ‹x ∈ f-``a› and 1
have "x ∉ domain(?f1)"
by simp
ultimately
show "induced_surj(f,a,e)`x = f`x"
unfolding induced_surj_def using fun_disjoint_apply2[of x ?f1 ?f2] by simp
qed
lemma induced_surj_is_surj :
assumes
"e∈a" "function(f)" "domain(f) = α" "⋀y. y ∈ a ⟹ ∃x∈α. f ` x = y"
shows
"induced_surj(f,a,e) ∈ surj(α,a)"
unfolding surj_def
proof (intro CollectI ballI)
from assms
show "induced_surj(f,a,e): α → a"
using induced_surj_type[of f a e] cons_eq cons_absorb by simp
fix y
assume "y ∈ a"
with assms
have "∃x∈α. f ` x = y"
by simp
then
obtain x where "x∈α" "f ` x = y" by auto
with ‹y∈a› assms
have "x∈f-``a"
using vimage_iff function_apply_Pair[of f x] by auto
with ‹f ` x = y› assms
have "induced_surj(f, a, e) ` x = y"
using induced_surj_type by simp
with ‹x∈α› show
"∃x∈α. induced_surj(f, a, e) ` x = y" by auto
qed
context G_generic
begin
definition
upair_name :: "i ⇒ i ⇒ i" where
"upair_name(τ,ρ) == {⟨τ,one⟩,⟨ρ,one⟩}"
definition
is_upair_name :: "[i,i,i] ⇒ o" where
"is_upair_name(x,y,z) ≡ ∃xo∈M. ∃yo∈M. pair(##M,x,one,xo) ∧ pair(##M,y,one,yo) ∧
upair(##M,xo,yo,z)"
lemma upair_name_abs :
assumes "x∈M" "y∈M" "z∈M"
shows "is_upair_name(x,y,z) ⟷ z = upair_name(x,y)"
unfolding is_upair_name_def upair_name_def using assms one_in_M pair_in_M_iff by simp
lemma upair_name_closed :
"⟦ x∈M; y∈M ⟧ ⟹ upair_name(x,y)∈M"
unfolding upair_name_def using upair_in_M_iff pair_in_M_iff one_in_M by simp
definition
upair_name_fm :: "[i,i,i,i] ⇒ i" where
"upair_name_fm(x,y,o,z) ≡ Exists(Exists(And(pair_fm(x#+2,o#+2,1),
And(pair_fm(y#+2,o#+2,0),upair_fm(1,0,z#+2)))))"
lemma upair_name_fm_type[TC] :
"⟦ s∈nat;x∈nat;y∈nat;o∈nat⟧ ⟹ upair_name_fm(s,x,y,o)∈formula"
unfolding upair_name_fm_def by simp
lemma sats_upair_name_fm :
assumes "x∈nat" "y∈nat" "z∈nat" "o∈nat" "env∈list(M)""nth(o,env)=one"
shows
"sats(M,upair_name_fm(x,y,o,z),env) ⟷ is_upair_name(nth(x,env),nth(y,env),nth(z,env))"
unfolding upair_name_fm_def is_upair_name_def using assms by simp
definition
opair_name :: "i ⇒ i ⇒ i" where
"opair_name(τ,ρ) == upair_name(upair_name(τ,τ),upair_name(τ,ρ))"
definition
is_opair_name :: "[i,i,i] ⇒ o" where
"is_opair_name(x,y,z) ≡ ∃upxx∈M. ∃upxy∈M. is_upair_name(x,x,upxx) ∧ is_upair_name(x,y,upxy)
∧ is_upair_name(upxx,upxy,z)"
lemma opair_name_abs :
assumes "x∈M" "y∈M" "z∈M"
shows "is_opair_name(x,y,z) ⟷ z = opair_name(x,y)"
unfolding is_opair_name_def opair_name_def using assms upair_name_abs upair_name_closed by simp
lemma opair_name_closed :
"⟦ x∈M; y∈M ⟧ ⟹ opair_name(x,y)∈M"
unfolding opair_name_def using upair_name_closed by simp
definition
opair_name_fm :: "[i,i,i,i] ⇒ i" where
"opair_name_fm(x,y,o,z) ≡ Exists(Exists(And(upair_name_fm(x#+2,x#+2,o#+2,1),
And(upair_name_fm(x#+2,y#+2,o#+2,0),upair_name_fm(1,0,o#+2,z#+2)))))"
lemma opair_name_fm_type[TC] :
"⟦ s∈nat;x∈nat;y∈nat;o∈nat⟧ ⟹ opair_name_fm(s,x,y,o)∈formula"
unfolding opair_name_fm_def by simp
lemma sats_opair_name_fm :
assumes "x∈nat" "y∈nat" "z∈nat" "o∈nat" "env∈list(M)""nth(o,env)=one"
shows
"sats(M,opair_name_fm(x,y,o,z),env) ⟷ is_opair_name(nth(x,env),nth(y,env),nth(z,env))"
unfolding opair_name_fm_def is_opair_name_def using assms sats_upair_name_fm by simp
lemma val_upair_name : "val(G,upair_name(τ,ρ)) = {val(G,τ),val(G,ρ)}"
unfolding upair_name_def using val_Upair generic one_in_G one_in_P by simp
lemma val_opair_name : "val(G,opair_name(τ,ρ)) = <val(G,τ),val(G,ρ)>"
unfolding opair_name_def Pair_def using val_upair_name by simp
lemma val_RepFun_one: "val(G,{⟨f(x),one⟩ . x∈a}) = {val(G,f(x)) . x∈a}"
proof -
let ?A = "{f(x) . x ∈ a}"
let ?Q = "λ<x,p> . p = one"
have "one ∈ P∩G" using generic one_in_G one_in_P by simp
have "{<f(x),one> . x ∈ a} = {t ∈ ?A × P . ?Q(t)}"
using one_in_P by force
then
have "val(G,{<f(x),one> . x ∈ a}) = val(G,{t ∈ ?A × P . ?Q(t)})"
by simp
also
have "... = {val(G,t) .. t ∈ ?A , ∃p∈P∩G . ?Q(<t,p>)}"
using val_of_name_alt by simp
also
have "... = {val(G,t) . t ∈ ?A }"
using ‹one∈P∩G› by force
also
have "... = {val(G,f(x)) . x ∈ a}"
by auto
finally show ?thesis by simp
qed
subsection‹$M[G]$ is a transitive model of ZF›
interpretation mgzf: 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 separation_in_MG infinity_in_MG
by unfold_locales simp_all
definition
is_opname_check :: "[i,i,i] ⇒ o" where
"is_opname_check(s,x,y) ≡ ∃chx∈M. ∃sx∈M. is_check(x,chx) ∧ fun_apply(##M,s,x,sx) ∧
is_opair_name(chx,sx,y)"
definition
opname_check_fm :: "[i,i,i,i] ⇒ i" where
"opname_check_fm(s,x,y,o) ≡ Exists(Exists(And(check_fm(2#+x,2#+o,1),
And(fun_apply_fm(2#+s,2#+x,0),opair_name_fm(1,0,2#+o,2#+y)))))"
lemma opname_check_fm_type[TC] :
"⟦ s∈nat;x∈nat;y∈nat;o∈nat⟧ ⟹ opname_check_fm(s,x,y,o)∈formula"
unfolding opname_check_fm_def by simp
lemma sats_opname_check_fm:
assumes "x∈nat" "y∈nat" "z∈nat" "o∈nat" "env∈list(M)" "nth(o,env)=one"
"y<length(env)"
shows
"sats(M,opname_check_fm(x,y,z,o),env) ⟷ is_opname_check(nth(x,env),nth(y,env),nth(z,env))"
unfolding opname_check_fm_def is_opname_check_def
using assms sats_check_fm sats_opair_name_fm one_in_M by simp
lemma opname_check_abs :
assumes "s∈M" "x∈M" "y∈M"
shows "is_opname_check(s,x,y) ⟷ y = opair_name(check(x),s`x)"
unfolding is_opname_check_def
using assms check_abs check_in_M opair_name_abs apply_abs apply_closed by simp
lemma repl_opname_check :
assumes
"A∈M" "f∈M"
shows
"{opair_name(check(x),f`x). x∈A}∈M"
proof -
have "arity(opname_check_fm(3,0,1,2))= 4"
unfolding opname_check_fm_def opair_name_fm_def upair_name_fm_def
check_fm_def rcheck_fm_def tran_closure_fm_def is_eclose_fm_def mem_eclose_fm_def
is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def finite_ordinal_fm_def is_iterates_fm_def
is_wfrec_fm_def is_recfun_fm_def restriction_fm_def pre_image_fm_def eclose_n_fm_def
is_nat_case_fm_def quasinat_fm_def Memrel_fm_def singleton_fm_def fm_defs iterates_MH_fm_def
by (simp add:nat_simp_union)
moreover
have "x∈A ⟹ opair_name(check(x), f ` x)∈M" for x
using assms opair_name_closed apply_closed transitivity check_in_M
by simp
ultimately
show ?thesis using assms opname_check_abs[of f] sats_opname_check_fm
one_in_M
Repl_in_M[of "opname_check_fm(3,0,1,2)" "[one,f]" "is_opname_check(f)"
"λx. opair_name(check(x),f`x)"]
by simp
qed
theorem choice_in_MG:
assumes "choice_ax(##M)"
shows "choice_ax(##M[G])"
proof -
{
fix a
assume "a∈M[G]"
then
obtain τ where "τ∈M" "val(G,τ) = a"
using GenExt_def by auto
with ‹τ∈M›
have "domain(τ)∈M"
using domain_closed by simp
then
obtain s α where "s∈surj(α,domain(τ))" "Ord(α)" "s∈M" "α∈M"
using assms choice_ax_abs by auto
then
have "α∈M[G]"
using M_subset_MG generic one_in_G subsetD by blast
let ?A="domain(τ)×P"
let ?g = "{opair_name(check(β),s`β). β∈α}"
have "?g ∈ M" using ‹s∈M› ‹α∈M› repl_opname_check by simp
let ?f_dot="{⟨opair_name(check(β),s`β),one⟩. β∈α}"
have "?f_dot = ?g × {one}" by blast
from one_in_M have "{one} ∈ M" using singletonM by simp
define f where
"f == val(G,?f_dot)"
from ‹{one}∈M› ‹?g∈M› ‹?f_dot = ?g×{one}›
have "?f_dot∈M"
using cartprod_closed by simp
then
have "f ∈ M[G]"
unfolding f_def by (blast intro:GenExtI)
have "f = {val(G,opair_name(check(β),s`β)) . β∈α}"
unfolding f_def using val_RepFun_one by simp
also
have "... = {<β,val(G,s`β)> . β∈α}"
using val_opair_name valcheck generic one_in_G one_in_P by simp
finally
have "f = {<β,val(G,s`β)> . β∈α}" .
then
have 1: "domain(f) = α" "function(f)"
unfolding function_def by auto
have 2: "y ∈ a ⟹ ∃x∈α. f ` x = y" for y
proof -
fix y
assume
"y ∈ a"
with ‹val(G,τ) = a›
obtain σ where "σ∈domain(τ)" "val(G,σ) = y"
using elem_of_val[of y _ τ] by blast
with ‹s∈surj(α,domain(τ))›
obtain β where "β∈α" "s`β = σ"
unfolding surj_def by auto
with ‹val(G,σ) = y›
have "val(G,s`β) = y"
by simp
with ‹f = {<β,val(G,s`β)> . β∈α}› ‹β∈α›
have "<β,y>∈f"
by auto
with ‹function(f)›
have "f`β = y"
using function_apply_equality by simp
with ‹β∈α› show
"∃β∈α. f ` β = y"
by auto
qed
then
have "∃α∈(M[G]). ∃f'∈(M[G]). Ord(α) ∧ f' ∈ surj(α,a)"
proof (cases "a=0")
case True
then
have "0∈surj(0,a)"
unfolding surj_def by simp
then
show ?thesis using zero_in_MG by auto
next
case False
with ‹a∈M[G]›
obtain e where "e∈a" "e∈M[G]"
using transitivity_MG by blast
with 1 and 2
have "induced_surj(f,a,e) ∈ surj(α,a)"
using induced_surj_is_surj by simp
moreover from ‹f∈M[G]› ‹a∈M[G]› ‹e∈M[G]›
have "induced_surj(f,a,e) ∈ M[G]"
unfolding induced_surj_def
by (simp flip: setclass_iff)
moreover note
‹α∈M[G]› ‹Ord(α)›
ultimately show ?thesis by auto
qed
}
then
show ?thesis using mgzf.choice_ax_abs by simp
qed
end
end