Theory Internal_ZFC_Axioms
section‹The ZFC axioms, internalized›
theory Internal_ZFC_Axioms
imports
Fm_Definitions
begin
schematic_goal ZF_union_auto:
"Union_ax(##A) ⟷ (A, [] ⊨ ?zfunion)"
unfolding Union_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_union" from_schematic ZF_union_auto
notation ZF_union_fm (‹⋅Union Ax⋅›)
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" from_schematic ZF_power_auto
notation ZF_power_fm (‹⋅Powerset Ax⋅›)
schematic_goal ZF_pairing_auto:
"upair_ax(##A) ⟷ (A, [] ⊨ ?zfpair)"
unfolding upair_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_pairing" from_schematic ZF_pairing_auto
notation ZF_pairing_fm (‹⋅Pairing⋅›)
schematic_goal ZF_foundation_auto:
"foundation_ax(##A) ⟷ (A, [] ⊨ ?zffound)"
unfolding foundation_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_foundation" from_schematic ZF_foundation_auto
notation ZF_foundation_fm (‹⋅Foundation⋅›)
schematic_goal ZF_extensionality_auto:
"extensionality(##A) ⟷ (A, [] ⊨ ?zfext)"
unfolding extensionality_def
by ((rule sep_rules | simp)+)
synthesize "ZF_extensionality" from_schematic ZF_extensionality_auto
notation ZF_extensionality_fm (‹⋅Extensionality⋅›)
schematic_goal ZF_infinity_auto:
"infinity_ax(##A) ⟷ (A, [] ⊨ (?φ(i,j,h)))"
unfolding infinity_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_infinity" from_schematic ZF_infinity_auto
notation ZF_infinity_fm (‹⋅Infinity⋅›)
schematic_goal ZF_choice_auto:
"choice_ax(##A) ⟷ (A, [] ⊨ (?φ(i,j,h)))"
unfolding choice_ax_def
by ((rule sep_rules | simp)+)
synthesize "ZF_choice" from_schematic ZF_choice_auto
notation ZF_choice_fm (‹⋅AC⋅›)
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 ≡ {⋅Extensionality⋅, ⋅Foundation⋅, ⋅Pairing⋅,
⋅Union Ax⋅, ⋅Infinity⋅, ⋅Powerset Ax⋅}"
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) ≡ (⋅∀(⋅∃(⋅∀⋅⋅0 ∈ 1⋅ ↔ ⋅⋅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" (‹⋅Separation'(_')⋅›) 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, [] ⊨ ⋅Separation(φ)⋅)
⟷
(∀env∈list(M). arity(φ) ≤ 1 +⇩ω length(env) ⟶
separation(##M,λx. M, [x] @ env ⊨ φ))"
proof (intro iffI ballI impI)
let ?n="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) = pred(arity(φ))"
using list_split[OF ‹arity(φ) ≤ succ(_)› ‹env∈_›] by force
moreover from ‹φ∈_›
have "arity(φ) ≤ succ(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="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) = 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" 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" (‹⋅Replacement'(_')⋅›) 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, [] ⊨ ⋅Replacement(φ)⋅) ⟷ (∀env. replacement_assm(M,env,φ))"
unfolding replacement_assm_def
proof (intro iffI allI impI)
let ?n="pred(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) = pred(pred(arity(φ)))"
using list_split[OF ‹pred(_) ≤ _› ‹env∈_›] by auto
moreover
note ‹φ∈_›
moreover from this
have "arity(φ) ≤ succ(succ(pred(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="pred(pred(arity(φ)))"
assume asm:"∀env. φ ∈ formula ⟶
env ∈ list(M) ⟶ arity(φ) ≤ 2 +⇩ω length(env) ⟶
strong_replacement(##M, λx y. M, [x, y] @ env ⊨ φ)"
{
fix some
assume "some∈list(M)" "length(some) = pred(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_schemes :: "i" where
"ZF_schemes ≡ {⋅Separation(p)⋅ . p ∈ formula } ∪ {⋅Replacement(p)⋅ . p ∈ formula }"
lemma Un_subset_formula [TC]: "A⊆formula ∧ B⊆formula ⟹ A∪B ⊆ formula"
by auto
lemma ZF_schemes_subset_formula [TC]: "ZF_schemes ⊆ formula"
unfolding ZF_schemes_def by auto
lemma ZF_fin_subset_formula [TC]: "ZF_fin ⊆ formula"
unfolding ZF_fin_def by simp
definition
ZF :: "i" where
"ZF ≡ ZF_schemes ∪ ZF_fin"
lemma ZF_subset_formula [TC]: "ZF ⊆ formula"
unfolding ZF_def by auto
definition
ZFC :: "i" where
"ZFC ≡ ZF ∪ {⋅AC⋅}"
definition
ZF_minus_P :: "i" where
"ZF_minus_P ≡ ZF - { ⋅Powerset Ax⋅ }"
definition
Zermelo_fms :: "i" (‹⋅Z⋅›) where
"Zermelo_fms ≡ ZF_fin ∪ {⋅Separation(p)⋅ . p ∈ formula }"
definition
ZC :: "i" where
"ZC ≡ Zermelo_fms ∪ {⋅AC⋅}"
lemma ZFC_subset_formula: "ZFC ⊆ formula"
by (simp add:ZFC_def Un_subset_formula)
text‹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 satT_mono: "A ⊨ Φ ⟹ Ψ ⊆ Φ ⟹ A ⊨ Ψ"
by blast
lemma satT_Un_iff: "M ⊨ Φ ∪ Ψ ⟷ M ⊨ Φ ∧ M ⊨ Ψ" by auto
lemma sats_ZFC_iff_sats_ZF_AC:
"(N ⊨ ZFC) ⟷ (N ⊨ ZF) ∧ (N, [] ⊨ ⋅AC⋅)"
unfolding ZFC_def ZF_def by auto
lemma satT_ZF_imp_satT_Z: "M ⊨ ZF ⟹ M ⊨ ⋅Z⋅"
unfolding ZF_def ZF_schemes_def Zermelo_fms_def ZF_fin_def by auto
lemma satT_ZFC_imp_satT_ZC: "M ⊨ ZFC ⟹ M ⊨ ZC"
unfolding ZFC_def ZF_def ZF_schemes_def ZC_def Zermelo_fms_def by auto
lemma satT_Z_ZF_replacement_imp_satT_ZF: "N ⊨ ⋅Z⋅ ⟹ N ⊨ {⋅Replacement(x)⋅ . x ∈ formula} ⟹ N ⊨ ZF"
unfolding ZF_def ZF_schemes_def Zermelo_fms_def ZF_fin_def by auto
lemma satT_ZC_ZF_replacement_imp_satT_ZFC: "N ⊨ ZC ⟹ N ⊨ {⋅Replacement(x)⋅ . x ∈ formula} ⟹ N ⊨ ZFC"
unfolding ZFC_def ZF_def ZF_schemes_def ZC_def Zermelo_fms_def by auto
lemma ground_repl_fm_sub_ZF: "{⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ formula} ⊆ ZF"
unfolding ZF_def ZF_schemes_def by auto
lemma ZF_replacement_fms_sub_ZFC: "{⋅Replacement(φ)⋅ . φ ∈ formula} ⊆ ZFC"
unfolding ZFC_def ZF_def ZF_schemes_def by auto
lemma ground_repl_fm_sub_ZFC: "{⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ formula} ⊆ ZFC"
unfolding ZFC_def ZF_def ZF_schemes_def by auto
lemma ZF_replacement_ground_repl_fm_type: "{⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ formula} ⊆ formula"
by auto
end