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] ― ‹We keep \<^term>‹Pow(a) ∩ M[G]› to be consistent with Kunen.› 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 ― ‹\<^locale>‹G_generic1›› 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 ― ‹\<^locale>‹G_generic1›› end