Theory ZF_Trans_Interpretations
section‹Further instances of axiom-schemes›
theory ZF_Trans_Interpretations
imports
Internal_ZFC_Axioms
Replacement_Instances
begin
locale M_ZF2 = M_ZF1 +
assumes
replacement_ax2:
"replacement_assm(M,env,ordtype_replacement_fm)"
"replacement_assm(M,env,wfrec_ordertype_fm)"
"replacement_assm(M,env,wfrec_Aleph_fm)"
"replacement_assm(M,env,omap_replacement_fm)"
definition instances2_fms where "instances2_fms ≡
{ ordtype_replacement_fm,
wfrec_ordertype_fm,
wfrec_Aleph_fm,
omap_replacement_fm }"
lemmas replacement_instances2_defs =
ordtype_replacement_fm_def wfrec_ordertype_fm_def
wfrec_Aleph_fm_def omap_replacement_fm_def
declare (in M_ZF2) replacement_instances2_defs [simp]
locale M_ZF2_trans = M_ZF1_trans + M_ZF2
locale M_ZFC2 = M_ZFC1 + M_ZF2
locale M_ZFC2_trans = M_ZFC1_trans + M_ZF2_trans + M_ZFC2
locale M_ZF2_ground_notCH = M_ZF2 + M_ZF_ground_notCH
locale M_ZF2_ground_notCH_trans = M_ZF2_trans + M_ZF2_ground_notCH + M_ZF_ground_notCH_trans
locale M_ZFC2_ground_notCH = M_ZFC2 + M_ZF2_ground_notCH
locale M_ZFC2_ground_notCH_trans = M_ZFC2_trans + M_ZFC2_ground_notCH + M_ZF2_ground_notCH_trans
locale M_ZFC2_ground_CH_trans = M_ZFC2_ground_notCH_trans + M_ZF_ground_CH_trans
locale M_ctm2 = M_ctm1 + M_ZF2_ground_notCH_trans
locale M_ctm2_AC = M_ctm2 + M_ctm1_AC + M_ZFC2_ground_notCH_trans
locale M_ctm2_AC_CH = M_ctm2_AC + M_ZFC2_ground_CH_trans
lemmas (in M_ZF1_trans) separation_instances =
separation_well_ord_iso
separation_obase_equals separation_is_obase
separation_PiP_rel separation_surjP_rel
separation_radd_body separation_rmult_body
context M_ZF2_trans
begin
lemma replacement_HAleph_wfrec_repl_body:
"B∈M ⟹ strong_replacement(##M, HAleph_wfrec_repl_body(##M,B))"
using strong_replacement_rel_in_ctm[where φ="HAleph_wfrec_repl_body_fm(2,0,1)" and env="[B]"]
zero_in_M arity_HAleph_wfrec_repl_body_fm replacement_ax2(3) ord_simp_union
by simp
lemma HAleph_wfrec_repl:
"(##M)(sa) ⟹
(##M)(esa) ⟹
(##M)(mesa) ⟹
strong_replacement
(##M,
λx z. ∃y[##M].
pair(##M, x, y, z) ∧
(∃f[##M].
(∀z[##M].
z ∈ f ⟷
(∃xa[##M].
∃y[##M].
∃xaa[##M].
∃sx[##M].
∃r_sx[##M].
∃f_r_sx[##M].
pair(##M, xa, y, z) ∧
pair(##M, xa, x, xaa) ∧
upair(##M, xa, xa, sx) ∧
pre_image(##M, mesa, sx, r_sx) ∧ restriction(##M, f, r_sx, f_r_sx) ∧ xaa ∈ mesa ∧ is_HAleph(##M, xa, f_r_sx, y))) ∧
is_HAleph(##M, x, f, y)))"
using replacement_HAleph_wfrec_repl_body unfolding HAleph_wfrec_repl_body_def by simp
lemma replacement_is_order_eq_map:
"A∈M ⟹ r∈M ⟹ strong_replacement(##M, order_eq_map(##M,A,r))"
using strong_replacement_rel_in_ctm[where φ="order_eq_map_fm(2,3,0,1)" and env="[A,r]" and f="order_eq_map(##M,A,r)"]
order_eq_map_iff_sats[where env="[_,_,A,r]"] zero_in_M fst_snd_closed pair_in_M_iff
arity_order_eq_map_fm ord_simp_union replacement_ax2(4)
by simp
end
definition omap_wfrec_body where
"omap_wfrec_body(A,r) ≡ (⋅∃⋅image_fm(2, 0, 1) ∧ pred_set_fm(A #+ 9, 3, r #+ 9, 0) ⋅⋅)"
lemma type_omap_wfrec_body_fm :"A∈nat ⟹ r∈nat ⟹ omap_wfrec_body(A,r)∈formula"
unfolding omap_wfrec_body_def by simp
lemma arity_aux : "A∈nat ⟹ r∈nat ⟹ arity(omap_wfrec_body(A,r)) = (9+⇩ωA) ∪ (9+⇩ωr)"
unfolding omap_wfrec_body_def
using arity_image_fm arity_pred_set_fm pred_Un_distrib union_abs2[of 3] union_abs1
by (simp add:FOL_arities, auto simp add:Un_assoc[symmetric] union_abs1)
lemma arity_omap_wfrec: "A∈nat ⟹ r∈nat ⟹
arity(is_wfrec_fm(omap_wfrec_body(A,r),succ(succ(succ(r))), 1, 0)) =
(4+⇩ωA) ∪ (4+⇩ωr)"
using Arities.arity_is_wfrec_fm[OF _ _ _ _ _ arity_aux,of A r "3+⇩ωr" 1 0] pred_Un_distrib
union_abs1 union_abs2 type_omap_wfrec_body_fm
by auto
lemma arity_isordermap: "A∈nat ⟹ r∈nat ⟹d∈nat⟹
arity(is_ordermap_fm(A,r,d)) = succ(d) ∪ (succ(A) ∪ succ(r))"
unfolding is_ordermap_fm_def
using arity_lambda_fm[where i="(4+⇩ωA) ∪ (4+⇩ωr)",OF _ _ _ _ arity_omap_wfrec,
unfolded omap_wfrec_body_def] pred_Un_distrib union_abs1
by auto
lemma arity_is_ordertype: "A∈nat ⟹ r∈nat ⟹d∈nat⟹
arity(is_ordertype_fm(A,r,d)) = succ(d) ∪ (succ(A) ∪ succ(r))"
unfolding is_ordertype_fm_def
using arity_isordermap arity_image_fm pred_Un_distrib FOL_arities
by auto
lemma arity_is_order_body: "arity(is_order_body_fm(1,0)) = 2"
using arity_is_order_body_fm arity_is_ordertype ord_simp_union
by (simp add:FOL_arities)
lemma (in M_ZF2_trans) replacement_is_order_body:
"strong_replacement(##M, λx z . ∃y[##M]. is_order_body(##M,x,y) ∧ z = ⟨x,y⟩)"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f] ⊨ (⋅∃ ⋅is_order_body_fm(1,0) ∧ pair_fm(1,0,2) ⋅⋅)",THEN iffD1])
apply(simp add: is_order_body_iff_sats[where env="[_,_]",symmetric])
apply(simp_all add:zero_in_M )
apply(rule_tac replacement_ax2(1)[unfolded replacement_assm_def, rule_format, where env="[]",simplified])
apply(simp_all add:arity_is_order_body arity pred_Un_distrib ord_simp_union)
done
definition H_order_pred where
"H_order_pred(A,r) ≡ λx f . f `` Order.pred(A, x, r)"
relationalize "H_order_pred" "is_H_order_pred"
lemma (in M_basic) H_order_pred_abs :
"M(A) ⟹ M(r) ⟹ M(x) ⟹ M(f) ⟹ M(z) ⟹
is_H_order_pred(M,A,r,x,f,z) ⟷ z = H_order_pred(A,r,x,f)"
unfolding is_H_order_pred_def H_order_pred_def
by simp
synthesize "is_H_order_pred" from_definition assuming "nonempty"
lemma (in M_ZF2_trans) wfrec_replacement_order_pred:
"A∈M ⟹ r∈M ⟹ wfrec_replacement(##M, λx g z. is_H_order_pred(##M,A,r,x,g,z) , r)"
unfolding wfrec_replacement_def is_wfrec_def M_is_recfun_def is_H_order_pred_def
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f,r,A] ⊨ order_pred_wfrec_body_fm(3,2,1,0)",THEN iffD1])
apply(subst order_pred_wfrec_body_def[symmetric])
apply(rule_tac order_pred_wfrec_body_iff_sats[where env="[_,_,r,A]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax2(2)[unfolded replacement_assm_def, rule_format, where env="[r,A]",simplified])
apply(simp_all add: arity_order_pred_wfrec_body_fm ord_simp_union)
done
lemma (in M_ZF2_trans) wfrec_replacement_order_pred':
"A∈M ⟹ r∈M ⟹ wfrec_replacement(##M, λx g z. z = H_order_pred(A,r,x,g) , r)"
using wfrec_replacement_cong[OF H_order_pred_abs[of A r,rule_format] refl,THEN iffD1,
OF _ _ _ _ _ wfrec_replacement_order_pred[of A r]]
by simp
sublocale M_ZF2_trans ⊆ M_pre_cardinal_arith "##M"
using separation_instances wfrec_replacement_order_pred'[unfolded H_order_pred_def]
replacement_is_order_eq_map[unfolded order_eq_map_def]
by unfold_locales simp_all
definition is_well_ord_fst_snd where
"is_well_ord_fst_snd(A,x) ≡ (∃a[A]. ∃b[A]. is_well_ord(A,a,b) ∧ is_snd(A, x, b) ∧ is_fst(A, x, a))"
synthesize "is_well_ord_fst_snd" from_definition assuming "nonempty"
arity_theorem for "is_well_ord_fst_snd_fm"
lemma (in M_ZF2_trans) separation_well_ord: "separation(##M, λx. is_well_ord(##M,fst(x), snd(x)))"
using arity_is_well_ord_fst_snd_fm is_well_ord_iff_sats[symmetric] nonempty
fst_closed snd_closed fst_abs snd_abs
separation_in_ctm[where env="[]" and φ="is_well_ord_fst_snd_fm(0)"]
by(simp_all add: is_well_ord_fst_snd_def)
sublocale M_ZF2_trans ⊆ M_pre_aleph "##M"
using HAleph_wfrec_repl replacement_is_order_body
separation_well_ord separation_Pow_rel
by unfold_locales (simp_all add: transrec_replacement_def
wfrec_replacement_def is_wfrec_def M_is_recfun_def flip:setclass_iff)
arity_theorem intermediate for "is_HAleph_fm"
lemma arity_is_HAleph_fm: "arity(is_HAleph_fm(2, 1, 0)) = 3"
using arity_fun_apply_fm[of "11" 0 1,simplified]
arity_is_HAleph_fm' arity_ordinal_fm arity_is_If_fm
arity_empty_fm arity_is_Limit_fm
arity_is_If_fm
arity_is_Limit_fm arity_empty_fm
arity_Replace_fm[where i="12" and v=10 and n=3]
pred_Un_distrib ord_simp_union
by (simp add:FOL_arities)
lemma arity_is_Aleph[arity]: "arity(is_Aleph_fm(0, 1)) = 2"
unfolding is_Aleph_fm_def
using arity_transrec_fm[OF _ _ _ _ arity_is_HAleph_fm] ord_simp_union
by simp
definition bex_Aleph_rel :: "[i⇒o,i,i] ⇒ o" where
"bex_Aleph_rel(M,x) ≡ λy. ∃z∈x. y = ℵ⇘z⇙⇗M⇖"
relationalize "bex_Aleph_rel" "is_bex_Aleph"
schematic_goal sats_is_bex_Aleph_fm_auto:
"a ∈ nat ⟹ c ∈ nat ⟹ env ∈ list(A) ⟹
a < length(env) ⟹ c < length(env) ⟹ 0 ∈ A ⟹
is_bex_Aleph(##A, nth(a, env), nth(c, env)) ⟷ A, env ⊨ ?fm(a, c)"
unfolding is_bex_Aleph_def
by (rule iff_sats | simp)+
synthesize_notc "is_bex_Aleph" from_schematic
lemma is_bex_Aleph_fm_type [TC]:
"x ∈ ω ⟹ z ∈ ω ⟹ is_bex_Aleph_fm(x, z) ∈ formula"
unfolding is_bex_Aleph_fm_def by simp
lemma sats_is_bex_Aleph_fm:
"x ∈ ω ⟹
z ∈ ω ⟹ x < length(env) ⟹ z < length(env) ⟹
env ∈ list(Aa) ⟹
0 ∈ Aa ⟹
(Aa, env ⊨ is_bex_Aleph_fm(x, z)) ⟷
is_bex_Aleph(##Aa,nth(x, env), nth(z, env))"
using sats_is_bex_Aleph_fm_auto unfolding is_bex_Aleph_def is_bex_Aleph_fm_def
by simp
lemma is_bex_Aleph_iff_sats [iff_sats]:
"nth(x, env) = xa ⟹
nth(z, env) = za ⟹
x ∈ ω ⟹
z ∈ ω ⟹ x < length(env) ⟹ z < length(env) ⟹
env ∈ list(Aa) ⟹
0 ∈ Aa ⟹
is_bex_Aleph(##Aa, xa, za) ⟷
Aa, env ⊨ is_bex_Aleph_fm(x, z)"
using sats_is_bex_Aleph_fm by simp
arity_theorem for "is_bex_Aleph_fm"
lemma (in M_ZF1_trans) separation_is_bex_Aleph:
assumes "(##M)(A)"
shows "separation(##M,is_bex_Aleph(##M, A))"
using assms separation_in_ctm[where env="[A]" and φ="is_bex_Aleph_fm(1,0)",
OF _ _ _ is_bex_Aleph_iff_sats[symmetric],
of "λ_.A"]
nonempty arity_is_bex_Aleph_fm is_bex_Aleph_fm_type
by (simp add:ord_simp_union)
lemma (in M_pre_aleph) bex_Aleph_rel_abs:
assumes "Ord(u)" "M(u)" "M(v)"
shows "is_bex_Aleph(M, u, v) ⟷ bex_Aleph_rel(M,u,v)"
unfolding is_bex_Aleph_def bex_Aleph_rel_def
using assms is_Aleph_iff transM[of _ u] Ord_in_Ord
by simp
lemma (in M_ZF2_trans) separation_bex_Aleph_rel:
"Ord(x) ⟹ (##M)(x) ⟹ separation(##M, bex_Aleph_rel(##M,x))"
using separation_is_bex_Aleph bex_Aleph_rel_abs
separation_cong[where P="is_bex_Aleph(##M,x)" and M="##M",THEN iffD1]
unfolding bex_Aleph_rel_def
by simp
sublocale M_ZF2_trans ⊆ M_aleph "##M"
using separation_bex_Aleph_rel[unfolded bex_Aleph_rel_def]
by unfold_locales
sublocale M_ZF1_trans ⊆ M_FiniteFun "##M"
using separation_is_function separation_omfunspace
by unfold_locales simp
sublocale M_ZFC2_trans ⊆ M_cardinal_AC "##M"
using lam_replacement_minimum
by unfold_locales simp
lemma (in M_ZF1_trans) separation_cardinal_rel_lesspoll_rel:
"(##M)(κ) ⟹ separation(##M, λx. x ≺⇗M⇖ κ)"
using separation_in_ctm[where φ="( ⋅0 ≺ 1⋅ )" and env="[κ]"]
is_lesspoll_iff nonempty
arity_is_cardinal_fm arity_is_lesspoll_fm arity_is_bij_fm ord_simp_union
by (simp add:FOL_arities)
sublocale M_ZFC2_trans ⊆ M_library "##M"
using separation_cardinal_rel_lesspoll_rel lam_replacement_minimum
by unfold_locales simp_all
locale M_ZF3 = M_ZF2 +
assumes
ground_replacements3:
"ground_replacement_assm(M,env,ordtype_replacement_fm)"
"ground_replacement_assm(M,env,wfrec_ordertype_fm)"
"ground_replacement_assm(M,env,eclose_abs_fm)"
"ground_replacement_assm(M,env,wfrec_rank_fm)"
"ground_replacement_assm(M,env,transrec_VFrom_fm)"
"ground_replacement_assm(M,env,eclose_closed_fm)"
"ground_replacement_assm(M,env,wfrec_Aleph_fm)"
"ground_replacement_assm(M,env,omap_replacement_fm)"
definition instances3_fms where "instances3_fms ≡
{ ground_repl_fm(ordtype_replacement_fm),
ground_repl_fm(wfrec_ordertype_fm),
ground_repl_fm(eclose_abs_fm),
ground_repl_fm(wfrec_rank_fm),
ground_repl_fm(transrec_VFrom_fm),
ground_repl_fm(eclose_closed_fm),
ground_repl_fm(wfrec_Aleph_fm),
ground_repl_fm(omap_replacement_fm) }"
text‹This set has $8$ internalized formulas, corresponding to the total
count of previous replacement instances (apart from those $5$ in
\<^term>‹instances_ground_fms› and \<^term>‹instances_ground_notCH_fms›,
and \<^term>‹dc_abs_fm›).›
definition overhead where
"overhead ≡ instances1_fms ∪ instances_ground_fms"
definition overhead_notCH where
"overhead_notCH ≡ overhead ∪ instances2_fms ∪
instances3_fms ∪ instances_ground_notCH_fms"
definition overhead_CH where
"overhead_CH ≡ overhead_notCH ∪ { dc_abs_fm }"
text‹Hence, the ``overhead'' to create a proper extension of a ctm by forcing
consists of $7$ replacement instances. To force $\neg\CH$,
21 instances are need, and one further instance is required to
force $\CH$.›
lemma instances2_fms_type[TC] : "instances2_fms ⊆ formula"
unfolding instances2_fms_def replacement_instances2_defs
by (auto simp del: Lambda_in_M_fm_def)
lemma overhead_type: "overhead ⊆ formula"
using instances1_fms_type instances_ground_fms_type
unfolding overhead_def replacement_instances1_defs
by simp
lemma overhead_notCH_type: "overhead_notCH ⊆ formula"
using overhead_type
unfolding overhead_notCH_def rec_constr_abs_fm_def
rec_constr_fm_def instances_ground_notCH_fms_def
instances2_fms_def instances3_fms_def
by (auto simp: replacement_instances1_defs
replacement_instances2_defs simp del: Lambda_in_M_fm_def)
lemma overhead_CH_type: "overhead_CH ⊆ formula"
using overhead_notCH_type unfolding overhead_CH_def dc_abs_fm_def
by auto
locale M_ZF3_trans = M_ZF2_trans + M_ZF3
locale M_ZFC3 = M_ZFC2 + M_ZF3
locale M_ZFC3_trans = M_ZFC2_trans + M_ZF3_trans + M_ZFC3
locale M_ctm3 = M_ctm2 + M_ZF3_trans
locale M_ctm3_AC = M_ctm3 + M_ctm1_AC + M_ZFC3_trans
lemma M_satT_imp_M_ZF2: "(M ⊨ ZF) ⟹ M_ZF1(M)"
proof -
assume "M ⊨ ZF"
then
have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)"
"extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)"
unfolding ZF_def ZF_fin_def ZFC_fm_defs satT_def
using ZFC_fm_sats[of M] by simp_all
{
fix φ env
assume "φ ∈ formula" "env∈list(M)"
moreover from ‹M ⊨ ZF›
have "∀p∈formula. (M, [] ⊨ (ZF_separation_fm(p)))"
"∀p∈formula. (M, [] ⊨ (ZF_replacement_fm(p)))"
unfolding ZF_def ZF_schemes_def by auto
moreover from calculation
have "arity(φ) ≤ succ(length(env)) ⟹ separation(##M, λx. (M, Cons(x, env) ⊨ φ))"
"arity(φ) ≤ succ(succ(length(env))) ⟹ strong_replacement(##M,λx y. sats(M,φ,Cons(x,Cons(y, env))))"
using sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff
unfolding replacement_assm_def by simp_all
}
with fin
show "M_ZF1(M)"
by unfold_locales (simp_all add:replacement_assm_def ground_replacement_assm_def)
qed
lemma M_satT_imp_M_ZFC1:
shows "(M ⊨ ZFC) ⟶ M_ZFC1(M)"
proof -
have "(M ⊨ ZF) ∧ choice_ax(##M) ⟶ M_ZFC1(M)"
using M_satT_imp_M_ZF2[of M]
unfolding M_ZFC1_def M_ZC_basic_def M_ZF1_def M_AC_def
by auto
then
show ?thesis
unfolding ZFC_def by auto
qed
lemma M_satT_instances1_imp_M_ZF1:
assumes "(M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ instances1_fms })"
shows "M_ZF1(M)"
proof -
from assms
have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)"
"extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)"
unfolding ZF_fin_def Zermelo_fms_def ZFC_fm_defs satT_def
using ZFC_fm_sats[of M] by simp_all
moreover
{
fix φ env
from ‹M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ instances1_fms }›
have "∀p∈formula. (M, [] ⊨ (ZF_separation_fm(p)))"
unfolding Zermelo_fms_def ZF_def instances1_fms_def
by auto
moreover
assume "φ ∈ formula" "env∈list(M)"
ultimately
have "arity(φ) ≤ succ(length(env)) ⟹ separation(##M, λx. (M, Cons(x, env) ⊨ φ))"
using sats_ZF_separation_fm_iff by simp_all
}
moreover
{
fix φ env
assume "φ ∈ instances1_fms" "env∈list(M)"
moreover from this and ‹M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ instances1_fms }›
have "M, [] ⊨ ⋅Replacement(φ)⋅" by auto
ultimately
have "arity(φ) ≤ succ(succ(length(env))) ⟹ strong_replacement(##M,λx y. sats(M,φ,Cons(x,Cons(y, env))))"
using sats_ZF_replacement_fm_iff[of φ] instances1_fms_type
unfolding replacement_assm_def by auto
}
ultimately
show ?thesis
unfolding instances1_fms_def
by unfold_locales (simp_all add:replacement_assm_def ground_replacement_assm_def)
qed
theorem M_satT_imp_M_ZF_ground_trans:
assumes "Transset(M)" "M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ overhead}"
shows "M_ZF_ground_trans(M)"
proof -
from ‹M ⊨ ⋅Z⋅ ∪ _›
have "M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ instances1_fms }"
"M ⊨ {⋅Replacement(p)⋅ . p ∈ instances_ground_fms }"
unfolding overhead_def by auto
then
interpret M_ZF1 M
using M_satT_instances1_imp_M_ZF1
by simp
from ‹Transset(M)›
interpret M_ZF1_trans M
using M_satT_imp_M_ZF2
by unfold_locales
{
fix φ env
assume "φ ∈ instances_ground_fms" "env∈list(M)"
moreover from this and ‹M ⊨ {⋅Replacement(p)⋅ . p ∈ instances_ground_fms}›
have "M, [] ⊨ ⋅Replacement(φ)⋅" by auto
ultimately
have "arity(φ) ≤ succ(succ(length(env))) ⟹ strong_replacement(##M,λx y. sats(M,φ,Cons(x,Cons(y, env))))"
using sats_ZF_replacement_fm_iff[of φ] instances_ground_fms_type
unfolding replacement_assm_def by auto
}
then
show ?thesis
unfolding instances_ground_fms_def
by unfold_locales (simp_all add:replacement_assm_def)
qed
theorem M_satT_imp_M_ZF_ground_notCH_trans:
assumes
"Transset(M)"
"M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}"
shows "M_ZF_ground_notCH_trans(M)"
proof -
from assms
interpret M_ZF_ground_trans M
using M_satT_imp_M_ZF_ground_trans unfolding overhead_notCH_def by force
{
fix φ env
assume "φ ∈ instances_ground_notCH_fms" "env∈list(M)"
moreover from this and assms
have "M, [] ⊨ ⋅Replacement(φ)⋅"
unfolding overhead_notCH_def by auto
ultimately
have "arity(φ) ≤ succ(succ(length(env))) ⟹ strong_replacement(##M,λx y. sats(M,φ,Cons(x,Cons(y, env))))"
using sats_ZF_replacement_fm_iff[of φ] instances_ground_notCH_fms_type
unfolding replacement_assm_def by auto
}
then
show ?thesis
by unfold_locales (simp_all add:replacement_assm_def instances_ground_notCH_fms_def)
qed
theorem M_satT_imp_M_ZF_ground_CH_trans:
assumes
"Transset(M)"
"M ⊨ ⋅Z⋅ ∪ {⋅Replacement(p)⋅ . p ∈ overhead_CH }"
shows "M_ZF_ground_CH_trans(M)"
proof -
from assms
interpret M_ZF_ground_notCH_trans M
using M_satT_imp_M_ZF_ground_notCH_trans unfolding overhead_CH_def by auto
{
fix env
assume "env ∈ list(M)"
moreover from assms
have "M, [] ⊨ ⋅Replacement(dc_abs_fm)⋅"
unfolding overhead_CH_def by auto
ultimately
have "arity(dc_abs_fm) ≤ succ(succ(length(env)))
⟹ strong_replacement(##M,λx y. sats(M,dc_abs_fm,Cons(x,Cons(y, env))))"
using sats_ZF_replacement_fm_iff[of dc_abs_fm]
unfolding replacement_assm_def
by (auto simp:dc_abs_fm_def)
}
then
show ?thesis
by unfold_locales (simp_all add:replacement_assm_def)
qed
lemma (in M_Z_basic) M_satT_Zermelo_fms: "M ⊨ ⋅Z⋅"
using upair_ax Union_ax power_ax extensionality foundation_ax
infinity_ax separation_ax sats_ZF_separation_fm_iff
unfolding Zermelo_fms_def ZF_fin_def
by auto
lemma (in M_ZFC1) M_satT_ZC: "M ⊨ ZC"
using upair_ax Union_ax power_ax extensionality foundation_ax
infinity_ax separation_ax sats_ZF_separation_fm_iff choice_ax
unfolding ZC_def Zermelo_fms_def ZF_fin_def
by auto
locale M_ZF = M_Z_basic +
assumes
replacement_ax:"replacement_assm(M,env,φ)"
sublocale M_ZF ⊆ M_ZF3
using replacement_ax
by unfold_locales (simp_all add:ground_replacement_assm_def)
lemma M_satT_imp_M_ZF: " M ⊨ ZF ⟹ M_ZF(M)"
proof -
assume "M ⊨ ZF"
then
have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)"
"extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)"
unfolding ZF_def ZF_fin_def ZFC_fm_defs satT_def
using ZFC_fm_sats[of M] by simp_all
{
fix φ env
assume "φ ∈ formula" "env∈list(M)"
moreover from ‹M ⊨ ZF›
have "∀p∈formula. (M, [] ⊨ (ZF_separation_fm(p)))"
"∀p∈formula. (M, [] ⊨ (ZF_replacement_fm(p)))"
unfolding ZF_def ZF_schemes_def by auto
moreover from calculation
have "arity(φ) ≤ succ(length(env)) ⟹ separation(##M, λx. (M, Cons(x, env) ⊨ φ))"
"arity(φ) ≤ succ(succ(length(env))) ⟹ strong_replacement(##M,λx y. sats(M,φ,Cons(x,Cons(y, env))))"
using sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff
unfolding replacement_assm_def by simp_all
}
with fin
show "M_ZF(M)"
unfolding M_ZF_def M_Z_basic_def M_ZF_axioms_def replacement_assm_def by simp
qed
lemma (in M_ZF) M_satT_ZF: "M ⊨ ZF"
using upair_ax Union_ax power_ax extensionality foundation_ax
infinity_ax separation_ax sats_ZF_separation_fm_iff
replacement_ax sats_ZF_replacement_fm_iff
unfolding ZF_def ZF_schemes_def ZF_fin_def replacement_assm_def
by auto
lemma M_ZF_iff_M_satT: "M_ZF(M) ⟷ (M ⊨ ZF)"
using M_ZF.M_satT_ZF M_satT_imp_M_ZF
by auto
locale M_ZFC = M_ZF + M_ZC_basic
sublocale M_ZFC ⊆ M_ZFC3
by unfold_locales
lemma M_ZFC_iff_M_satT:
notes iff_trans[trans]
shows "M_ZFC(M) ⟷ (M ⊨ ZFC)"
proof -
have "M_ZFC(M) ⟷ (M ⊨ ZF) ∧ choice_ax(##M)"
using M_ZF_iff_M_satT
unfolding M_ZFC_def M_ZC_basic_def M_AC_def M_ZF_def by auto
also
have " … ⟷ M ⊨ ZFC"
unfolding ZFC_def by auto
ultimately
show ?thesis by simp
qed
lemma M_satT_imp_M_ZF3: "(M ⊨ ZF) ⟶ M_ZF3(M)"
proof
assume "M ⊨ ZF"
then
interpret M_ZF M
using M_satT_imp_M_ZF by simp
show "M_ZF3(M)"
by unfold_locales
qed
lemma M_satT_imp_M_ZFC3:
shows "(M ⊨ ZFC) ⟶ M_ZFC3(M)"
proof
assume "M ⊨ ZFC"
then
interpret M_ZFC M
using M_ZFC_iff_M_satT by simp
show "M_ZFC3(M)"
by unfold_locales
qed
lemma M_satT_overhead_imp_M_ZF3:
"(M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}) ⟶ M_ZFC3(M)"
proof
assume "M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}"
then
have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)" "choice_ax(##M)"
"extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)"
unfolding ZC_def ZF_fin_def Zermelo_fms_def ZFC_fm_defs satT_def
using ZFC_fm_sats[of M] by simp_all
moreover
{
fix φ env
from ‹M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}›
have "∀p∈formula. (M, [] ⊨ (ZF_separation_fm(p)))"
unfolding ZC_def Zermelo_fms_def ZF_def by auto
moreover
assume "φ ∈ formula" "env∈list(M)"
ultimately
have "arity(φ) ≤ succ(length(env)) ⟹ separation(##M, λx. (M, Cons(x, env) ⊨ φ))"
using sats_ZF_separation_fm_iff by simp_all
}
moreover
{
fix φ env
assume "φ ∈ overhead_notCH" "env∈list(M)"
moreover from this and ‹M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}›
have "M, [] ⊨ ⋅Replacement(φ)⋅" by auto
ultimately
have "arity(φ) ≤ succ(succ(length(env))) ⟹ strong_replacement(##M,λx y. sats(M,φ,Cons(x,Cons(y, env))))"
using sats_ZF_replacement_fm_iff[of φ] overhead_notCH_type
unfolding replacement_assm_def by auto
}
ultimately
show "M_ZFC3(M)"
unfolding overhead_def overhead_notCH_def instances1_fms_def
instances2_fms_def instances3_fms_def
by unfold_locales (simp_all add:replacement_assm_def ground_replacement_assm_def)
qed
end