Theory Powerset_Axiom
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,χ]"
context G_generic1
begin
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 . M, [q,p,l,o,s,χ] ⊨ φ} ∈ M" (is "?θ ∈ M")
proof -
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›
have "?φ' ∈ formula" "arity(?φ')≤7"
unfolding perm_pow_fn_def
using perm_pow_thm arity_ren ren_tc Nil_type
by auto
with ‹?φ' ∈ formula›
have arty: "arity(Exists(Exists(And(pair_fm(0,1,2),?φ'))))≤5" (is "arity(?ψ)≤5")
using ord_simp_union pred_le
by (auto simp:arity)
{
fix sp
note ‹A×B ∈ M› ‹A∈M› ‹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 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 arty ‹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 "... ⟷ 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 "(M,[sp,p,l,o,χ,p] ⊨ ?ψ) ⟷ M, [snd(sp),p,l,o,fst(sp),χ] ⊨ φ"
by simp
}
then
have "?θ = {sp∈A×B . sats(M,?ψ,[sp,p,l,o,χ,p])}"
by auto
with assms ‹A×B∈M›
show ?thesis
using separation_ax separation_iff arty leI ‹?φ' ∈ formula›
by simp
qed
declare nat_into_M[rule del, simplified setclass_iff, intro]
lemmas ssimps = domain_closed cartprod_closed cons_closed Pow_rel_closed
declare ssimps [simp del, simplified setclass_iff, simp, intro]
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⇗M⇖(domain(τ)×ℙ)"
let ?π="?Q×{𝟭}"
let ?b="val(G,?π)"
from ‹τ∈M›
have "domain(τ)×ℙ ∈ M" "domain(τ) ∈ M"
by simp_all
then
have "?b ∈ M[G]"
by (auto intro!:GenExtI)
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 GenExt_iff by auto
let ?θ="{⟨σ,p⟩ ∈domain(τ)×ℙ . p ⊩ ⋅0 ∈ 1⋅ [σ,χ] }"
have "arity(forces( ⋅0 ∈ 1⋅ )) = 6"
using arity_forces_at by auto
with ‹domain(τ) ∈ M› ‹χ ∈ M›
have "?θ ∈ M"
using sats_fst_snd_in_M
by simp
with ‹domain(τ)×ℙ ∈ M›
have "?θ ∈ ?Q"
using Pow_rel_char by auto
have "val(G,?θ) = c"
proof(intro equalityI subsetI)
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 ⊩ ⋅0 ∈ 1⋅ [σ,χ]" "p∈ℙ"
by simp_all
moreover
note ‹val(G,χ) = c› ‹χ ∈ M›
ultimately
have "M[G], [x, c] ⊨ ⋅0 ∈ 1⋅"
using generic definition_of_forcing[where φ="⋅0 ∈ 1⋅"] ord_simp_union
by auto
moreover from ‹σ∈M› ‹χ∈M›
have "x∈M[G]"
using ‹val(G,σ) = x› 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(G, τ) = a›
obtain σ where "σ∈domain(τ)" "val(G,σ) = x"
using elem_of_val by blast
moreover
note ‹x∈c› ‹val(G,χ) = c› ‹c∈M[G]› ‹x∈M[G]›
moreover from calculation
have "val(G,σ) ∈ val(G,χ)"
by simp
moreover from calculation
have "M[G], [x, c] ⊨ ⋅0 ∈ 1⋅"
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 ⊩ ⋅0 ∈ 1⋅ [σ,χ]"
using generic truth_lemma[of "⋅0 ∈ 1⋅" "[σ,χ]" ] ord_simp_union
by auto
moreover from ‹p∈G›
have "p∈ℙ"
using generic by blast
ultimately
have "⟨σ,p⟩∈?θ"
using ‹σ∈domain(τ)› by simp
with ‹val(G,σ) = x› ‹p∈G›
show "x∈val(G,?θ)"
using val_of_elem [of _ _ "?θ" G] by auto
qed
with ‹?θ ∈ ?Q›
show "c∈?b"
using one_in_G generic val_of_elem [of ?θ 𝟭 ?π G]
by auto
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] ⊨ ⋅0 ⊆ 1⋅ )} ∩ M[G]"
using Transset_MG by force
also from ‹?b∈M[G]›
have " ... = {x∈?b . ( M[G], [x,a] ⊨ ⋅0 ⊆ 1⋅ )}"
by (intro equalityI) (auto dest:ext.transM)
also from ‹?b∈M[G]› ‹a∈M[G]›
have " ... ∈ M[G]"
using Collect_sats_in_MG GenExtI ord_simp_union by (simp add:arity)
finally
show ?thesis .
qed
end
sublocale G_generic1 ⊆ ext: M_trivial "##M[G]"
using generic Union_MG pairing_in_MG
by unfold_locales (simp; blast)
context G_generic1 begin
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
text‹After simplification, we have to show that for every
\<^term>‹a∈M[G]› there exists some \<^term>‹x∈M[G]› satisfying
\<^term>‹powerset(##M[G],a,x)››
assume "a ∈ M[G]"
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]› this
have "powerset(##M[G], a, {x∈Pow(a) . x ∈ M[G]})"
using ext.powerset_abs
by simp
ultimately
show "∃x∈M[G] . powerset(##M[G], a, x)"
by auto
qed
end
end