section‹The Powerset Axiom in $M[G]$›
theory Powerset_Axiom
imports Separation_Axiom Pairing_Axiom Union_Axiom
begin
simple_rename "perm_pow" src "[ss,p,l,o,fs,χ]" tgt "[fs,ss,sp,p,l,o,χ]"
lemma Collect_inter_Transset:
assumes
"Transset(M)" "b ∈ M"
shows
"{x∈b . P(x)} = {x∈b . P(x)} ∩ M"
using assms unfolding Transset_def
by (auto)
context G_generic begin
lemma name_components_in_M:
assumes "<σ,p>∈θ" "θ ∈ M"
shows "σ∈M" "p∈M"
proof -
from assms obtain a where
"σ ∈ a" "p ∈ a" "a∈<σ,p>"
unfolding Pair_def by auto
moreover from assms have
"<σ,p>∈M"
using transitivity by simp
moreover from calculation have
"a∈M"
using transitivity by simp
ultimately show
"σ∈M" "p∈M"
using transitivity by simp_all
qed
lemma sats_fst_snd_in_M:
assumes
"A∈M" "B∈M" "φ ∈ formula" "p∈M" "l∈M" "o∈M" "χ∈M"
"arity(φ) ≤ 6"
shows
"{sq ∈A×B . sats(M,φ,[snd(sq),p,l,o,fst(sq),χ])} ∈ M"
(is "?θ ∈ M")
proof -
have "6∈nat" "7∈nat" by simp_all
let ?φ' = "ren(φ)`6`7`perm_pow_fn"
from ‹A∈M› ‹B∈M› have
"A×B ∈ M"
using cartprod_closed by simp
from ‹arity(φ) ≤ 6› ‹φ∈ formula› ‹6∈_› ‹7∈_› have
"?φ' ∈ formula" "arity(?φ')≤7"
unfolding perm_pow_fn_def
using perm_pow_thm arity_ren ren_tc Nil_type
by auto
with ‹?φ' ∈ formula› have
1: "arity(Exists(Exists(And(pair_fm(0,1,2),?φ'))))≤5" (is "arity(?ψ)≤5")
unfolding pair_fm_def upair_fm_def
using nat_simp_union pred_le arity_type by auto
{
fix sp
note ‹A×B ∈ M›
moreover assume
"sp ∈ A×B"
moreover from calculation have
"fst(sp) ∈ A" "snd(sp) ∈ B"
using fst_type snd_type by simp_all
ultimately have
"sp ∈ M" "fst(sp) ∈ M" "snd(sp) ∈ M"
using ‹A∈M› ‹B∈M› transitivity
by simp_all
note
inM = ‹A∈M› ‹B∈M› ‹p∈M› ‹l∈M› ‹o∈M› ‹χ∈M›
‹sp∈M› ‹fst(sp)∈M› ‹snd(sp)∈M›
with 1 ‹sp ∈ M› ‹?φ' ∈ formula› have
"sats(M,?ψ,[sp,p,l,o,χ]@[p]) ⟷ sats(M,?ψ,[sp,p,l,o,χ])" (is "sats(M,_,?env0@_) ⟷ _")
using arity_sats_iff[of ?ψ "[p]" M ?env0] by auto
also from inM ‹sp ∈ A×B› have
"... ⟷ sats(M,?φ',[fst(sp),snd(sp),sp,p,l,o,χ])"
by auto
also from inM ‹φ ∈ formula› ‹arity(φ) ≤ 6› have
" ... ⟷ sats(M,φ,[snd(sp),p,l,o,fst(sp),χ])"
(is "sats(_,_,?env1) ⟷ sats(_,_,?env2)")
using sats_iff_sats_ren[of φ 6 7 ?env2 M ?env1 perm_pow_fn] perm_pow_thm
unfolding perm_pow_fn_def by simp
finally have
"sats(M,?ψ,[sp,p,l,o,χ,p]) ⟷
sats(M,φ,[snd(sp),p,l,o,fst(sp),χ])"
by simp
}
then have
"?θ = {sp∈A×B . sats(M,?ψ,[sp,p,l,o,χ,p])}"
by auto
also from assms ‹A×B∈M› have
" ... ∈ M"
proof -
from 1 have
"arity(?ψ) ≤ 6"
using leI by simp
moreover from ‹?φ' ∈ formula› have
"?ψ ∈ formula"
by simp
moreover note assms ‹A×B∈M›
ultimately show
"{x ∈ A×B . sats(M, ?ψ, [x, p, l, o, χ, p])} ∈ M"
using separation_ax separation_iff
by simp
qed
finally show ?thesis .
qed
lemma Pow_inter_MG:
assumes
"a∈M[G]"
shows
"Pow(a) ∩ M[G] ∈ M[G]"
proof -
from assms obtain τ where
"τ ∈ M" "val(G, τ) = a"
using GenExtD by auto
let
?Q="Pow(domain(τ)×P) ∩ M"
from ‹τ∈M› have
"domain(τ)×P ∈ M" "domain(τ) ∈ M"
using domain_closed cartprod_closed P_in_M
by simp_all
then have
"?Q ∈ M"
proof -
from power_ax ‹domain(τ)×P ∈ M› obtain Q where
"powerset(##M,domain(τ)×P,Q)" "Q ∈ M"
unfolding power_ax_def by auto
moreover from calculation have
"z∈Q ⟹ z∈M" for z
using transitivity by blast
ultimately have
"Q = {a∈Pow(domain(τ)×P) . a∈M}"
using ‹domain(τ)×P ∈ M› powerset_abs[of "domain(τ)×P" Q]
by (simp flip: setclass_iff)
also have
" ... = ?Q"
by auto
finally show
"?Q ∈ M"
using ‹Q∈M› by simp
qed
let
?π="?Q×{one}"
let
?b="val(G,?π)"
from ‹?Q∈M› have
"?π∈M"
using one_in_P P_in_M transitivity
by (simp flip: setclass_iff)
from ‹?π∈M› have
"?b ∈ M[G]"
using GenExtI by simp
have
"Pow(a) ∩ M[G] ⊆ ?b"
proof
fix c
assume
"c ∈ Pow(a) ∩ M[G]"
then obtain χ where
"c∈M[G]" "χ ∈ M" "val(G,χ) = c"
using GenExtD by auto
let
?θ="{sp ∈domain(τ)×P . snd(sp) ⊩ (Member(0,1)) [fst(sp),χ] }"
have
"arity(forces(Member(0,1))) = 6"
using arity_forces_at by auto
with ‹domain(τ) ∈ M› ‹χ ∈ M› have
"?θ ∈ M"
using P_in_M one_in_M leq_in_M sats_fst_snd_in_M
by simp
then have
"?θ ∈ ?Q"
by auto
then have
"val(G,?θ) ∈ ?b"
using one_in_G one_in_P generic val_of_elem [of ?θ one ?π G]
by auto
have
"val(G,?θ) = c"
proof
{
fix x
assume
"x ∈ val(G,?θ)"
then obtain σ p where
1: "<σ,p>∈?θ" "p∈G" "val(G,σ) = x"
using elem_of_val_pair
by blast
moreover from ‹<σ,p>∈?θ› ‹?θ ∈ M› have
"σ∈M"
using name_components_in_M[of _ _ ?θ] by auto
moreover from 1 have
"(p ⊩ (Member(0,1)) [σ,χ])" "p∈P"
by simp_all
moreover note
‹val(G,χ) = c›
ultimately have
"sats(M[G],Member(0,1),[x,c])"
using ‹χ ∈ M› generic definition_of_forcing nat_simp_union
by auto
moreover have
"x∈M[G]"
using ‹val(G,σ) = x› ‹σ∈M› ‹χ∈M› GenExtI by blast
ultimately have
"x∈c"
using ‹c∈M[G]› by simp
}
then show
"val(G,?θ) ⊆ c"
by auto
next
{
fix x
assume
"x ∈ c"
with ‹c ∈ Pow(a) ∩ M[G]› have
"x ∈ a" "c∈M[G]" "x∈M[G]"
using transitivity_MG
by auto
with ‹val(G, τ) = a› obtain σ where
"σ∈domain(τ)" "val(G,σ) = x"
using elem_of_val
by blast
moreover note ‹x∈c› ‹val(G,χ) = c›
moreover from calculation have
"val(G,σ) ∈ val(G,χ)"
by simp
moreover note ‹c∈M[G]› ‹x∈M[G]›
moreover from calculation have
"sats(M[G],Member(0,1),[x,c])"
by simp
moreover have
"Member(0,1)∈formula" by simp
moreover have
"σ∈M"
proof -
from ‹σ∈domain(τ)› obtain p where
"<σ,p> ∈ τ"
by auto
with ‹τ∈M› show ?thesis
using name_components_in_M by blast
qed
moreover note ‹χ ∈ M›
ultimately obtain p where
"p∈G" "(p ⊩ Member(0,1) [σ,χ])"
using generic truth_lemma[of "Member(0,1)" "G" "[σ,χ]" ] nat_simp_union
by auto
moreover from ‹p∈G› have
"p∈P"
using generic unfolding M_generic_def filter_def by blast
ultimately have
"<σ,p>∈?θ"
using ‹σ∈domain(τ)› by simp
with ‹val(G,σ) = x› ‹p∈G› have
"x∈val(G,?θ)"
using val_of_elem [of _ _ "?θ"] by auto
}
then show
"c ⊆ val(G,?θ)"
by auto
qed
with ‹val(G,?θ) ∈ ?b› show
"c∈?b"
by simp
qed
then have
"Pow(a) ∩ M[G] = {x∈?b . x⊆a & x∈M[G]}"
by auto
also from ‹a∈M[G]› have
" ... = {x∈?b . sats(M[G],subset_fm(0,1),[x,a]) & x∈M[G]}"
using Transset_MG by force
also have
" ... = {x∈?b . sats(M[G],subset_fm(0,1),[x,a])} ∩ M[G]"
by auto
also from ‹?b∈M[G]› have
" ... = {x∈?b . sats(M[G],subset_fm(0,1),[x,a])}"
using Collect_inter_Transset Transset_MG
by simp
also from ‹?b∈M[G]› ‹a∈M[G]›
have
" ... ∈ M[G]"
using Collect_sats_in_MG GenExtI nat_simp_union by simp
finally show ?thesis .
qed
end
context G_generic begin
interpretation mgtriv: M_trivial "##M[G]"
using generic Union_MG pairing_in_MG zero_in_MG transitivity_MG
unfolding M_trivial_def M_trans_def M_trivial_axioms_def by (simp; blast)
theorem power_in_MG :
"power_ax(##(M[G]))"
unfolding power_ax_def
proof (intro rallI, simp only:setclass_iff rex_setclass_is_bex)
fix a
assume
"a ∈ M[G]"
then
have "(##M[G])(a)" by simp
have
"{x∈Pow(a) . x ∈ M[G]} = Pow(a) ∩ M[G]"
by auto
also from ‹a∈M[G]› have
" ... ∈ M[G]"
using Pow_inter_MG by simp
finally have
"{x∈Pow(a) . x ∈ M[G]} ∈ M[G]" .
moreover from ‹a∈M[G]› ‹{x∈Pow(a) . x ∈ M[G]} ∈ _› have
"powerset(##M[G], a, {x∈Pow(a) . x ∈ M[G]})"
using mgtriv.powerset_abs[OF ‹(##M[G])(a)›]
by simp
ultimately show
"∃x∈M[G] . powerset(##M[G], a, x)"
by auto
qed
end
end