section‹The Powerset Axiom in $M[G]$›
theory Powerset_Axiom
imports Renaming_Auto 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
"{<s,q> ∈A×B . sats(M,φ,[q,p,l,o,s,χ])} ∈ 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 "M, [sp,p,l,o,χ]@[p] ⊨ ?ψ ⟷ M,[sp,p,l,o,χ] ⊨ ?ψ" (is "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(P,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 ?thesis using ‹Q∈M› by simp
qed
let ?π="?Q×{one}"
let ?b="val(P,G,?π)"
from ‹?Q∈M›
have "?π∈M"
using one_in_P P_in_M transitivity
by (simp flip: setclass_iff)
then
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(P,G,χ) = c"
using GenExtD by auto
let ?θ="{<σ,p> ∈domain(τ)×P . p ⊩ (Member(0,1)) [σ,χ] }"
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(P,G,?θ) ∈ ?b"
using one_in_G one_in_P generic val_of_elem [of ?θ one ?π G]
by auto
have "val(P,G,?θ) = c"
proof(intro equalityI subsetI)
fix x
assume "x ∈ val(P,G,?θ)"
then obtain σ p where
1: "<σ,p>∈?θ" "p∈G" "val(P,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(P,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(P,G,σ) = x› ‹σ∈M› ‹χ∈M› GenExtI by blast
ultimately
show "x∈c"
using ‹c∈M[G]› by simp
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(P,G, τ) = a›
obtain σ where "σ∈domain(τ)" "val(P,G,σ) = x"
using elem_of_val by blast
moreover note ‹x∈c› ‹val(P,G,χ) = c›
moreover from calculation
have "val(P,G,σ) ∈ val(P,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 "σ∈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 by blast
ultimately
have "<σ,p>∈?θ"
using ‹σ∈domain(τ)› by simp
with ‹val(P,G,σ) = x› ‹p∈G›
show "x∈val(P,G,?θ)"
using val_of_elem [of _ _ "?θ"] by auto
qed
with ‹val(P,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 . (M[G], [x,a] ⊨ subset_fm(0,1)) ∧ x∈M[G]}"
using Transset_MG by force
also
have " ... = {x∈?b . (M[G], [x,a] ⊨ subset_fm(0,1))} ∩ M[G]"
by auto
also from ‹?b∈M[G]›
have " ... = {x∈?b . (M[G], [x,a] ⊨ subset_fm(0,1))}"
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