Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka
• Version: 16 May 2015
• Author: Dominik Kirst, Saarland University
• This file covers Section 4 of the paper
• Acknowlegments: Axiomatisation based on course "Computational Logic II" by Gert Smolka in winter term 2014/2015

Global Set Implicit Arguments.
Global Unset Strict Implicit.

Require Export Setoid.

# Axiomatized Set Theory

We assume a type of sets and a membership relation between sets

Axiom set: Type.
Axiom elem: set -> set -> Prop.

Implicit Types x y z: set.
Implicit Types p q: set -> Prop.

Notation "x 'el' y" := (elem x y) (at level 70).

Definition class x y := elem y x.
Definition inhab x := exists y, y el x.

Extensionality

Axiom Ext: forall x y, (forall z, z el x <-> z el y) -> x = y.

Subset ordering

Definition sub x y := forall z, z el x -> z el y.
Definition subcc p q := forall z, p z -> q z.
Definition subsc x p := forall z, z el x -> p z.
Definition subcs p x := forall z, p z -> z el x.

Hint Unfold sub subcc subsc subcs.

Notation "x '<<=' y" := (subcc x y) (at level 70).
Notation "x '<<=' y" := (subsc x y) (at level 70).
Notation "x '<<=' y" := (subcs x y) (at level 70).
Notation "x '<<=' y" := (sub x y) (at level 70).
Notation "x '<<' y" := (sub x y /\ x <> y) (at level 70).

Lemma sub_refl x:
x <<= x.
Proof.
unfold sub. auto.
Qed.

Hint Resolve sub_refl.

Lemma sub_trans x y z:
x <<= y -> y <<= z -> x <<= z.
Proof.
unfold sub. auto.
Qed.

Lemma sub_anti x y:
x <<= y -> y <<= x -> x = y.
Proof.
intros A B; apply Ext.
split; intros C.
- apply A, C.
- apply B, C.
Qed.

Definition least x p :=
p x /\ forall y, p y -> x <<= y.

Definition greatest x p :=
p x /\ forall y, p y -> y <<= x.

Fact least_unique x y p:
least x p -> least y p -> x = y.
Proof.
intros [A B] [C D]. apply Ext.
intros z. split; intros E.
- now apply B.
- now apply D.
Qed.

Fact greatest_unique x y p:
greatest x p -> greatest y p -> x = y.
Proof.
intros [A B] [C D]. apply Ext.
intros z. split; intros E.
- now apply (D x).
- now apply (B y).
Qed.

Realizable classes

Definition realizes x p :=
forall z, z el x <-> p z.

Definition realizable p :=
exists x, realizes x p.

Lemma Russell:
~ realizable (fun z => ~ z el z).
Proof.
intros [x A]. specialize (A x). simpl in *. tauto.
Qed.

Lemma unrealizable_new_el p:
(forall x, subsc x p -> exists y, p y /\ ~ y el x) -> ~ realizable p.
Proof.
intros A [x B].
destruct (A x) as [y [C D]].
- intros y D. apply B, D.
- apply D, B, C.
Qed.

Unordered Pairs

Axiom upair: set -> set -> set.
Axiom Upair: forall x y z, z el upair x y <-> z = x \/ z = y.

Lemma upair_inl x y:
x el upair x y.
Proof.
apply Upair; auto.
Qed.

Lemma upair_inr x y:
y el upair x y.
Proof.
apply Upair; auto.
Qed.

Hint Resolve upair_inl upair_inr.

Lemma upair_injective x y a b:
upair x y = upair a b -> x=a /\ y=b \/ x=b /\ y=a.
Proof.
intros A.
assert (B: x=a \/ x=b).
{ apply Upair. rewrite <- A; auto. }
assert (C: y=a \/ y=b).
{ apply Upair. rewrite <- A; auto. }
assert (D: a=x \/ a=y).
{ apply Upair. rewrite A; auto. }
assert (E: b=x \/ b=y).
{ apply Upair. rewrite A; auto. }
intuition.
Qed.

Singletons

Definition sing x: set := upair x x.

Lemma sing_injective x y:
sing x = sing y -> x=y.
Proof.
intros A.
apply upair_injective in A. intuition.
Qed.

Lemma el_sing x y:
x el sing y <-> x=y.
Proof.
unfold sing. rewrite Upair. tauto.
Qed.

Lemma in_sing x y:
x=y -> x el sing y.
Proof.
now apply el_sing.
Qed.

Hint Resolve in_sing.

Hint Extern 4 =>
match goal with
| [ H : ?x el sing _ |- _ ] => apply el_sing in H; subst x
end.

Lemma eq_sing x y:
x = sing y -> y el x.
Proof.
intros A. rewrite A. auto.
Qed.

Lemma upair_sing x y z:
upair x y = sing z -> x = y /\ x = z.
Proof.
intros A. apply upair_injective in A.
intuition; congruence.
Qed.

Lemma sub_sing x y:
x <<= sing y -> inhab x -> x = sing y.
Proof.
intros A B. apply Ext. intros z. split.
- auto.
- intros C. apply el_sing in C. subst z.
destruct B as [z B]. assert (C:= B).
apply A in C. apply el_sing in C. congruence.
Qed.

Union

Axiom union: set -> set.
Axiom Union: forall x z, z el union x <-> exists y, y el x /\ z el y.

Lemma union_el_incl x y:
y el x -> y <<= union x.
Proof.
intros A z B. apply Union. eauto.
Qed.

Lemma union_incl u x:
union x <<= u <-> forall y, y el x -> y <<= u.
Proof.
split.
- intros A y B z C. apply A, Union. eauto.
- intros A z B. apply Union in B as [y [B C]].
now apply (A y).
Qed.

Lemma union_lub u x:
union x = u <->
(forall z, z el x -> z <<= u) /\
(forall v, (forall z, z el x -> z <<= v) -> u <<= v).
Proof.
split.
- intros A. subst u. split.
+ intros y. apply union_el_incl.
+ intros v. apply union_incl.
- intros [A B]. apply sub_anti.
+ intros z C. apply Union in C as [y [C E]].
apply (A y); auto.
+ apply B. intros y. apply union_el_incl.
Qed.

Lemma union_sing_eq x:
union (sing x) = x.
Proof.
apply union_lub. split; auto.
Qed.

Lemma union_monotone x y:
x <<= y -> union x <<= union y.
Proof.
intros A z. rewrite !Union. firstorder.
Qed.

Binary union

Definition bun (x y : set): set := union (upair x y).

Lemma bun_in x y z:
x el y \/ x el z -> x el bun y z.
Proof.
intros A. apply Union. intuition; eauto.
Qed.

Hint Resolve bun_in.

Lemma el_bun x y z:
z el bun x y <-> z el x \/ z el y.
Proof.
split.
- intros A. apply Union in A as [u [A B]].
apply Upair in A as [|]; subst u; auto.
- intuition.
Qed.

Lemma bun_incl' x y u:
u <<= x \/ u <<= y -> u <<= bun x y.
Proof.
intros A z C. apply el_bun; intuition.
Qed.

Separation

Axiom sep: set -> (set -> Prop) -> set.
Axiom Sep: forall x p z, z el sep x p <-> z el x /\ p z.

Lemma sep_realizes x p:
subcs p x -> realizes (sep x p) p.
Proof.
intros A z. rewrite Sep. specialize (A z). tauto.
Qed.

Lemma sep_incl x y p:
x <<= y -> sep x p <<= y.
Proof.
intros A z B. apply Sep in B. apply A, B.
Qed.

Lemma sep_incl' y x p:
y <<= x -> subsc y p -> y <<= sep x p.
Proof.
intros A B z C. apply Sep. intuition.
Qed.

Lemma sep_subc x p:
subsc (sep x p) p.
Proof.
intros z A. apply Sep in A. apply A.
Qed.

Lemma unrealizable_red p q:
~ realizable p -> subcc p q -> ~ realizable q.
Proof.
intros A B. contradict A.
destruct A as [x A]. exists (sep x p).
intros z. rewrite Sep.
specialize (A z). intuition.
Qed.

Relative empty sets

Definition eset x :=
sep x (fun _ => False).

Lemma eset_equal x y:
eset x = eset y.
Proof.
apply sub_anti; intros z Z; apply Sep in Z as [_ []].
Qed.

Lemma not_inhab x:
~ inhab x -> x = eset x.
Proof.
intros XN. apply sub_anti; intros z Z.
- contradict XN. now exists z.
- apply Sep in Z as [_ []].
Qed.

Lemma union_eset_eq x:
union (eset x) = eset x.
Proof.
apply sub_anti; intros z Z.
- apply Union in Z as [y[Y1 Y2]]. apply Sep in Y1 as [_ []].
- apply Sep in Z as [_ []].
Qed.

Replacement

Implicit Types R: set -> set -> Prop.

Definition func R :=
forall x y y', R x y -> R x y' -> y = y'.

Definition fpart R x y :=
unique (R x) y.

Lemma func_fpart R:
func (fpart R).
Proof.
firstorder.
Qed.

Definition Rep1 :=
exists rep, forall R y u, func R -> (y el rep u R <-> exists x, x el u /\ R x y).

Definition Rep2 :=
exists rep, forall R y u, y el rep u R <-> exists x, x el u /\ unique (R x) y.

Lemma Rep1_Rep2:
Rep1 <-> Rep2.
Proof.
split; intros [rep Rep].
- exists (fun x R => rep x (fpart R)). intros R y u. split; intros H.
+ apply Rep in H; auto using func_fpart.
+ apply Rep; auto using func_fpart.
- exists rep. intros R y u FR. split; intros H.
+ apply Rep in H; firstorder.
+ apply Rep; firstorder.
Qed.

Axiom rep: set -> (set -> set -> Prop) -> set.
Axiom Rep: forall R y u, y el rep u R <-> exists x, x el u /\ unique (R x) y.

Lemma rep_func R:
func R -> forall y u, y el rep u R <-> exists x, x el u /\ R x y.
Proof.
intros FR. intros y u; split; intros H.
- apply Rep in H. firstorder.
- apply Rep. firstorder.
Qed.

Fact sep_rep u p:
sep u p = rep u (fun x y => x = y /\ p x).
Proof.
apply Ext. intros z.
rewrite Sep, Rep; firstorder congruence.
Qed.

Definition frep x F :=
rep x (fun a b => b = F a).

Lemma frep_correct F x z:
z el frep x F <-> exists y, y el x /\ z = F y.
Proof.
split.
- intros Z. apply Rep in Z as [y[Z1 [Z2 _]]]. exists y. now split.
- intros [y[Y1 Y2]]. apply Rep. exists y. split; firstorder; congruence.
Qed.

Definition desc p x :=
union (rep (sing (eset x)) (fun y => p)).

Lemma desc_correct p x:
unique p x -> p (desc p x).
Proof.
intros [P1 P2]. cutrewrite (desc p x = x); trivial.
apply sub_anti; intros y Y.
- apply Union in Y as [z[Z1 Z2]]. apply Rep in Z1 as [u[U1 U2]].
cutrewrite (x = z); trivial. apply P2. apply U2.
- apply Union. exists x. split; trivial. apply Rep.
exists (eset x). split; firstorder using el_sing.
Qed.

Power sets

Axiom pow: set -> set.
Axiom Power: forall x z, z el pow x <-> z <<= x.

Lemma power_incl x y:
x <<= y -> x el pow y.
Proof.
apply Power.
Qed.

Lemma power_incl' x y:
x el pow y -> x <<= y.
Proof.
apply Power.
Qed.

Lemma power_monotone x y:
x <<= y -> pow x <<= pow y.
Proof.
intros I z Z. apply Power in Z.
apply Power. now apply (sub_trans Z).
Qed.

Hint Resolve power_incl power_incl' power_monotone.

Lemma union_power_eq x:
union (pow x) = x.
Proof.
apply sub_anti.
- apply union_incl. auto.
- apply union_el_incl. auto.
Qed.