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