section‹The Axiom of Separation in $M[G]$›
theory Separation_Axiom
imports Forcing_Theorems Separation_Rename
begin
context G_generic
begin
lemma map_val :
assumes "env∈list(M[G])"
shows "∃nenv∈list(M). env = map(val(P,G),nenv)"
using assms
proof(induct env)
case Nil
have "map(val(P,G),Nil) = Nil" by simp
then show ?case by force
next
case (Cons a l)
then obtain a' l' where
"l' ∈ list(M)" "l=map(val(P,G),l')" "a = val(P,G,a')"
"Cons(a,l) = map(val(P,G),Cons(a',l'))" "Cons(a',l') ∈ list(M)"
using ‹a∈M[G]› GenExtD
by force
then show ?case by force
qed
lemma Collect_sats_in_MG :
assumes
"c∈M[G]"
"φ ∈ formula" "env∈list(M[G])" "arity(φ) ≤ 1 #+ length(env)"
shows
"{x∈c. (M[G], [x] @ env ⊨ φ)}∈ M[G]"
proof -
from ‹c∈M[G]›
obtain π where "π ∈ M" "val(P,G, π) = c"
using GenExt_def by auto
let ?χ="And(Member(0,1 #+ length(env)),φ)" and ?Pl1="[P,leq,one]"
let ?new_form="sep_ren(length(env),forces(?χ))"
let ?ψ="Exists(Exists(And(pair_fm(0,1,2),?new_form)))"
note phi = ‹φ∈formula› ‹arity(φ) ≤ 1 #+ length(env)›
then
have "?χ∈formula" by simp
with ‹env∈_› phi
have "arity(?χ) ≤ 2#+length(env) "
using nat_simp_union leI by simp
with ‹env∈list(_)› phi
have "arity(forces(?χ)) ≤ 6 #+ length(env)"
using arity_forces_le by simp
then
have "arity(forces(?χ)) ≤ 7 #+ length(env)"
using nat_simp_union arity_forces leI by simp
with ‹arity(forces(?χ)) ≤7 #+ _› ‹env ∈ _› ‹φ ∈ formula›
have "arity(?new_form) ≤ 7 #+ length(env)" "?new_form ∈ formula"
using arity_rensep[OF definability[of "?χ"]] definability[of "?χ"] type_rensep
by auto
then
have "pred(pred(arity(?new_form))) ≤ 5 #+ length(env)" "?ψ∈formula"
unfolding pair_fm_def upair_fm_def
using nat_simp_union length_type[OF ‹env∈list(M[G])›]
pred_mono[OF _ pred_mono[OF _ ‹arity(?new_form) ≤ _›]]
by auto
with ‹arity(?new_form) ≤ _› ‹?new_form ∈ formula›
have "arity(?ψ) ≤ 5 #+ length(env)"
unfolding pair_fm_def upair_fm_def
using nat_simp_union arity_forces
by auto
from ‹φ∈formula›
have "forces(?χ) ∈ formula"
using definability by simp
from ‹π∈M› P_in_M
have "domain(π)∈M" "domain(π) × P ∈ M"
by (simp_all flip:setclass_iff)
from ‹env ∈ _›
obtain nenv where "nenv∈list(M)" "env = map(val(P,G),nenv)" "length(nenv) = length(env)"
using map_val by auto
from ‹arity(φ) ≤ _› ‹env∈_› ‹φ∈_›
have "arity(φ) ≤ 2#+ length(env)"
using le_trans[OF ‹arity(φ)≤_›] add_le_mono[of 1 2,OF _ le_refl]
by auto
with ‹nenv∈_› ‹env∈_› ‹π∈M› ‹φ∈_› ‹length(nenv) = length(env)›
have "arity(?χ) ≤ length([θ] @ nenv @ [π])" for θ
using nat_union_abs2[OF _ _ ‹arity(φ) ≤ 2#+ _›] nat_simp_union
by simp
note in_M = ‹π∈M› ‹domain(π) × P ∈ M› P_in_M one_in_M leq_in_M
{
fix u
assume "u ∈ domain(π) × P" "u ∈ M"
with in_M ‹?new_form ∈ formula› ‹?ψ∈formula› ‹nenv ∈ _›
have Eq1: "(M, [u] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ) ⟷
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
M, [θ,p,u]@?Pl1@[π] @ nenv ⊨ ?new_form)"
by (auto simp add: transitivity)
have Eq3: "θ∈M ⟹ p∈P ⟹
(M, [θ,p,u]@?Pl1@[π]@nenv ⊨ ?new_form) ⟷
(∀F. M_generic(F) ∧ p ∈ F ⟶ (M[F], map(val(P,F), [θ] @ nenv@[π]) ⊨ ?χ))"
for θ p
proof -
fix p θ
assume "θ ∈ M" "p∈P"
then
have "p∈M" using P_in_M by (simp add: transitivity)
note in_M' = in_M ‹θ ∈ M› ‹p∈M› ‹u ∈ domain(π) × P› ‹u ∈ M› ‹nenv∈_›
then
have "[θ,u] ∈ list(M)" by simp
let ?env="[p]@?Pl1@[θ] @ nenv @ [π,u]"
let ?new_env=" [θ,p,u,P,leq,one,π] @ nenv"
let ?ψ="Exists(Exists(And(pair_fm(0,1,2),?new_form)))"
have "[θ, p, u, π, leq, one, π] ∈ list(M)"
using in_M' by simp
have "?χ ∈ formula" "forces(?χ)∈ formula"
using phi by simp_all
from in_M'
have "?Pl1 ∈ list(M)" by simp
from in_M' have "?env ∈ list(M)" by simp
have Eq1': "?new_env ∈ list(M)" using in_M' by simp
then
have "(M, [θ,p,u]@?Pl1@[π] @ nenv ⊨ ?new_form) ⟷ (M, ?new_env ⊨ ?new_form)"
by simp
from in_M' ‹env ∈ _› Eq1' ‹length(nenv) = length(env)›
‹arity(forces(?χ)) ≤ 7 #+ length(env)› ‹forces(?χ)∈ formula›
‹[θ, p, u, π, leq, one, π] ∈ list(M)›
have "... ⟷ M, ?env ⊨ forces(?χ)"
using sepren_action[of "forces(?χ)" "nenv",OF _ _ ‹nenv∈list(M)›]
by simp
also from in_M'
have "... ⟷ M, ([p,P, leq, one,θ]@nenv@ [π])@[u] ⊨ forces(?χ)"
using app_assoc by simp
also
from in_M' ‹env∈_› phi ‹length(nenv) = length(env)›
‹arity(forces(?χ)) ≤ 6 #+ length(env)› ‹forces(?χ)∈formula›
have "... ⟷ M, [p,P, leq, one,θ]@ nenv @ [π] ⊨ forces(?χ)"
by (rule_tac arity_sats_iff,auto)
also
from ‹arity(forces(?χ)) ≤ 6 #+ length(env)› ‹forces(?χ)∈formula› in_M' phi
have " ... ⟷ (∀F. M_generic(F) ∧ p ∈ F ⟶
M[F], map(val(P,F), [θ] @ nenv @ [π]) ⊨ ?χ)"
using definition_of_forcing
proof (intro iffI)
assume a1: "M, [p,P, leq, one,θ] @ nenv @ [π] ⊨ forces(?χ)"
note definition_of_forcing ‹arity(φ)≤ 1#+_›
with ‹nenv∈_› ‹arity(?χ) ≤ length([θ] @ nenv @ [π])› ‹env∈_›
have "p ∈ P ⟹ ?χ∈formula ⟹ [θ,π] ∈ list(M) ⟹
M, [p,P, leq, one] @ [θ]@ nenv@[π] ⊨ forces(?χ) ⟹
∀G. M_generic(G) ∧ p ∈ G ⟶ M[G], map(val(P,G), [θ] @ nenv @[π]) ⊨ ?χ"
by auto
then
show "∀F. M_generic(F) ∧ p ∈ F ⟶
M[F], map(val(P,F), [θ] @ nenv @ [π]) ⊨ ?χ"
using ‹?χ∈formula› ‹p∈P› a1 ‹θ∈M› ‹π∈M› by simp
next
assume "∀F. M_generic(F) ∧ p ∈ F ⟶
M[F], map(val(P,F), [θ] @ nenv @[π]) ⊨ ?χ"
with definition_of_forcing [THEN iffD2] ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
show "M, [p, P, leq, one,θ] @ nenv @ [π] ⊨ forces(?χ)"
using ‹?χ∈formula› ‹p∈P› in_M'
by auto
qed
finally
show "(M, [θ,p,u]@?Pl1@[π]@nenv ⊨ ?new_form) ⟷ (∀F. M_generic(F) ∧ p ∈ F ⟶
M[F], map(val(P,F), [θ] @ nenv @ [π]) ⊨ ?χ)"
by simp
qed
with Eq1
have "(M, [u] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ) ⟷
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(∀F. M_generic(F) ∧ p ∈ F ⟶ M[F], map(val(P,F), [θ] @ nenv @ [π]) ⊨ ?χ))"
by auto
}
then
have Equivalence: "u∈ domain(π) × P ⟹ u ∈ M ⟹
(M, [u] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ) ⟷
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(∀F. M_generic(F) ∧ p ∈ F ⟶ M[F], map(val(P,F), [θ] @ nenv @[π]) ⊨ ?χ))"
for u
by simp
moreover from ‹env = _› ‹π∈M› ‹nenv∈list(M)›
have map_nenv:"map(val(P,G), nenv@[π]) = env @ [val(P,G,π)]"
using map_app_distrib append1_eq_iff by auto
ultimately
have aux:"(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧ (p∈G ⟶ M[G], [val(P,G,θ)] @ env @ [val(P,G,π)] ⊨ ?χ))"
(is "(∃θ∈M. ∃p∈P. _ ( _ ⟶ _, ?vals(θ) ⊨ _))")
if "u ∈ domain(π) × P" "u ∈ M" "M, [u]@ ?Pl1 @[π] @ nenv ⊨ ?ψ" for u
using Equivalence[THEN iffD1, OF that] generic by force
moreover
have "θ∈M ⟹ val(P,G,θ)∈M[G]" for θ
using GenExt_def by auto
moreover
have "θ∈ M ⟹ [val(P,G, θ)] @ env @ [val(P,G, π)] ∈ list(M[G])" for θ
proof -
from ‹π∈M›
have "val(P,G,π)∈ M[G]" using GenExtI by simp
moreover
assume "θ ∈ M"
moreover
note ‹env ∈ list(M[G])›
ultimately
show ?thesis
using GenExtI by simp
qed
ultimately
have "(∃θ∈M. ∃p∈P. u=⟨θ,p⟩ ∧ (p∈G ⟶ val(P,G,θ)∈nth(1 #+ length(env),[val(P,G, θ)] @ env @ [val(P,G, π)])
∧ M[G], ?vals(θ) ⊨ φ))"
if "u ∈ domain(π) × P" "u ∈ M" "M, [u] @ ?Pl1 @[π] @ nenv ⊨ ?ψ" for u
using aux[OF that] by simp
moreover from ‹env ∈ _› ‹π∈M›
have nth:"nth(1 #+ length(env),[val(P,G, θ)] @ env @ [val(P,G, π)]) = val(P,G,π)"
if "θ∈M" for θ
using nth_concat[of "val(P,G,θ)" "val(P,G,π)" "M[G]"] using that GenExtI by simp
ultimately
have "(∃θ∈M. ∃p∈P. u=⟨θ,p⟩ ∧ (p∈G ⟶ val(P,G,θ)∈val(P,G,π) ∧ M[G], ?vals(θ) ⊨ φ))"
if "u ∈ domain(π) × P" "u ∈ M" "M, [u] @ ?Pl1 @[π] @ nenv ⊨ ?ψ" for u
using that ‹π∈M› ‹env ∈ _› by simp
with ‹domain(π)×P∈M›
have "∀u∈domain(π)×P . (M, [u] @ ?Pl1 @[π] @ nenv ⊨ ?ψ) ⟶ (∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(p ∈ G ⟶ val(P,G, θ)∈val(P,G, π) ∧ M[G], ?vals(θ) ⊨ φ))"
by (simp add:transitivity)
then
have "{u∈domain(π)×P . (M,[u] @ ?Pl1 @[π] @ nenv ⊨ ?ψ) } ⊆
{u∈domain(π)×P . ∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(p ∈ G ⟶ val(P,G, θ)∈val(P,G, π) ∧ (M[G], ?vals(θ) ⊨ φ))}"
(is "?n⊆?m")
by auto
with val_mono
have first_incl: "val(P,G,?n) ⊆ val(P,G,?m)"
by simp
note ‹val(P,G,π) = c›
with ‹?ψ∈formula› ‹arity(?ψ) ≤ _› in_M ‹nenv ∈ _› ‹env ∈ _› ‹length(nenv) = _›
have "?n∈M"
using separation_ax leI separation_iff by auto
from generic
have "filter(G)" "G⊆P"
unfolding M_generic_def filter_def by simp_all
from ‹val(P,G,π) = c›
have "val(P,G,?m) =
{val(P,G,t) .. t∈domain(π) , ∃q∈P .
(∃θ∈M. ∃p∈P. ⟨t,q⟩ = ⟨θ, p⟩ ∧
(p ∈ G ⟶ val(P,G, θ) ∈ c ∧ (M[G], [val(P,G, θ)] @ env @ [c] ⊨ φ)) ∧ q ∈ G)}"
using val_of_name by auto
also
have "... = {val(P,G,t) .. t∈domain(π) , ∃q∈P.
val(P,G, t) ∈ c ∧ (M[G], [val(P,G, t)] @ env @ [c] ⊨ φ) ∧ q ∈ G}"
proof -
have "t∈M ⟹
(∃q∈P. (∃θ∈M. ∃p∈P. ⟨t,q⟩ = ⟨θ, p⟩ ∧
(p ∈ G ⟶ val(P,G, θ) ∈ c ∧ (M[G], [val(P,G, θ)] @ env @ [c] ⊨ φ)) ∧ q ∈ G))
⟷
(∃q∈P. val(P,G, t) ∈ c ∧ ( M[G], [val(P,G, t)]@env@[c]⊨ φ ) ∧ q ∈ G)" for t
by auto
then show ?thesis using ‹domain(π)∈M› by (auto simp add:transitivity)
qed
also
have "... = {x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G], [x] @ env @ [c] ⊨ φ) ∧ q ∈ G}"
proof
show "... ⊆ {x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G], [x] @ env @ [c] ⊨ φ) ∧ q ∈ G}"
by auto
next
{
fix x
assume "x∈{x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G], [x] @ env @ [c] ⊨ φ) ∧ q ∈ G}"
then
have "∃q∈P. x ∈ c ∧ (M[G], [x] @ env @ [c] ⊨ φ) ∧ q ∈ G"
by simp
with ‹val(P,G,π) = c›
have "∃q∈P. ∃t∈domain(π). val(P,G,t) =x ∧ (M[G], [val(P,G,t)] @ env @ [c] ⊨ φ) ∧ q ∈ G"
using Sep_and_Replace elem_of_val by auto
}
then
show " {x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G], [x] @ env @ [c] ⊨ φ) ∧ q ∈ G} ⊆ ..."
using SepReplace_iff by force
qed
also
have " ... = {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}"
using ‹G⊆P› G_nonempty by force
finally
have val_m: "val(P,G,?m) = {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}" by simp
have "val(P,G,?m) ⊆ val(P,G,?n)"
proof
fix x
assume "x ∈ val(P,G,?m)"
with val_m
have Eq4: "x ∈ {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}" by simp
with ‹val(P,G,π) = c›
have "x ∈ val(P,G,π)" by simp
then
have "∃θ. ∃q∈G. ⟨θ,q⟩∈π ∧ val(P,G,θ) =x"
using elem_of_val_pair by auto
then obtain θ q where
"⟨θ,q⟩∈π" "q∈G" "val(P,G,θ)=x" by auto
from ‹⟨θ,q⟩∈π›
have "θ∈M"
using domain_trans[OF trans_M ‹π∈_›] by auto
with ‹π∈M› ‹nenv ∈ _› ‹env = _›
have "[val(P,G,θ), val(P,G,π)] @ env ∈list(M[G])"
using GenExt_def by auto
with Eq4 ‹val(P,G,θ)=x› ‹val(P,G,π) = c› ‹x ∈ val(P,G,π)› nth ‹θ∈M›
have Eq5: "M[G], [val(P,G,θ)] @ env @[val(P,G,π)] ⊨ And(Member(0,1 #+ length(env)),φ)"
by auto
with ‹θ∈M› ‹π∈M› Eq5 ‹M_generic(G)› ‹φ∈formula› ‹nenv ∈ _ › ‹env = _ › map_nenv
‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
have "(∃r∈G. M, [r,P,leq,one,θ] @ nenv @[π] ⊨ forces(?χ))"
using truth_lemma
by auto
then obtain r where
"r∈G" "M, [r,P,leq,one,θ] @ nenv @ [π] ⊨ forces(?χ)" by auto
with ‹filter(G)› and ‹q∈G› obtain p where
"p∈G" "p≼q" "p≼r"
unfolding filter_def compat_in_def by force
with ‹r∈G› ‹q∈G› ‹G⊆P›
have "p∈P" "r∈P" "q∈P" "p∈M"
using P_in_M by (auto simp add:transitivity)
with ‹φ∈formula› ‹θ∈M› ‹π∈M› ‹p≼r› ‹nenv ∈ _› ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
‹M, [r,P,leq,one,θ] @ nenv @ [π] ⊨ forces(?χ)› ‹env∈_›
have "M, [p,P,leq,one,θ] @ nenv @ [π] ⊨ forces(?χ)"
using strengthening_lemma
by simp
with ‹p∈P› ‹φ∈formula› ‹θ∈M› ‹π∈M› ‹nenv ∈ _› ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
have "∀F. M_generic(F) ∧ p ∈ F ⟶
M[F], map(val(P,F), [θ] @ nenv @[π]) ⊨ ?χ"
using definition_of_forcing
by simp
with ‹p∈P› ‹θ∈M›
have Eq6: "∃θ'∈M. ∃p'∈P. ⟨θ,p⟩ = <θ',p'> ∧ (∀F. M_generic(F) ∧ p' ∈ F ⟶
M[F], map(val(P,F), [θ'] @ nenv @ [π]) ⊨ ?χ)" by auto
from ‹π∈M› ‹⟨θ,q⟩∈π›
have "⟨θ,q⟩ ∈ M" by (simp add:transitivity)
from ‹⟨θ,q⟩∈π› ‹θ∈M› ‹p∈P› ‹p∈M›
have "⟨θ,p⟩∈M" "⟨θ,p⟩∈domain(π)×P"
using tuples_in_M by auto
with ‹θ∈M› Eq6 ‹p∈P›
have "M, [⟨θ,p⟩] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ"
using Equivalence by auto
with ‹⟨θ,p⟩∈domain(π)×P›
have "⟨θ,p⟩∈?n" by simp
with ‹p∈G› ‹p∈P›
have "val(P,G,θ)∈val(P,G,?n)"
using val_of_elem[of θ p] by simp
with ‹val(P,G,θ)=x›
show "x∈val(P,G,?n)" by simp
qed
with val_m first_incl
have "val(P,G,?n) = {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}" by auto
also
have " ... = {x∈c. (M[G], [x] @ env ⊨ φ)}"
proof -
{
fix x
assume "x∈c"
moreover from assms
have "c∈M[G]"
unfolding GenExt_def by auto
moreover from this and ‹x∈c›
have "x∈M[G]"
using transitivity_MG
by simp
ultimately
have "(M[G], ([x] @ env) @[c] ⊨ φ) ⟷ (M[G], [x] @ env ⊨ φ)"
using phi ‹env ∈ _› by (rule_tac arity_sats_iff, simp_all)
}
then show ?thesis by auto
qed
finally
show "{x∈c. (M[G], [x] @ env ⊨ φ)}∈ M[G]"
using ‹?n∈M› GenExt_def by force
qed
theorem separation_in_MG:
assumes
"φ∈formula" and "arity(φ) ≤ 1 #+ length(env)" and "env∈list(M[G])"
shows
"separation(##M[G],λx. (M[G], [x] @ env ⊨ φ))"
proof -
{
fix c
assume "c∈M[G]"
moreover from ‹env ∈ _›
obtain nenv where "nenv∈list(M)"
"env = map(val(P,G),nenv)" "length(env) = length(nenv)"
using GenExt_def map_val[of env] by auto
moreover note ‹φ ∈ _› ‹arity(φ) ≤ _› ‹env ∈ _›
ultimately
have Eq1: "{x∈c. (M[G], [x] @ env ⊨ φ)} ∈ M[G]"
using Collect_sats_in_MG by auto
}
then
show ?thesis
using separation_iff rev_bexI unfolding is_Collect_def by force
qed
end
end