theory Separation_Axiom
imports Forcing_Theorems Renaming
begin
definition
perm_sep_forces :: "i" where
"perm_sep_forces == {<0,3>,<1,4>,<2,5>,<3,1>,<4,0>,<5,6>,<6,7>,<7,2>}"
lemma perm_sep_ftc : "perm_sep_forces ∈ 8 -||> 8"
by(unfold perm_sep_forces_def,(rule consI,auto)+,rule emptyI)
lemma dom_perm_sep : "domain(perm_sep_forces) = 8"
by(unfold perm_sep_forces_def,auto)
lemma perm_sep_tc : "perm_sep_forces ∈ 8 → 8"
by(subst dom_perm_sep[symmetric],rule FiniteFun_is_fun,rule perm_sep_ftc)
lemma perm_sep_env :
"{p,q,r,s,t,u,v,w} ⊆ A ⟹ j<8 ⟹
nth(j,[t,s,w,p,q,r,u,v]) = nth(perm_sep_forces`j,[q,p,v,t,s,w,r,u])"
apply(subgoal_tac "j∈nat")
apply(rule natE,simp,subst apply_fun,rule perm_sep_tc,simp add:perm_sep_forces_def,simp_all)+
apply(subst apply_fun,rule perm_sep_tc,simp add:perm_sep_forces_def,simp_all,drule ltD,auto)
done
context G_generic begin
lemmas transitivity = Transset_intf trans_M
lemma one_in_M: "one ∈ M"
by (insert one_in_P P_in_M, simp add: transitivity)
lemma six_sep_aux:
assumes
"b ∈ M" "[σ, π] ∈ list(M)" "ψ∈formula" "arity(ψ) ≤ 6"
shows
"{u ∈ b. sats(M,ψ,[u] @ [P, leq, one] @ [σ, π])} ∈ M"
proof -
from assms P_in_M leq_in_M one_in_M have
"(∀u∈M. separation(##M,λx. sats(M,ψ,[x] @ [P, leq, one] @ [σ, π])))"
using sixp_sep by simp
with ‹b ∈ M› show ?thesis
using separation_iff by auto
qed
lemma Collect_sats_in_MG :
assumes
"π ∈ M" "σ ∈ M" "val(G, π) = c" "val(G, σ) = w"
"φ ∈ formula" "arity(φ) ≤ 2"
shows
"{x∈c. sats(M[G], φ, [x, w])}∈ M[G]"
proof -
let
?χ="And(Member(0,2),φ)"
and
?Pl1="[P,leq,one]"
let
?new_form="ren(forces(?χ))`8`8`perm_sep_forces"
let
?ψ="Exists(Exists(And(pair_fm(0,1,2),?new_form)))"
have "8∈nat" by simp
note phi = ‹φ∈formula› ‹arity(φ) ≤ 2›
then have
"arity(?χ) ≤ 3"
using nat_simp_union leI by simp
with phi have
"arity(forces(?χ)) ≤ 8"
using nat_simp_union arity_forces leI by simp
with phi definability[of "?χ"] arity_forces have
"?new_form ∈ formula"
using ren_tc[of "forces(?χ)" 8 8 "perm_sep_forces"] perm_sep_tc
by simp
then have
"?ψ ∈ formula"
by simp
from ‹φ∈formula› have
"forces(?χ) ∈ formula"
using definability by simp
with ‹arity(forces(?χ)) ≤ 8› have
"arity(?new_form) ≤ 8"
using ren_arity perm_sep_tc definability by simp
then have
"arity(?ψ) ≤ 6"
unfolding pair_fm_def upair_fm_def
using nat_simp_union pred2_Un[of "8"] by simp
from ‹π∈M› ‹σ∈M› P_in_M have
"domain(π)∈M" "domain(π) × P ∈ M"
by (simp_all del:setclass_iff add:setclass_iff[symmetric])
note in_M = ‹π∈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› have
Eq1: "sats(M,?ψ,[u] @ ?Pl1 @ [σ,π]) ⟷
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
sats(M,?new_form,[θ,p,u]@?Pl1@[σ,π]))"
by (auto simp add: transitivity)
have
Eq3: "θ∈M ⟹ p∈P ⟹
sats(M,?new_form,[θ,p,u]@?Pl1@[σ,π]) ⟷
(∀F. M_generic(F) ∧ p ∈ F ⟶ sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F, π)]))"
for θ p
proof -
fix p θ
assume
"θ ∈ M" "p∈P"
with P_in_M have "p∈M" by (simp add: transitivity)
note
in_M' = in_M ‹θ ∈ M› ‹p∈M› ‹u ∈ domain(π) × P› ‹u ∈ M›
then have
"[θ,σ,u] ∈ list(M)" by simp
let
?env="?Pl1@[p,θ,σ,π,u]"
let
?new_env=" [θ,p,u,P,leq,one,σ,π]"
let
?ψ="Exists(Exists(And(pair_fm(0,1,2),?new_form)))"
have
"?χ ∈ formula" "arity(?χ) ≤ 3" "forces(?χ)∈ formula"
using phi nat_simp_union leI by auto
with arity_forces have
"arity(forces(?χ)) ≤ 7"
by simp
then have "arity(forces(?χ)) ≤ 8" using le_trans by simp
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
"sats(M,?new_form,[θ,p,u]@?Pl1@[σ,π]) ⟷ sats(M,?new_form,?new_env)"
by simp
also from ‹forces(?χ)∈formula› ‹8∈nat› ‹?env∈list(M)›
‹?new_env∈list(M)› perm_sep_tc ‹arity(forces(?χ)) ≤ 8›
have
"... ⟷ sats(M,forces(?χ),?env)"
using sats_iff_sats_ren[of _ 8 8 ?env M ?new_env] perm_sep_env
by auto
also have
"... ⟷ sats(M,forces(?χ), [P, leq, one,p,θ,σ,π]@[u])" by simp
also from ‹arity(forces(?χ)) ≤ 7› ‹forces(?χ)∈formula› in_M' phi have
"... ⟷ sats(M,forces(?χ), [P, leq, one,p,θ,σ,π])"
by (rule_tac arity_sats_iff,auto)
also from ‹arity(forces(?χ)) ≤ 7› ‹forces(?χ)∈formula› in_M' phi have
" ... ⟷ (∀F. M_generic(F) ∧ p ∈ F ⟶
sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F, π)]))"
using definition_of_forces
proof (intro iffI)
assume
a1: "sats(M, forces(?χ), [P, leq, one,p,θ,σ,π])"
note definition_of_forces
then have
"p ∈ P ⟹ ?χ∈formula ⟹ [θ,σ,π] ∈ list(M) ⟹
sats(M, forces(?χ), [P, leq, one, p] @ [θ,σ,π]) ⟹
∀G. M_generic(G) ∧ p ∈ G ⟶ sats(M[G], ?χ, map(val(G), [θ,σ,π]))" ..
then show
"∀F. M_generic(F) ∧ p ∈ F ⟶
sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F, π)])"
using ‹?χ∈formula› ‹p∈P› a1 ‹θ∈M› ‹σ∈M› ‹π∈M› by auto
next
assume
"∀F. M_generic(F) ∧ p ∈ F ⟶
sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F, π)])"
with definition_of_forces [THEN iffD2] show
"sats(M, forces(?χ), [P, leq, one,p,θ,σ,π])"
using ‹?χ∈formula› ‹p∈P› in_M' by auto
qed
finally show
"sats(M,?new_form,[θ,p,u]@?Pl1@[σ,π]) ⟷ (∀F. M_generic(F) ∧ p ∈ F ⟶
sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F, π)]))" by simp
qed
with Eq1 have
"sats(M,?ψ,[u] @ ?Pl1 @ [σ,π]) ⟷
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(∀F. M_generic(F) ∧ p ∈ F ⟶ sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F, π)])))"
by auto
}
then have
Equivalence: "u∈ domain(π) × P ⟹ u ∈ M ⟹
sats(M,?ψ,[u] @ ?Pl1 @ [σ,π]) ⟷
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(∀F. M_generic(F) ∧ p ∈ F ⟶ sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F, π)])))"
for u
by simp
with generic have
"u ∈ domain(π) × P ⟹ u ∈ M ⟹
sats(M,?ψ,[u, P, leq, one,σ, π]) ⟹
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(p ∈ G ⟶ sats(M[G], ?χ, [val(G, θ), val(G, σ), val(G, π)])))" for u
by force
moreover have
"val(G,σ)∈M[G]" and "θ∈M ⟹ val(G,θ)∈M[G]" for θ
using GenExt_def ‹σ∈M› by auto
ultimately have
"u ∈ domain(π) × P ⟹ u ∈ M ⟹
sats(M,?ψ,[u, P, leq, one,σ, π]) ⟹
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(p ∈ G ⟶
val(G,θ) ∈ val(G,π) ∧ sats(M[G], φ, [val(G, θ), val(G, σ), val(G, π)])))" for u
using ‹π∈M› by auto
with ‹domain(π)×P∈M› have
"∀u∈domain(π)×P . sats(M,?ψ,[u] @ ?Pl1 @ [σ,π]) ⟶
(∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(p ∈ G ⟶ val(G, θ)∈val(G, π) ∧ sats(M[G], φ, [val(G, θ), val(G, σ), val(G, π)])))"
by (simp add:transitivity)
then have
"{u∈domain(π)×P . sats(M,?ψ,[u] @ ?Pl1 @ [σ,π]) } ⊆
{u∈domain(π)×P . ∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
(p ∈ G ⟶ val(G, θ)∈val(G, π) ∧ sats(M[G], φ, [val(G, θ), val(G, σ), val(G, π)]))}"
(is "?n⊆?m")
by auto
with val_mono have
first_incl: "val(G,?n) ⊆ val(G,?m)"
by simp
note
‹val(G,π) = c› ‹val(G,σ) = w›
with ‹?ψ∈formula› ‹arity(?ψ) ≤ 6› in_M have
"?n∈M"
using six_sep_aux by simp
from generic have
"filter(G)" "G⊆P"
unfolding M_generic_def filter_def by simp_all
from ‹val(G,π) = c› ‹val(G,σ) = w› have
"val(G,?m) =
{val(G,t) .. t∈domain(π) , ∃q∈P .
(∃θ∈M. ∃p∈P. <t,q> = ⟨θ, p⟩ ∧
(p ∈ G ⟶ val(G, θ) ∈ c ∧ sats(M[G], φ, [val(G, θ), w, c])) ∧ q ∈ G)}"
using val_of_name by auto
also have
"... = {val(G,t) .. t∈domain(π) , ∃q∈P.
val(G, t) ∈ c ∧ sats(M[G], φ, [val(G, t), w, c]) ∧ q ∈ G}"
proof -
have
"t∈M ⟹
(∃q∈P. (∃θ∈M. ∃p∈P. <t,q> = ⟨θ, p⟩ ∧
(p ∈ G ⟶ val(G, θ) ∈ c ∧ sats(M[G], φ, [val(G, θ), w, c])) ∧ q ∈ G))
⟷
(∃q∈P. val(G, t) ∈ c ∧ sats(M[G], φ, [val(G, t), w, 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 ∧ sats(M[G], φ, [x, w, c]) ∧ q ∈ G}"
proof
show
"... ⊆ {x .. x∈c , ∃q∈P. x ∈ c ∧ sats(M[G], φ, [x, w, c]) ∧ q ∈ G}"
by auto
next
{
fix x
assume
"x∈{x .. x∈c , ∃q∈P. x ∈ c ∧ sats(M[G], φ, [x, w, c]) ∧ q ∈ G}"
then have
"∃q∈P. x ∈ c ∧ sats(M[G], φ, [x, w, c]) ∧ q ∈ G"
by simp
with ‹val(G,π) = c› have
"∃q∈P. ∃t∈domain(π). val(G,t) =x ∧ sats(M[G], φ, [val(G,t), w, c]) ∧ q ∈ G"
using Sep_and_Replace elem_of_val by auto
}
then show
" {x .. x∈c , ∃q∈P. x ∈ c ∧ sats(M[G], φ, [x, w, c]) ∧ q ∈ G} ⊆ ..."
using SepReplace_iff by force
qed
also have
" ... = {x∈c. sats(M[G], φ, [x, w, c])}"
using ‹G⊆P› G_nonempty by force
finally have
val_m: "val(G,?m) = {x∈c. sats(M[G], φ, [x, w, c])}" by simp
have
"val(G,?m) ⊆ val(G,?n)"
proof
fix x
assume
"x ∈ val(G,?m)"
with val_m have
Eq4: "x ∈ {x∈c. sats(M[G], φ, [x, w, c])}" by simp
with ‹val(G,π) = c› have
"x ∈ val(G,π)" by simp
then have
"∃θ. ∃q∈G. ⟨θ,q⟩∈π ∧ val(G,θ) =x"
using elem_of_val_pair by auto
then obtain θ q where
"⟨θ,q⟩∈π" "q∈G" "val(G,θ)=x" by auto
from ‹⟨θ,q⟩∈π› ‹π∈M› trans_M have
"θ∈M"
unfolding Pair_def Transset_def by auto
with ‹π∈M› ‹σ∈M› have
"[val(G,θ), val(G,σ), val(G,π)]∈list(M[G])"
using GenExt_def by auto
with Eq4 ‹val(G,θ)=x› ‹val(G,π) = c› ‹val(G,σ) = w› ‹x ∈ val(G,π)› have
Eq5: "sats(M[G], And(Member(0,2),φ), [val(G,θ), val(G,σ), val(G,π)])"
by auto
with ‹θ∈M› ‹π∈M› ‹σ∈M› Eq5 ‹M_generic(G)› ‹φ∈formula› have
"(∃r∈G. sats(M,forces(?χ), [P,leq,one,r,θ,σ,π]))"
using truth_lemma by auto
then obtain r where
"r∈G" "sats(M,forces(?χ), [P,leq,one,r,θ,σ,π])" by auto
with ‹filter(G)› and ‹q∈G› obtain p where
"p∈G" "<p,q>∈leq" "<p,r>∈leq"
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› ‹σ∈M› ‹<p,r>∈leq›
‹sats(M,forces(?χ), [P,leq,one,r,θ,σ,π])› have
"sats(M,forces(?χ), [P,leq,one,p,θ,σ,π])"
using strengthening by simp
with ‹p∈P› ‹φ∈formula› ‹θ∈M› ‹π∈M› ‹σ∈M› have
"∀F. M_generic(F) ∧ p ∈ F ⟶
sats(M[F], ?χ, [val(F, θ), val(F, σ), val(F,π)])"
using definition_of_forces by simp
with ‹p∈P› ‹θ∈M› have
Eq6: "∃θ'∈M. ∃p'∈P. ⟨θ,p⟩ = <θ',p'> ∧ (∀F. M_generic(F) ∧ p' ∈ F ⟶
sats(M[F], ?χ, [val(F, θ'), val(F, σ), val(F,π)]))" 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 pairM by auto
with ‹θ∈M› Eq6 ‹p∈P› have
"sats(M,?ψ,[⟨θ,p⟩] @ ?Pl1 @ [σ,π])"
using Equivalence by auto
with ‹⟨θ,p⟩∈domain(π)×P› have
"⟨θ,p⟩∈?n" by simp
with ‹p∈G› ‹p∈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∈c. sats(M[G], φ, [x, w, c])}" by auto
also have
" ... = {x∈c. sats(M[G], φ, [x, w])}"
proof -
{
fix x
assume
"x∈c"
moreover from assms have
"c∈M[G]" "w∈M[G]"
unfolding GenExt_def by auto
moreover with ‹x∈c› have
"x∈M[G]"
by (simp add:Transset_MG Transset_intf)
ultimately have
"sats(M[G], φ, [x,w]@[c]) ⟷ sats(M[G], φ, [x,w])"
using phi by (rule_tac arity_sats_iff, simp_all)
}
then show ?thesis by auto
qed
finally show
"{x∈c. sats(M[G], φ, [x, w])}∈ M[G]"
using ‹?n∈M› GenExt_def by force
qed
theorem separation_in_MG:
assumes
"φ∈formula" and "arity(φ) = 1 ∨ arity(φ)=2"
shows
"(∀a∈(M[G]). separation(##M[G],λx. sats(M[G],φ,[x,a])))"
proof -
{
fix c w
assume
"c∈M[G]" "w∈M[G]"
then obtain π σ where
"val(G, π) = c" "val(G, σ) = w" "π ∈ M" "σ ∈ M"
using GenExt_def by auto
with assms have
Eq1: "{x∈c. sats(M[G], φ, [x,w])} ∈ 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