Theory Separation_Axiom
section‹The Axiom of Separation in $M[G]$›
theory Separation_Axiom
imports Forcing_Theorems Separation_Rename
begin
context G_generic1
begin
lemma map_val :
assumes "env∈list(M[G])"
shows "∃nenv∈list(M). env = map(val(G),nenv)"
using assms
proof(induct env)
case Nil
have "map(val(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(G),l')" "a = val(G,a')"
"Cons(a,l) = map(val(G),Cons(a',l'))" "Cons(a',l') ∈ list(M)"
using GenExtD
by force
then show ?case by force
qed
lemma Collect_sats_in_MG :
assumes
"A∈M[G]"
"φ ∈ formula" "env∈list(M[G])" "arity(φ) ≤ 1 +⇩ω length(env)"
shows
"{x ∈ A . (M[G], [x] @ env ⊨ φ)} ∈ M[G]"
proof -
from ‹A∈M[G]›
obtain π where "π ∈ M" "val(G, π) = A"
using GenExt_def by auto
then
have "domain(π)∈M" "domain(π) × ℙ ∈ M"
using cartprod_closed[of _ ℙ,simplified]
by (simp_all flip:setclass_iff)
let ?χ="⋅⋅ 0 ∈ (1 +⇩ω length(env)) ⋅ ∧ φ ⋅"
let ?new_form="sep_ren(length(env),forces(?χ))"
let ?ψ="(⋅∃(⋅∃⋅⋅⟨0,1⟩ is 2 ⋅ ∧ ?new_form ⋅ ⋅)⋅)"
note phi = ‹φ∈formula› ‹arity(φ) ≤ 1 +⇩ω length(env)›
then
have "?χ∈formula" "forces(?χ) ∈ formula" "arity(φ) ≤ 2+⇩ω length(env)"
using definability le_trans[OF ‹arity(φ)≤_›] add_le_mono[of 1 2,OF _ le_refl]
by simp_all
with ‹env∈_› phi
have "arity(?χ) ≤ 2+⇩ωlength(env)"
using ord_simp_union leI FOL_arities 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 ord_simp_union arity_forces leI by simp
with ‹arity(forces(?χ)) ≤7 +⇩ω _› ‹env ∈ _› ‹φ ∈ formula›
have "arity(?new_form) ≤ 7 +⇩ω length(env)" "?new_form ∈ formula" "?ψ∈formula"
using arity_rensep[OF definability[of "?χ"]]
by auto
then
have "arity(?ψ) ≤ 5 +⇩ω length(env)"
using ord_simp_union arity_forces pred_mono[OF _ pred_mono[OF _ ‹arity(?new_form) ≤ _›]]
by (auto simp:arity)
from ‹env ∈ _›
obtain nenv where "nenv∈list(M)" "env = map(val(G),nenv)" "length(nenv) = length(env)"
using map_val by auto
from phi ‹nenv∈_› ‹env∈_› ‹π∈M› ‹φ∈_› ‹length(nenv) = length(env)›
have "arity(?χ) ≤ length([θ] @ nenv @ [π])" for θ
using union_abs2[OF ‹arity(φ) ≤ 2+⇩ω _›] ord_simp_union FOL_arities
by simp
note in_M = ‹π∈M› ‹domain(π) × ℙ ∈ M›
have Equivalence: "
(M, [u,ℙ,leq,𝟭,π] @ nenv ⊨ ?ψ) ⟷
(∃θ∈M. ∃p∈ℙ. u =⟨θ,p⟩ ∧
(∀F. M_generic(F) ∧ p ∈ F ⟶ M[F], map(val(F), [θ] @ nenv @[π]) ⊨ ?χ))"
if "u ∈ domain(π) × ℙ"
for u
proof -
from ‹u ∈ domain(π) × ℙ› ‹domain(π) × ℙ ∈ M›
have "u∈M" by (simp add:transitivity)
have "(M, [θ,p,u,ℙ,leq,𝟭,π]@nenv ⊨ ?new_form) ⟷
(∀F. M_generic(F) ∧ p ∈ F ⟶ (M[F], map(val(F), [θ] @ nenv@[π]) ⊨ ?χ))"
if "θ∈M" "p∈ℙ"
for θ p
proof -
from ‹p∈ℙ›
have "p∈M" by (simp add: transitivity)
let ?env="[p,ℙ,leq,𝟭,θ] @ nenv @ [π,u]"
let ?new_env=" [θ,p,u,ℙ,leq,𝟭,π] @ nenv"
note types = in_M ‹θ ∈ M› ‹p∈M› ‹u ∈ domain(π) × ℙ› ‹u ∈ M› ‹nenv∈_›
then
have tyenv:"?env ∈ list(M)" "?new_env ∈ list(M)"
by simp_all
from types
have eq_env:"[p, ℙ, leq, 𝟭] @ ([θ] @ nenv @ [π,u]) =
([p, ℙ, leq, 𝟭] @ ([θ] @ nenv @ [π])) @ [u]"
using app_assoc by simp
then
have "(M, [θ,p,u,ℙ,leq,𝟭,π] @ nenv ⊨ ?new_form) ⟷ (M, ?new_env ⊨ ?new_form)"
by simp
from tyenv ‹length(nenv) = length(env)› ‹arity(forces(?χ)) ≤ 7 +⇩ω length(env)› ‹forces(?χ) ∈ formula›
have "... ⟷ p ⊩ ?χ ([θ] @ nenv @ [π,u])"
using sepren_action[of "forces(?χ)" "nenv",OF _ _ ‹nenv∈list(M)›]
by simp
also from types phi ‹env∈_› ‹length(nenv) = length(env)› ‹arity(forces(?χ)) ≤ 6 +⇩ω length(env)›
have "... ⟷ p ⊩ ?χ ([θ] @ nenv @ [π])"
by (subst eq_env,rule_tac arity_sats_iff,auto)
also from types phi ‹p∈ℙ› ‹arity(forces(?χ)) ≤ 6 +⇩ω length(env)› ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
have " ... ⟷ (∀F . M_generic(F) ∧ p ∈ F ⟶
M[F], map(val(F), [θ] @ nenv @ [π]) ⊨ ?χ)"
using definition_of_forcing[where φ="⋅⋅ 0 ∈ (1 +⇩ω length(env)) ⋅ ∧ φ ⋅"]
by auto
finally
show ?thesis
by simp
qed
with in_M ‹?new_form ∈ formula› ‹?ψ∈formula› ‹nenv ∈ _› ‹u ∈ domain(π)×ℙ›
show ?thesis
by (auto simp add: transitivity)
qed
moreover from ‹env = _› ‹π∈M› ‹nenv∈list(M)›
have map_nenv:"map(val(G), nenv @ [π]) = env @ [val(G,π)]"
using map_app_distrib append1_eq_iff by auto
ultimately
have aux:"(∃θ∈M. ∃p∈ℙ. u =⟨θ,p⟩ ∧ (p∈G ⟶ M[G], [val(G,θ)] @ env @ [val(G,π)] ⊨ ?χ))"
(is "(∃θ∈M. ∃p∈ℙ. _ ( _ ⟶ M[G] , ?vals(θ) ⊨ _))")
if "u ∈ domain(π) × ℙ" "M, [u,ℙ,leq,𝟭,π] @ nenv ⊨ ?ψ" for u
using Equivalence[THEN iffD1, OF that] generic by force
moreover
have "[val(G, θ)] @ env @ [val(G, π)] ∈ list(M[G])" if "θ∈M" for θ
using ‹π∈M› ‹env ∈ list(M[G])› GenExtI that by force
ultimately
have "(∃θ∈M. ∃p∈ℙ. u=⟨θ,p⟩ ∧ (p∈G ⟶ val(G,θ)∈nth(1 +⇩ω length(env),[val(G, θ)] @ env @ [val(G, π)])
∧ (M[G], ?vals(θ) ⊨ φ)))"
if "u ∈ domain(π) × ℙ" "M, [u,ℙ,leq,𝟭,π] @ nenv ⊨ ?ψ" for u
using aux[OF that] by simp
moreover from ‹env ∈ _› ‹π∈M›
have nth:"nth(1 +⇩ω length(env),[val(G, θ)] @ env @ [val(G, π)]) = val(G,π)"
if "θ∈M" for θ
using nth_concat[of "val(G,θ)" "val(G,π)" "M[G]"] that GenExtI by simp
ultimately
have "(∃θ∈M. ∃p∈ℙ. u=⟨θ,p⟩ ∧ (p∈G ⟶ val(G,θ)∈val(G,π) ∧ (M[G],?vals(θ) ⊨ φ)))"
if "u ∈ domain(π) × ℙ" "M, [u,ℙ,leq,𝟭,π] @ nenv ⊨ ?ψ" for u
using that ‹π∈M› ‹env ∈ _› by simp
with ‹domain(π)×ℙ∈M›
have "∀u∈domain(π)×ℙ . (M, [u,ℙ,leq,𝟭,π] @ nenv ⊨ ?ψ) ⟶ (∃θ∈M. ∃p∈ℙ. u =⟨θ,p⟩ ∧
(p ∈ G ⟶ val(G, θ)∈val(G, π) ∧ (M[G],?vals(θ) ⊨ φ)))"
by (simp add:transitivity)
then
have "{u∈domain(π)×ℙ . (M,[u,ℙ,leq,𝟭,π] @ nenv ⊨ ?ψ) } ⊆
{u∈domain(π)×ℙ . ∃θ∈M. ∃p∈ℙ. u =⟨θ,p⟩ ∧
(p ∈ G ⟶ val(G, θ)∈val(G, π) ∧ (M[G], ?vals(θ) ⊨ φ))}"
(is "?n⊆?m")
by auto
then
have first_incl: "val(G,?n) ⊆ val(G,?m)"
using val_mono by simp
note ‹val(G,π) = A›
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⊆ℙ"
by auto
from ‹val(G,π) = A›
have "val(G,?m) =
{z . t∈domain(π) , (∃q∈ℙ .
(∃θ∈M. ∃p∈ℙ. ⟨t,q⟩ = ⟨θ, p⟩ ∧
(p ∈ G ⟶ val(G, θ) ∈ A ∧ (M[G], [val(G, θ)] @ env @ [A] ⊨ φ)) ∧ q ∈ G)) ∧
z=val(G,t)}"
using val_of_name by auto
also
have "... = {z . t∈domain(π) , (∃q∈ℙ.
val(G, t) ∈ A ∧ (M[G], [val(G, t)] @ env @ [A] ⊨ φ) ∧ q ∈ G) ∧ z=val(G,t)}"
using ‹domain(π)∈M› by (auto simp add:transitivity)
also
have "... = {x∈A . ∃q∈ℙ. x ∈ A ∧ (M[G], [x] @ env @ [A] ⊨ φ) ∧ q ∈ G}"
proof(intro equalityI, auto)
{
fix x q
assume "M[G], Cons(x, env @ [A]) ⊨ φ" "x∈A" "q ∈ ℙ" "q ∈ G"
from this ‹val(G,π) = A›
show "x ∈ {y . x ∈ domain(π), val(G, x) ∈ A ∧ (M[G], Cons(val(G, x), env @ [A]) ⊨ φ) ∧ (∃q∈ℙ. q ∈ G) ∧ y = val(G, x)}"
using elem_of_val by force
}
qed
also
have " ... = {x ∈ A. (M[G], [x] @ env @ [A] ⊨ φ)}"
using ‹G⊆ℙ› G_nonempty by force
finally
have val_m: "val(G,?m) = {x ∈ A. (M[G], [x] @ env @ [A] ⊨ φ)}" by simp
have "val(G,?m) ⊆ val(G,?n)"
proof
fix x
assume "x ∈ val(G,?m)"
with val_m
have "x ∈ {x ∈ A. (M[G], [x] @ env @ [A] ⊨ φ)}" by simp
with ‹val(G,π) = A›
have "x ∈ val(G,π)" by simp
then
obtain θ q where "⟨θ,q⟩∈π" "q∈G" "val(G,θ)=x" "θ∈M"
using elem_of_val_pair domain_trans[OF trans_M ‹π∈_›]
by force
with ‹π∈M› ‹nenv ∈ _› ‹env = _›
have "[val(G,θ), val(G,π)] @ env ∈ list(M[G])" "[θ] @ nenv @ [π]∈list(M)"
using GenExt_def by auto
with ‹val(G,θ)=x› ‹val(G,π) = A› ‹x ∈ val(G,π)› nth ‹θ∈M› ‹x∈ {x ∈ A . _}›
have "M[G], [val(G,θ)] @ env @ [val(G,π)] ⊨ ⋅⋅ 0 ∈ (1 +⇩ω length(env)) ⋅ ∧ φ ⋅"
by auto
with ‹[_] @ nenv @ [_] ∈ _ › map_nenv ‹arity(?χ) ≤ length(_)› ‹length(nenv) = _›
obtain r where "r∈G" "r ⊩ ?χ ([θ] @ nenv @ [π])"
using truth_lemma[OF ‹?χ∈_›,of "[θ] @ nenv @ [π]"]
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⊆ℙ›
have "p∈ℙ" "r∈ℙ" "q∈ℙ" "p∈M"
using transitivity[OF _ P_in_M] subsetD
by simp_all
with ‹φ∈formula› ‹θ∈M› ‹π∈M› ‹p≼r› ‹nenv ∈ _› ‹arity(?χ) ≤ length(_)› ‹r ⊩ ?χ _› ‹env∈_›
have "p ⊩ ?χ ([θ] @ nenv @ [π])"
using strengthening_lemma
by simp
with ‹p∈ℙ› ‹φ∈formula› ‹θ∈M› ‹π∈M› ‹nenv ∈ _› ‹arity(?χ) ≤ length(_)›
have "∀F. M_generic(F) ∧ p ∈ F ⟶
M[F], map(val(F), [θ] @ nenv @ [π]) ⊨ ?χ"
using definition_of_forcing[where φ="⋅⋅ 0 ∈ (1 +⇩ω length(env)) ⋅ ∧ φ ⋅"]
by simp
with ‹p∈ℙ› ‹θ∈M›
have Eq6: "∃θ'∈M. ∃p'∈ℙ. ⟨θ,p⟩ = ⟨θ',p'⟩ ∧ (∀F. M_generic(F) ∧ p' ∈ F ⟶
M[F], map(val(F), [θ'] @ nenv @ [π]) ⊨ ?χ)" by auto
from ‹π∈M› ‹⟨θ,q⟩∈π› ‹θ∈M› ‹p∈ℙ› ‹p∈M›
have "⟨θ,q⟩ ∈ M" "⟨θ,p⟩∈M" "⟨θ,p⟩∈domain(π)×ℙ"
using pair_in_M_iff transitivity
by auto
with ‹θ∈M› Eq6 ‹p∈ℙ›
have "M, [⟨θ,p⟩,ℙ,leq,𝟭,π] @ nenv ⊨ ?ψ"
using Equivalence by auto
with ‹⟨θ,p⟩∈domain(π)×ℙ›
have "⟨θ,p⟩∈?n" by simp
with ‹p∈G› ‹p∈ℙ›
have "val(G,θ)∈val(G,?n)"
using val_of_elem[of θ p] by simp
with ‹val(G,θ)=x›
show "x∈val(G,?n)" by simp
qed
with val_m first_incl
have "val(G,?n) = {x ∈ A. (M[G], [x] @ env @ [A] ⊨ φ)}" by auto
also from ‹A∈_› phi ‹env ∈ _›
have " ... = {x ∈ A. (M[G], [x] @ env ⊨ φ)}"
using arity_sats_iff[where env="[_]@env"] transitivity_MG
by auto
finally
show "{x ∈ A. (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 A
assume "A∈M[G]"
moreover from ‹env ∈ _›
obtain nenv where "nenv∈list(M)""env = map(val(G),nenv)" "length(env) = length(nenv)"
using GenExt_def map_val[of env] by auto
moreover note ‹φ ∈ _› ‹arity(φ) ≤ _› ‹env ∈ _›
ultimately
have "{x ∈ A . (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