File CoMoZFC.ZFC
The universe of our set (theory).
We need some Relation "is element of"
Axiom of extensionality
Existence of an empty set
Parameter empty_set : S.
Definition empty_property s :=
∀ x,
¬ elem x s.
Axiom empty :
empty_property empty_set.
Definition empty_property s :=
∀ x,
¬ elem x s.
Axiom empty :
empty_property empty_set.
Thanks to the empty_set, our domain S cannot be empty.
Axiom of regularity/foundation
Axiom of union
Parameter union_set : S → S.
Definition union_property a s :=
∀ c,
elem c s ↔
∃ d,
elem d a ∧
elem c d.
Axiom union :
∀ a,
union_property a (union_set a).
Definition union_property a s :=
∀ c,
elem c s ↔
∃ d,
elem d a ∧
elem c d.
Axiom union :
∀ a,
union_property a (union_set a).
Axiom schema of replacement
Axiom replacement :
∀ (F : S → S → Prop),
(
∀ x y z,
F x y →
F x z →
y = z
) →
∀ a,
{ b : S |
∀ c,
elem c b ↔
∃ d,
elem d a ∧
F d c}.
∀ (F : S → S → Prop),
(
∀ x y z,
F x y →
F x z →
y = z
) →
∀ a,
{ b : S |
∀ c,
elem c b ↔
∃ d,
elem d a ∧
F d c}.
"Axiom" of specification and the existence of subsets.
Definition sub_set_sig (P : S → Prop) (a : S) : {b : S | ∀ c, elem c b ↔ ∃ d, elem d a ∧ P d ∧ d = c}.
Proof.
apply replacement.
intros x y z [H1 H2] [H3 H4]; subst; reflexivity.
Defined.
Definition sub_set P a := proj1_sig (sub_set_sig P a).
Definition specification_property P a s :=
∀ c,
elem c s ↔
(
elem c a ∧
P c
).
Theorem specification :
∀ P a,
specification_property P a (sub_set P a).
Proof.
intros P a c;
split;
intros H1;
pose proof (proj2_sig (sub_set_sig P a)) as H2;
simpl in H2;
destruct (H2 c) as [H3 ?];
[destruct (H3 H1) | destruct H1];
firstorder;
subst;
firstorder.
Qed.
Definition intersection a := sub_set (fun b ⇒ ∀ c, elem c a → elem b c) (union_set a).
Axiom of power set
Parameter pot_set : S → S.
Definition pot_property a s :=
∀ b,
elem b s ↔
∀ c,
elem c b →
elem c a.
Axiom pot :
∀ a,
pot_property a (pot_set a).
Definition pot_property a s :=
∀ b,
elem b s ↔
∀ c,
elem c b →
elem c a.
Axiom pot :
∀ a,
pot_property a (pot_set a).
"Axiom" of pairing
Lemma pot_set_neq_empty_set : empty_set ≠ pot_set empty_set.
Proof.
intros H1.
pose proof (pot empty_set) as H2.
pose proof empty as H3.
rewrite H1 in H3.
specialize (H3 empty_set).
apply H3;
apply H2;
intros c H4;
exact H4.
Qed.
Definition pair_set_sig (a b : S) :
{p : S |
∀ c,
elem c p ↔
∃ d,
let special_pair := pot_set (pot_set empty_set) in
elem d special_pair ∧
(
(d = empty_set ∧ c = a) ∨
(d = pot_set empty_set ∧ c = b))
}.
Proof.
apply replacement.
intros x y z H1 H2.
destruct H1 as [H3|H3], H2 as [H4|H4];
destruct H3 as [H5 H6], H4 as [H7 H8];
subst;
firstorder;
exfalso;
try apply pot_set_neq_empty_set;
easy.
Defined.
Definition pair_set a b := proj1_sig (pair_set_sig a b).
Definition pair_property a b s :=
∀ d,
elem d s ↔
(
d = a ∨
d = b
).
Theorem pair :
∀ a b,
pair_property a b (pair_set a b).
Proof.
intros a b d; split; intros H1;
pose proof (proj2_sig (pair_set_sig a b)) as H2;
destruct (H2 d) as [H3 H4]; clear H2.
-
specialize (H3 H1).
destruct H3 as [e H5].
destruct H5; firstorder.
-
apply H4; clear H4 H3.
destruct H1; subst;
[∃ empty_set | ∃ (pot_set empty_set)];
split.
+
apply pot; intros; exfalso;
eapply empty; eassumption.
+
left; split; reflexivity.
+
apply pot; intros; assumption.
+
right; split; reflexivity.
Qed.
Theorem pair_uniqueness :
∀ a b c,
pair_property a b c →
c = pair_set a b.
Proof.
intros a b c H1;
red in H1.
apply extensionality;
intros z; split; intros H2.
-
destruct (H1 z) as [H3 H4].
destruct (H3 H2) as [H5|H5]; subst; apply pair; [left|right]; reflexivity.
-
destruct (pair a b z) as [H3 H4];
destruct (H3 H2) as [H5|H5]; subst; apply H1; [left|right]; reflexivity.
Qed.
Definition single_set a := pair_set a a.
Definition union2_set a b := union_set (pair_set a b).
Axiom of infinity
Parameter infinity_set : S.
Definition infinity_property s :=
elem empty_set s ∧
∀ x,
elem x s →
elem (union2_set x (single_set x)) s.
Axiom infinity : infinity_property infinity_set.
Definition naturals :=
sub_set
(
fun s ⇒
s = empty_set ∨
∃ s',
s = union2_set s' (single_set s')
)
infinity_set.
Definition infinity_property s :=
elem empty_set s ∧
∀ x,
elem x s →
elem (union2_set x (single_set x)) s.
Axiom infinity : infinity_property infinity_set.
Definition naturals :=
sub_set
(
fun s ⇒
s = empty_set ∨
∃ s',
s = union2_set s' (single_set s')
)
infinity_set.
Axiom of choice