Theory Replacement_Axiom
section‹The Axiom of Replacement in $M[G]$›
theory Replacement_Axiom
imports
Separation_Axiom
begin
context forcing_data1
begin
bundle sharp_simps1 = snd_abs[simp] fst_abs[simp] fst_closed[simp del, simplified, simp]
snd_closed[simp del, simplified, simp] M_inhabited[simplified, simp]
pair_in_M_iff[simp del, simplified, simp]
lemma sats_body_ground_repl_fm:
includes sharp_simps1
assumes
"∃t p. x=⟨t,p⟩" "[x,α,m,ℙ,leq,𝟭] @ nenv ∈list(M)"
"φ∈formula"
shows
"(∃τ∈M. ∃V∈M. is_Vset(λa. (##M)(a),α,V) ∧ τ ∈ V ∧ (snd(x) ⊩ φ ([fst(x),τ]@nenv)))
⟷ M, [α, x, m, ℙ, leq, 𝟭] @ nenv ⊨ body_ground_repl_fm(φ)"
unfolding body_ground_repl_fm_def rename_split_fm_def
by ((insert assms,rule iff_sats | simp add:nonempty[simplified])+,
insert sats_incr_bv_iff[where bvs="[_,_,_,_,_,_]", simplified],auto del: iffI)
end
context G_generic1
begin
lemma Replace_sats_in_MG:
assumes
"c∈M[G]" "env ∈ list(M[G])"
"φ ∈ formula" "arity(φ) ≤ 2 +⇩ω length(env)"
"univalent(##M[G], c, λx v. (M[G] , [x,v]@env ⊨ φ) )"
and
ground_replacement:
"⋀nenv. ground_replacement_assm(M,[ℙ,leq,𝟭] @ nenv, φ)"
shows
"{v. x∈c, v∈M[G] ∧ (M[G] , [x,v]@env ⊨ φ)} ∈ M[G]"
proof -
let ?R = "λ x v . v∈M[G] ∧ (M[G] , [x,v]@env ⊨ φ)"
from ‹c∈M[G]›
obtain π' where "val(G, π') = c" "π' ∈ M"
using GenExt_def by auto
then
have "domain(π')×ℙ∈M" (is "?π∈M")
using cartprod_closed domain_closed by simp
from ‹val(G, π') = c›
have "c ⊆ val(G,?π)"
using def_val[of G ?π] elem_of_val[of _ G π'] one_in_G
domain_of_prod[OF one_in_P, of "domain(π')"]
by (force del:M_genericD)
from ‹env ∈ _›
obtain nenv where "nenv∈list(M)" "env = map(val(G),nenv)"
using map_val by auto
then
have "length(nenv) = length(env)" by simp
with ‹arity(φ) ≤ _›
have "arity(φ) ≤ 2 +⇩ω length(nenv)" by simp
define f where "f(ρp) ≡ μ α. α∈M ∧ (∃τ∈M. τ ∈ Vset(α) ∧
(snd(ρp) ⊩ φ ([fst(ρp),τ] @ nenv)))" (is "_ ≡ μ α. ?P(ρp,α)") for ρp
have "f(ρp) = (μ α. α∈M ∧ (∃τ∈M. ∃V∈M. is_Vset(##M,α,V) ∧ τ∈V ∧
(snd(ρp) ⊩ φ ([fst(ρp),τ] @ nenv))))" (is "_ = (μ α. α∈M ∧ ?Q(ρp,α))") for ρp
unfolding f_def using Vset_abs Vset_closed Ord_Least_cong[of "?P(ρp)" "λ α. α∈M ∧ ?Q(ρp,α)"]
by (simp, simp del:setclass_iff)
moreover
note inM = ‹nenv∈list(M)› ‹?π∈M›
moreover
have "f(ρp) ∈ M" "Ord(f(ρp))" for ρp
unfolding f_def using Least_closed'[of "?P(ρp)"] by simp_all
ultimately
have 1:"least(##M,λα. ?Q(ρp,α),f(ρp))" for ρp
using least_abs'[of "λα. α∈M ∧ ?Q(ρp,α)" "f(ρp)"] least_conj
by (simp flip: setclass_iff)
define QQ where "QQ≡?Q"
from 1
have "least(##M,λα. QQ(ρp,α),f(ρp))" for ρp
unfolding QQ_def .
have body:"(M, [ρp,m,ℙ,leq,𝟭] @ nenv ⊨ ground_repl_fm(φ)) ⟷ least(##M, QQ(ρp), m)"
if "ρp∈M" "ρp∈?π" "m∈M" for ρp m
proof -
note inM that
moreover from this assms 1
have "(M , [α,ρp,m,ℙ,leq,𝟭] @ nenv ⊨ body_ground_repl_fm(φ)) ⟷ ?Q(ρp,α)" if "α∈M" for α
using that sats_body_ground_repl_fm[of ρp α m nenv φ]
by auto
moreover from calculation
have body:"⋀α. α ∈ M ⟹ (∃τ∈M. ∃V∈M. is_Vset(λa. a∈M, α, V) ∧ τ ∈ V ∧
(snd(ρp) ⊩ φ ([fst(ρp),τ] @ nenv))) ⟷
M, Cons(α, [ρp, m, ℙ, leq, 𝟭] @ nenv) ⊨ body_ground_repl_fm(φ)"
by simp
ultimately
show "(M , [ρp,m,ℙ,leq,𝟭] @ nenv ⊨ ground_repl_fm(φ)) ⟷ least(##M, QQ(ρp), m)"
using sats_least_fm[OF body,of 1] unfolding QQ_def ground_repl_fm_def
by (simp, simp flip: setclass_iff)
qed
then
have "univalent(##M, ?π, λρp m. M , [ρp,m] @ ([ℙ,leq,𝟭] @ nenv) ⊨ ground_repl_fm(φ))"
unfolding univalent_def by (auto intro:unique_least)
moreover from ‹length(_) = _› ‹env ∈ _›
have "length([ℙ,leq,𝟭] @ nenv) = 3 +⇩ω length(env)" by simp
moreover from ‹arity(φ) ≤ 2 +⇩ω length(nenv)›
‹length(_) = length(_)›[symmetric] ‹nenv∈_› ‹φ∈_›
have "arity(ground_repl_fm(φ)) ≤ 5 +⇩ω length(env)"
using arity_ground_repl_fm[of φ] le_trans Un_le by auto
moreover from ‹φ∈formula›
have "ground_repl_fm(φ)∈formula" by simp
moreover
note ‹length(nenv) = length(env)› inM
ultimately
obtain Y where "Y∈M"
"∀m∈M. m ∈ Y ⟷ (∃ρp∈M. ρp ∈ ?π ∧ (M, [ρp,m] @ ([ℙ,leq,𝟭] @ nenv) ⊨ ground_repl_fm(φ)))"
using ground_replacement[of nenv]
unfolding strong_replacement_def ground_replacement_assm_def replacement_assm_def by auto
with ‹least(_,QQ(_),f(_))› ‹f(_) ∈ M› ‹?π∈M› body
have "f(ρp)∈Y" if "ρp∈?π" for ρp
using that transitivity[OF _ ‹?π∈M›]
by (clarsimp,rename_tac ρ p ρp, rule_tac x="⟨ρ,p⟩" in bexI, auto)
from ‹Y∈M›
have "⋃ {y∈Y. Ord(y)} ∈ M" (is "?sup ∈ M")
using separation_Ord separation_closed Union_closed by simp
then
have "{x∈Vset(?sup). x ∈ M} × {𝟭} ∈ M" (is "?big_name ∈ M")
using Vset_closed cartprod_closed singleton_closed by simp
then
have "val(G,?big_name) ∈ M[G]"
by (blast intro:GenExtI)
have "{v. x∈c, ?R(x,v)} ⊆ val(G,?big_name)" (is "?repl⊆?big")
proof(intro subsetI)
fix v
assume "v∈?repl"
moreover from this
obtain x where "x∈c" "M[G], [x, v] @ env ⊨ φ" "v∈M[G]"
by auto
moreover
note ‹val(G,π')=c› ‹π'∈M›
moreover
from calculation
obtain ρ p where "⟨ρ,p⟩∈π'" "val(G,ρ) = x" "p∈G" "ρ∈M"
using elem_of_val_pair' by blast
moreover from this ‹v∈M[G]›
obtain σ where "val(G,σ) = v" "σ∈M"
using GenExtD by (force del:M_genericD)
moreover
note ‹φ∈_› ‹nenv∈_› ‹env = _› ‹arity(φ)≤ 2 +⇩ω length(env)›
ultimately
obtain q where "q∈G" "q ⊩ φ ([ρ,σ]@nenv)" "q∈ℙ"
using truth_lemma[OF ‹φ∈_›,of "[ρ,σ] @ nenv"]
by auto
with ‹⟨ρ,p⟩∈π'› ‹⟨ρ,q⟩∈?π ⟹ f(⟨ρ,q⟩)∈Y›
have "f(⟨ρ,q⟩)∈Y"
using generic by blast
let ?α="succ(rank(σ))"
note ‹σ∈M›
moreover from this
have "?α ∈ M" "σ ∈ Vset(?α)"
using rank_closed cons_closed Vset_Ord_rank_iff
by (simp_all flip: setclass_iff)
moreover
note ‹q ⊩ φ ([ρ,σ] @ nenv)›
ultimately
have "?P(⟨ρ,q⟩,?α)" by (auto simp del: Vset_rank_iff)
moreover
have "(μ α. ?P(⟨ρ,q⟩,α)) = f(⟨ρ,q⟩)"
unfolding f_def by simp
ultimately
obtain τ where "τ∈M" "τ ∈ Vset(f(⟨ρ,q⟩))" "q ⊩ φ ([ρ,τ] @ nenv)"
using LeastI[of "λ α. ?P(⟨ρ,q⟩,α)" ?α] by auto
with ‹q∈G› ‹ρ∈M› ‹nenv∈_› ‹arity(φ)≤ 2 +⇩ω length(nenv)›
have "M[G], map(val(G),[ρ,τ] @ nenv) ⊨ φ"
using truth_lemma[OF ‹φ∈_›, of "[ρ,τ] @ nenv"] by auto
moreover from ‹x∈c› ‹c∈M[G]›
have "x∈M[G]" using transitivity_MG by simp
moreover
note ‹M[G],[x,v] @ env⊨ φ› ‹env = map(val(G),nenv)› ‹τ∈M› ‹val(G,ρ)=x›
‹univalent(##M[G],_,_)› ‹x∈c› ‹v∈M[G]›
ultimately
have "v=val(G,τ)"
using GenExtI[of τ G] unfolding univalent_def by (auto)
from ‹τ ∈ Vset(f(⟨ρ,q⟩))› ‹Ord(f(_))› ‹f(⟨ρ,q⟩)∈Y›
have "τ ∈ Vset(?sup)"
using Vset_Ord_rank_iff lt_Union_iff[of _ "rank(τ)"] by auto
with ‹τ∈M›
have "val(G,τ) ∈ val(G,?big_name)"
using domain_of_prod[of 𝟭 "{𝟭}" "{x∈Vset(?sup). x ∈ M}" ] def_val[of G ?big_name]
one_in_G one_in_P by (auto simp del: Vset_rank_iff)
with ‹v=val(G,τ)›
show "v ∈ val(G,?big_name)"
by simp
qed
from ‹?big_name∈M›
have "?repl = {v∈?big. ∃x∈c. M[G], [x,v] @ env ⊨ φ}" (is "_ = ?rhs")
proof(intro equalityI subsetI)
fix v
assume "v∈?repl"
with ‹?repl⊆?big›
obtain x where "x∈c" "M[G], [x, v] @ env ⊨ φ" "v∈?big"
using subsetD by auto
with ‹univalent(##M[G],_,_)› ‹c∈M[G]›
show "v ∈ ?rhs"
unfolding univalent_def
using transitivity_MG ReplaceI[of "λ x v. ∃x∈c. M[G], [x, v] @ env ⊨ φ"] by blast
next
fix v
assume "v∈?rhs"
then
obtain x where
"v∈val(G, ?big_name)" "M[G], [x, v] @ env ⊨ φ" "x∈c"
by blast
moreover from this ‹c∈M[G]›
have "v∈M[G]" "x∈M[G]"
using transitivity_MG GenExtI[OF ‹?big_name∈_›,of G] by auto
moreover from calculation ‹univalent(##M[G],_,_)›
have "?R(x,y) ⟹ y = v" for y
unfolding univalent_def by auto
ultimately
show "v∈?repl"
using ReplaceI[of ?R x v c]
by blast
qed
moreover
let ?ψ = "(⋅∃⋅⋅0 ∈ 2 +⇩ω length(env) ⋅ ∧ φ⋅⋅)"
from ‹φ∈_›
have "?ψ∈formula" "arity(?ψ) ≤ 2 +⇩ω length(env)"
using pred_mono[OF _ ‹arity(φ)≤2+⇩ωlength(env)›] lt_trans[OF _ le_refl]
by (auto simp add:ord_simp_union arity)
moreover
from ‹φ∈_› ‹arity(φ)≤2+⇩ωlength(env)› ‹c∈M[G]› ‹env∈_›
have "(∃x∈c. M[G], [x,v] @ env ⊨ φ) ⟷ M[G], [v] @ env @ [c] ⊨ ?ψ" if "v∈M[G]" for v
using that nth_concat transitivity_MG[OF _ ‹c∈M[G]›] arity_sats_iff[of φ "[c]" _ "[_,v]@env"]
by auto
moreover from this
have "{v∈?big. ∃x∈c. M[G], [x,v] @ env ⊨ φ} = {v∈?big. M[G], [v] @ env @ [c] ⊨ ?ψ}"
using transitivity_MG[OF _ GenExtI, OF _ ‹?big_name∈M›]
by simp
moreover from calculation and ‹env∈_› ‹c∈_› ‹?big∈M[G]›
have "{v∈?big. M[G] , [v] @ env @ [c] ⊨ ?ψ} ∈ M[G]"
using Collect_sats_in_MG by auto
ultimately
show ?thesis by simp
qed
theorem strong_replacement_in_MG:
assumes
"φ∈formula" and "arity(φ) ≤ 2 +⇩ω length(env)" "env ∈ list(M[G])"
and
ground_replacement:
"⋀nenv. ground_replacement_assm(M,[ℙ,leq,𝟭] @ nenv, φ)"
shows
"strong_replacement(##M[G],λx v. M[G],[x,v] @ env ⊨ φ)"
proof -
let ?R="λx y . M[G], [x, y] @ env ⊨ φ"
{
fix A
let ?Y="{v . x ∈ A, v∈M[G] ∧ ?R(x,v)}"
assume 1: "(##M[G])(A)" "univalent(##M[G], A, ?R)"
with assms
have "(##M[G])(?Y)"
using Replace_sats_in_MG ground_replacement 1
unfolding ground_replacement_assm_def by auto
have "b ∈ ?Y ⟷ (∃x[##M[G]]. x ∈ A ∧ ?R(x,b))" if "(##M[G])(b)" for b
proof(rule)
from ‹(##M[G])(A)›
show "∃x[##M[G]]. x ∈ A ∧ ?R(x,b)" if "b ∈ ?Y"
using that transitivity_MG by auto
next
show "b ∈ ?Y" if "∃x[##M[G]]. x ∈ A ∧ ?R(x,b)"
proof -
from ‹(##M[G])(b)›
have "b∈M[G]" by simp
with that
obtain x where "(##M[G])(x)" "x∈A" "b∈M[G] ∧ ?R(x,b)"
by blast
moreover from this 1 ‹(##M[G])(b)›
have "x∈M[G]" "z∈M[G] ∧ ?R(x,z) ⟹ b = z" for z
unfolding univalent_def
by auto
ultimately
show ?thesis
using ReplaceI[of "λ x y. y∈M[G] ∧ ?R(x,y)"] by blast
qed
qed
then
have "∀b[##M[G]]. b ∈ ?Y ⟷ (∃x[##M[G]]. x ∈ A ∧ ?R(x,b))"
by simp
with ‹(##M[G])(?Y)›
have " (∃Y[##M[G]]. ∀b[##M[G]]. b ∈ Y ⟷ (∃x[##M[G]]. x ∈ A ∧ ?R(x,b)))"
by auto
}
then show ?thesis unfolding strong_replacement_def
by simp
qed
lemma replacement_assm_MG:
assumes
ground_replacement:
"⋀nenv. ground_replacement_assm(M,[ℙ,leq,𝟭] @ nenv, φ)"
shows
"replacement_assm(M[G],env,φ)"
using assms strong_replacement_in_MG
unfolding replacement_assm_def by simp
end
end