section‹The ZFC axioms, internalized›
theory Internal_ZFC_Axioms
imports
Forcing_Data
begin
schematic_goal ZF_union_auto:
"Union_ax(##A) ⟷ (A, [] ⊨ ?zfunion)"
unfolding Union_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_union_fm" from_schematic ZF_union_auto
schematic_goal ZF_power_auto:
"power_ax(##A) ⟷ (A, [] ⊨ ?zfpow)"
unfolding power_ax_def powerset_def subset_def
by ((rule sep_rules | simp)+)
synthesize "ZF_power_fm" from_schematic ZF_power_auto
schematic_goal ZF_pairing_auto:
"upair_ax(##A) ⟷ (A, [] ⊨ ?zfpair)"
unfolding upair_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_pairing_fm" from_schematic ZF_pairing_auto
schematic_goal ZF_foundation_auto:
"foundation_ax(##A) ⟷ (A, [] ⊨ ?zfpow)"
unfolding foundation_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_foundation_fm" from_schematic ZF_foundation_auto
schematic_goal ZF_extensionality_auto:
"extensionality(##A) ⟷ (A, [] ⊨ ?zfpow)"
unfolding extensionality_def
by ((rule sep_rules | simp)+)
synthesize "ZF_extensionality_fm" from_schematic ZF_extensionality_auto
schematic_goal ZF_infinity_auto:
"infinity_ax(##A) ⟷ (A, [] ⊨ (?φ(i,j,h)))"
unfolding infinity_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_infinity_fm" from_schematic ZF_infinity_auto
schematic_goal ZF_choice_auto:
"choice_ax(##A) ⟷ (A, [] ⊨ (?φ(i,j,h)))"
unfolding choice_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_choice_fm" from_schematic ZF_choice_auto
syntax
"_choice" :: "i" ("AC")
translations
"AC" ⇀ "CONST ZF_choice_fm"
lemmas ZFC_fm_defs = ZF_extensionality_fm_def ZF_foundation_fm_def ZF_pairing_fm_def
ZF_union_fm_def ZF_infinity_fm_def ZF_power_fm_def ZF_choice_fm_def
lemmas ZFC_fm_sats = ZF_extensionality_auto ZF_foundation_auto ZF_pairing_auto
ZF_union_auto ZF_infinity_auto ZF_power_auto ZF_choice_auto
definition
ZF_fin :: "i" where
"ZF_fin ≡ { ZF_extensionality_fm, ZF_foundation_fm, ZF_pairing_fm,
ZF_union_fm, ZF_infinity_fm, ZF_power_fm }"
definition
ZFC_fin :: "i" where
"ZFC_fin ≡ ZF_fin ∪ {ZF_choice_fm}"
lemma ZFC_fin_type : "ZFC_fin ⊆ formula"
unfolding ZFC_fin_def ZF_fin_def ZFC_fm_defs by (auto)
subsection‹The Axiom of Separation, internalized›
lemma iterates_Forall_type [TC]:
"⟦ n ∈ nat; p ∈ formula ⟧ ⟹ Forall^n(p) ∈ formula"
by (induct set:nat, auto)
lemma last_init_eq :
assumes "l ∈ list(A)" "length(l) = succ(n)"
shows "∃ a∈A. ∃l'∈list(A). l = l'@[a]"
proof-
from ‹l∈_› ‹length(_) = _›
have "rev(l) ∈ list(A)" "length(rev(l)) = succ(n)"
by simp_all
then
obtain a l' where "a∈A" "l'∈list(A)" "rev(l) = Cons(a,l')"
by (cases;simp)
then
have "l = rev(l') @ [a]" "rev(l') ∈ list(A)"
using rev_rev_ident[OF ‹l∈_›] by auto
with ‹a∈_›
show ?thesis by blast
qed
lemma take_drop_eq :
assumes "l∈list(M)"
shows "⋀ n . n < succ(length(l)) ⟹ l = take(n,l) @ drop(n,l)"
using ‹l∈list(M)›
proof induct
case Nil
then show ?case by auto
next
case (Cons a l)
then show ?case
proof -
{
fix i
assume "i<succ(succ(length(l)))"
with ‹l∈list(M)›
consider (lt) "i = 0" | (eq) "∃k∈nat. i = succ(k) ∧ k < succ(length(l))"
using ‹l∈list(M)› le_natI nat_imp_quasinat
by (cases rule:nat_cases[of i];auto)
then
have "take(i,Cons(a,l)) @ drop(i,Cons(a,l)) = Cons(a,l)"
using Cons
by (cases;auto)
}
then show ?thesis using Cons by auto
qed
qed
lemma list_split :
assumes "n ≤ succ(length(rest))" "rest ∈ list(M)"
shows "∃re∈list(M). ∃st∈list(M). rest = re @ st ∧ length(re) = pred(n)"
proof -
from assms
have "pred(n) ≤ length(rest)"
using pred_mono[OF _ ‹n≤_›] pred_succ_eq by auto
with ‹rest∈_›
have "pred(n)∈nat" "rest = take(pred(n),rest) @ drop(pred(n),rest)" (is "_ = ?re @ ?st")
using take_drop_eq[OF ‹rest∈_›] le_natI by auto
then
have "length(?re) = pred(n)" "?re∈list(M)" "?st∈list(M)"
using length_take[rule_format,OF _ ‹pred(n)∈_›] ‹pred(n) ≤ _› ‹rest∈_›
unfolding min_def
by auto
then
show ?thesis
using rev_bexI[of _ _ "λ re. ∃st∈list(M). rest = re @ st ∧ length(re) = pred(n)"]
‹length(?re) = _› ‹rest = _›
by auto
qed
lemma sats_nForall:
assumes
"φ ∈ formula"
shows
"n∈nat ⟹ ms ∈ list(M) ⟹
M, ms ⊨ (Forall^n(φ)) ⟷
(∀rest ∈ list(M). length(rest) = n ⟶ M, rest @ ms ⊨ φ)"
proof (induct n arbitrary:ms set:nat)
case 0
with assms
show ?case by simp
next
case (succ n)
have "(∀rest∈list(M). length(rest) = succ(n) ⟶ P(rest,n)) ⟷
(∀t∈M. ∀res∈list(M). length(res) = n ⟶ P(res @ [t],n))"
if "n∈nat" for n P
using that last_init_eq by force
from this[of _ "λrest _. (M, rest @ ms ⊨ φ)"] ‹n∈nat›
have "(∀rest∈list(M). length(rest) = succ(n) ⟶ M, rest @ ms ⊨ φ) ⟷
(∀t∈M. ∀res∈list(M). length(res) = n ⟶ M, (res @ [t]) @ ms ⊨ φ)"
by simp
with assms succ(1,3) succ(2)[of "Cons(_,ms)"]
show ?case
using arity_sats_iff[of φ _ M "Cons(_, ms @ _)"] app_assoc
by (simp)
qed
definition
sep_body_fm :: "i ⇒ i" where
"sep_body_fm(p) ≡ Forall(Exists(Forall(
Iff(Member(0,1),And(Member(0,2),
incr_bv1^2(p))))))"
lemma sep_body_fm_type [TC]: "p ∈ formula ⟹ sep_body_fm(p) ∈ formula"
by (simp add: sep_body_fm_def)
lemma sats_sep_body_fm:
assumes
"φ ∈ formula" "ms∈list(M)" "rest∈list(M)"
shows
"M, rest @ ms ⊨ sep_body_fm(φ) ⟷
separation(##M,λx. M, [x] @ rest @ ms ⊨ φ)"
using assms formula_add_params1[of _ 2 _ _ "[_,_]" ]
unfolding sep_body_fm_def separation_def by simp
definition
ZF_separation_fm :: "i ⇒ i" where
"ZF_separation_fm(p) ≡ Forall^(pred(arity(p)))(sep_body_fm(p))"
lemma ZF_separation_fm_type [TC]: "p ∈ formula ⟹ ZF_separation_fm(p) ∈ formula"
by (simp add: ZF_separation_fm_def)
lemma sats_ZF_separation_fm_iff:
assumes
"φ∈formula"
shows
"(M, [] ⊨ (ZF_separation_fm(φ)))
⟷
(∀env∈list(M). arity(φ) ≤ 1 #+ length(env) ⟶
separation(##M,λx. M, [x] @ env ⊨ φ))"
proof (intro iffI ballI impI)
let ?n="Arith.pred(arity(φ))"
fix env
assume "M, [] ⊨ ZF_separation_fm(φ)"
assume "arity(φ) ≤ 1 #+ length(env)" "env∈list(M)"
moreover from this
have "arity(φ) ≤ succ(length(env))" by simp
then
obtain some rest where "some∈list(M)" "rest∈list(M)"
"env = some @ rest" "length(some) = Arith.pred(arity(φ))"
using list_split[OF ‹arity(φ) ≤ succ(_)› ‹env∈_›] by force
moreover from ‹φ∈_›
have "arity(φ) ≤ succ(Arith.pred(arity(φ)))"
using succpred_leI by simp
moreover
note assms
moreover
assume "M, [] ⊨ ZF_separation_fm(φ)"
moreover from calculation
have "M, some ⊨ sep_body_fm(φ)"
using sats_nForall[of "sep_body_fm(φ)" ?n]
unfolding ZF_separation_fm_def by simp
ultimately
show "separation(##M, λx. M, [x] @ env ⊨ φ)"
unfolding ZF_separation_fm_def
using sats_sep_body_fm[of φ "[]" M some]
arity_sats_iff[of φ rest M "[_] @ some"]
separation_cong[of "##M" "λx. M, Cons(x, some @ rest) ⊨ φ" _ ]
by simp
next
let ?n="Arith.pred(arity(φ))"
assume asm:"∀env∈list(M). arity(φ) ≤ 1 #+ length(env) ⟶
separation(##M, λx. M, [x] @ env ⊨ φ)"
{
fix some
assume "some∈list(M)" "length(some) = Arith.pred(arity(φ))"
moreover
note ‹φ∈_›
moreover from calculation
have "arity(φ) ≤ 1 #+ length(some)"
using le_trans[OF succpred_leI] succpred_leI by simp
moreover from calculation and asm
have "separation(##M, λx. M, [x] @ some ⊨ φ)" by blast
ultimately
have "M, some ⊨ sep_body_fm(φ)"
using sats_sep_body_fm[of φ "[]" M some]
arity_sats_iff[of φ _ M "[_,_] @ some"]
strong_replacement_cong[of "##M" "λx y. M, Cons(x, Cons(y, some @ _)) ⊨ φ" _ ]
by simp
}
with ‹φ∈_›
show "M, [] ⊨ ZF_separation_fm(φ)"
using sats_nForall[of "sep_body_fm(φ)" ?n]
unfolding ZF_separation_fm_def
by simp
qed
subsection‹The Axiom of Replacement, internalized›
schematic_goal sats_univalent_fm_auto:
assumes
Q_iff_sats:"⋀x y z. x ∈ A ⟹ y ∈ A ⟹ z∈A ⟹
Q(x,z) ⟷ (A,Cons(z,Cons(y,Cons(x,env))) ⊨ Q1_fm)"
"⋀x y z. x ∈ A ⟹ y ∈ A ⟹ z∈A ⟹
Q(x,y) ⟷ (A,Cons(z,Cons(y,Cons(x,env))) ⊨ Q2_fm)"
and
asms: "nth(i,env) = B" "i ∈ nat" "env ∈ list(A)"
shows
"univalent(##A,B,Q) ⟷ A,env ⊨ ?ufm(i)"
unfolding univalent_def
by (insert asms; (rule sep_rules Q_iff_sats | simp)+)
synthesize_notc "univalent_fm" from_schematic sats_univalent_fm_auto
lemma univalent_fm_type [TC]: "q1∈ formula ⟹ q2∈formula ⟹ i∈nat ⟹
univalent_fm(q2,q1,i) ∈formula"
by (simp add:univalent_fm_def)
lemma sats_univalent_fm :
assumes
Q_iff_sats:"⋀x y z. x ∈ A ⟹ y ∈ A ⟹ z∈A ⟹
Q(x,z) ⟷ (A,Cons(z,Cons(y,Cons(x,env))) ⊨ Q1_fm)"
"⋀x y z. x ∈ A ⟹ y ∈ A ⟹ z∈A ⟹
Q(x,y) ⟷ (A,Cons(z,Cons(y,Cons(x,env))) ⊨ Q2_fm)"
and
asms: "nth(i,env) = B" "i ∈ nat" "env ∈ list(A)"
shows
"A,env ⊨ univalent_fm(Q1_fm,Q2_fm,i) ⟷ univalent(##A,B,Q)"
unfolding univalent_fm_def using asms sats_univalent_fm_auto[OF Q_iff_sats] by simp
definition
swap_vars :: "i⇒i" where
"swap_vars(φ) ≡
Exists(Exists(And(Equal(0,3),And(Equal(1,2),iterates(λp. incr_bv(p)`2 , 2, φ)))))"
lemma swap_vars_type[TC] :
"φ∈formula ⟹ swap_vars(φ) ∈formula"
unfolding swap_vars_def by simp
lemma sats_swap_vars :
"[x,y] @ env ∈ list(M) ⟹ φ∈formula ⟹
M, [x,y] @ env ⊨ swap_vars(φ)⟷ M,[y,x] @ env ⊨ φ"
unfolding swap_vars_def
using sats_incr_bv_iff [of _ _ M _ "[y,x]"] by simp
definition
univalent_Q1 :: "i ⇒ i" where
"univalent_Q1(φ) ≡ incr_bv1(swap_vars(φ))"
definition
univalent_Q2 :: "i ⇒ i" where
"univalent_Q2(φ) ≡ incr_bv(swap_vars(φ))`0"
lemma univalent_Qs_type [TC]:
assumes "φ∈formula"
shows "univalent_Q1(φ) ∈ formula" "univalent_Q2(φ) ∈ formula"
unfolding univalent_Q1_def univalent_Q2_def using assms by simp_all
lemma sats_univalent_fm_assm:
assumes
"x ∈ A" "y ∈ A" "z∈A" "env∈ list(A)" "φ ∈ formula"
shows
"(A, ([x,z] @ env) ⊨ φ) ⟷ (A, Cons(z,Cons(y,Cons(x,env))) ⊨ (univalent_Q1(φ)))"
"(A, ([x,y] @ env) ⊨ φ) ⟷ (A, Cons(z,Cons(y,Cons(x,env))) ⊨ (univalent_Q2(φ)))"
unfolding univalent_Q1_def univalent_Q2_def
using
sats_incr_bv_iff[of _ _ A _ "[]"]
sats_incr_bv1_iff[of _ "Cons(x,env)" A z y]
sats_swap_vars assms
by simp_all
definition
rep_body_fm :: "i ⇒ i" where
"rep_body_fm(p) ≡ Forall(Implies(
univalent_fm(univalent_Q1(incr_bv(p)`2),univalent_Q2(incr_bv(p)`2),0),
Exists(Forall(
Iff(Member(0,1),Exists(And(Member(0,3),incr_bv(incr_bv(p)`2)`2)))))))"
lemma rep_body_fm_type [TC]: "p ∈ formula ⟹ rep_body_fm(p) ∈ formula"
by (simp add: rep_body_fm_def)
lemmas ZF_replacement_simps = formula_add_params1[of φ 2 _ M "[_,_]" ]
sats_incr_bv_iff[of _ _ M _ "[]"]
sats_incr_bv_iff[of _ _ M _ "[_,_]"]
sats_incr_bv1_iff[of _ _ M] sats_swap_vars for φ M
lemma sats_rep_body_fm:
assumes
"φ ∈ formula" "ms∈list(M)" "rest∈list(M)"
shows
"M, rest @ ms ⊨ rep_body_fm(φ) ⟷
strong_replacement(##M,λx y. M, [x,y] @ rest @ ms ⊨ φ)"
using assms ZF_replacement_simps
unfolding rep_body_fm_def strong_replacement_def univalent_def
unfolding univalent_fm_def univalent_Q1_def univalent_Q2_def
by simp
definition
ZF_replacement_fm :: "i ⇒ i" where
"ZF_replacement_fm(p) ≡ Forall^(pred(pred(arity(p))))(rep_body_fm(p))"
lemma ZF_replacement_fm_type [TC]: "p ∈ formula ⟹ ZF_replacement_fm(p) ∈ formula"
by (simp add: ZF_replacement_fm_def)
lemma sats_ZF_replacement_fm_iff:
assumes
"φ∈formula"
shows
"(M, [] ⊨ (ZF_replacement_fm(φ)))
⟷
(∀env∈list(M). arity(φ) ≤ 2 #+ length(env) ⟶
strong_replacement(##M,λx y. M,[x,y] @ env ⊨ φ))"
proof (intro iffI ballI impI)
let ?n="Arith.pred(Arith.pred(arity(φ)))"
fix env
assume "M, [] ⊨ ZF_replacement_fm(φ)" "arity(φ) ≤ 2 #+ length(env)" "env∈list(M)"
moreover from this
have "arity(φ) ≤ succ(succ(length(env)))" by (simp)
moreover from calculation
have "pred(arity(φ)) ≤ succ(length(env))"
using pred_mono[OF _ ‹arity(φ)≤succ(_)›] pred_succ_eq by simp
moreover from calculation
obtain some rest where "some∈list(M)" "rest∈list(M)"
"env = some @ rest" "length(some) = Arith.pred(Arith.pred(arity(φ)))"
using list_split[OF ‹pred(_) ≤ _› ‹env∈_›] by auto
moreover
note ‹φ∈_›
moreover from this
have "arity(φ) ≤ succ(succ(Arith.pred(Arith.pred(arity(φ)))))"
using le_trans[OF succpred_leI] succpred_leI by simp
moreover from calculation
have "M, some ⊨ rep_body_fm(φ)"
using sats_nForall[of "rep_body_fm(φ)" ?n]
unfolding ZF_replacement_fm_def
by simp
ultimately
show "strong_replacement(##M, λx y. M, [x, y] @ env ⊨ φ)"
using sats_rep_body_fm[of φ "[]" M some]
arity_sats_iff[of φ rest M "[_,_] @ some"]
strong_replacement_cong[of "##M" "λx y. M, Cons(x, Cons(y, some @ rest)) ⊨ φ" _ ]
by simp
next
let ?n="Arith.pred(Arith.pred(arity(φ)))"
assume asm:"∀env∈list(M). arity(φ) ≤ 2 #+ length(env) ⟶
strong_replacement(##M, λx y. M, [x, y] @ env ⊨ φ)"
{
fix some
assume "some∈list(M)" "length(some) = Arith.pred(Arith.pred(arity(φ)))"
moreover
note ‹φ∈_›
moreover from calculation
have "arity(φ) ≤ 2 #+ length(some)"
using le_trans[OF succpred_leI] succpred_leI by simp
moreover from calculation and asm
have "strong_replacement(##M, λx y. M, [x, y] @ some ⊨ φ)" by blast
ultimately
have "M, some ⊨ rep_body_fm(φ)"
using sats_rep_body_fm[of φ "[]" M some]
arity_sats_iff[of φ _ M "[_,_] @ some"]
strong_replacement_cong[of "##M" "λx y. M, Cons(x, Cons(y, some @ _)) ⊨ φ" _ ]
by simp
}
with ‹φ∈_›
show "M, [] ⊨ ZF_replacement_fm(φ)"
using sats_nForall[of "rep_body_fm(φ)" ?n]
unfolding ZF_replacement_fm_def
by simp
qed
definition
ZF_inf :: "i" where
"ZF_inf ≡ {ZF_separation_fm(p) . p ∈ formula } ∪ {ZF_replacement_fm(p) . p ∈ formula }"
lemma Un_subset_formula: "A⊆formula ∧ B⊆formula ⟹ A∪B ⊆ formula"
by auto
lemma ZF_inf_subset_formula : "ZF_inf ⊆ formula"
unfolding ZF_inf_def by auto
definition
ZFC :: "i" where
"ZFC ≡ ZF_inf ∪ ZFC_fin"
definition
ZF :: "i" where
"ZF ≡ ZF_inf ∪ ZF_fin"
definition
ZF_minus_P :: "i" where
"ZF_minus_P ≡ ZF - { ZF_power_fm }"
lemma ZFC_subset_formula: "ZFC ⊆ formula"
by (simp add:ZFC_def Un_subset_formula ZF_inf_subset_formula ZFC_fin_type)
txt‹Satisfaction of a set of sentences›
definition
satT :: "[i,i] ⇒ o" ("_ ⊨ _" [36,36] 60) where
"A ⊨ Φ ≡ ∀φ∈Φ. (A,[] ⊨ φ)"
lemma satTI [intro!]:
assumes "⋀φ. φ∈Φ ⟹ A,[] ⊨ φ"
shows "A ⊨ Φ"
using assms unfolding satT_def by simp
lemma satTD [dest] :"A ⊨ Φ ⟹ φ∈Φ ⟹ A,[] ⊨ φ"
unfolding satT_def by simp
lemma sats_ZFC_iff_sats_ZF_AC:
"(N ⊨ ZFC) ⟷ (N ⊨ ZF) ∧ (N, [] ⊨ AC)"
unfolding ZFC_def ZFC_fin_def ZF_def by auto
lemma M_ZF_iff_M_satT: "M_ZF(M) ⟷ (M ⊨ ZF)"
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_inf_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 by simp_all
}
with fin
show "M_ZF(M)"
unfolding M_ZF_def by simp
next
assume ‹M_ZF(M)›
then
have "M ⊨ ZF_fin"
unfolding M_ZF_def ZF_fin_def ZFC_fm_defs satT_def
using ZFC_fm_sats[of M] by blast
moreover from ‹M_ZF(M)›
have "∀p∈formula. (M, [] ⊨ (ZF_separation_fm(p)))"
"∀p∈formula. (M, [] ⊨ (ZF_replacement_fm(p)))"
unfolding M_ZF_def using sats_ZF_separation_fm_iff
sats_ZF_replacement_fm_iff by simp_all
ultimately
show "M ⊨ ZF"
unfolding ZF_def ZF_inf_def by blast
qed
end