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
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.

Hint Resolve sub_refl.

Lemma sub_trans x y z:
x <<= y -> y <<= z -> x <<= z.

Lemma sub_anti x y:
x <<= y -> y <<= x -> x = y.

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.

Fact greatest_unique x y p:
greatest x p -> greatest y p -> x = y.

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).

Lemma unrealizable_new_el p:
(forall x, subsc x p -> exists y, p y /\ ~ y el x) -> ~ realizable p.

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.

Lemma upair_inr x y:
y el upair x y.

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.

Singletons

Definition sing x: set := upair x x.

Lemma sing_injective x y:
sing x = sing y -> x=y.

Lemma el_sing x y:
x el sing y <-> x=y.

Lemma in_sing x y:
x=y -> x el sing y.

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.

Lemma upair_sing x y z:
upair x y = sing z -> x = y /\ x = z.

Lemma sub_sing x y:
x <<= sing y -> inhab x -> x = sing y.

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.

Lemma union_incl u x:
union x <<= u <-> forall y, y el x -> y <<= u.

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).

Lemma union_sing_eq x:
union (sing x) = x.

Lemma union_monotone x y:
x <<= y -> union x <<= union y.

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.

Hint Resolve bun_in.

Lemma el_bun x y z:
z el bun x y <-> z el x \/ z el y.

Lemma bun_incl' x y u:
u <<= x \/ u <<= y -> u <<= bun x y.

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.

Lemma sep_incl x y p:
x <<= y -> sep x p <<= y.

Lemma sep_incl' y x p:
y <<= x -> subsc y p -> y <<= sep x p.

Lemma sep_subc x p:
subsc (sep x p) p.

Lemma unrealizable_red p q:
~ realizable p -> subcc p q -> ~ realizable q.

Relative empty sets

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

Lemma eset_equal x y:
eset x = eset y.

Lemma not_inhab x:
~ inhab x -> x = eset x.

Lemma union_eset_eq x:
union (eset x) = eset x.

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).

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.

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.

Fact sep_rep u p:
sep u p = rep u (fun x y => x = y /\ p x).

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.

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

Lemma desc_correct p x:
unique p x -> p (desc p x).

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.

Lemma power_incl' x y:
x el pow y -> x <<= y.

Lemma power_monotone x y:
x <<= y -> pow x <<= pow y.

Hint Resolve power_incl power_incl' power_monotone.

Lemma union_power_eq x:
union (pow x) = x.