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.