Library EnsEm

Require Export basic.
Require Import Choice. Require Import Sublogic.
Require Import ZFdef.

In this file, we build a model of both intuitionistic and classical ZF in Coq extended with the Type-Theoretical Collection Axiom (TTColl).

Module Ensembles (L:SublogicTheory) <: IZF_C_sig L <: IZF_R_HalfEx_sig L.

Import L.

The level of sets

Definition Thi := Type.

The level of indexes

Definition Tlo : Thi := Type.

Inductive set_ : Thi :=
  sup (X:Tlo) (f:X->set_).
Definition set := set_.

Definition idx (x:set) := let (X,_) := x in X.
Definition elts (x:set) : idx x -> set :=
  match x return idx x -> set with
  | sup X f => f
  end.

Statement of useful axioms (independently of the logic used):

TTRepl
TTColl

They are both consequence of choice

TTColl

Definition ttcoll (E:set->set->Prop) := ∀ (X:Tlo) (R:X->set->Prop),
  (∀ i, Proper (E ==>iff) (R i)) ->
  exists Y:Tlo , exists g:Y->set ,
    ∀ i, (exists w, R i w) -> exists j:Y , R i (g j).

Lemma ttcoll_mono (E E':set->set->Prop) :
  (∀ x y, E x y -> E' x y) ->
  ttcoll E -> ttcoll E'.

TTColl is a consequence of choice

Record ttcoll_dom (X:Tlo) (R:X->set->Prop) : Tlo := mkCi {
cd_i:X;
cd_dom : exists y, R cd_i y
}.

We show that all instances of ttcoll are a consequence of choice.

Lemma ttcoll_from_choice E :
(∀ (X:Tlo), choice X set) -> ttcoll E.

TTRepl

Definition ttrepl (E:set->set->Prop) :=
∀ X:Tlo, unique_choice X set E.

We show that all instances of ttrepl are a consequence of choice.

Lemma ttrepl_from_choice E :
(∀ X:Tlo, choice X set) -> ttrepl E.

Equality and membership

Fixpoint eq_set (x y:set) {struct x} :=
  (∀ i, #exists j, eq_set (elts x i) (elts y j)) /\
  (∀ j, #exists i, eq_set (elts x i) (elts y j)).

Lemma eq_set_def x y :
  eq_set x y <->
  (∀ i, #exists j, eq_set (elts x i) (elts y j)) /\
  (∀ j, #exists i, eq_set (elts x i) (elts y j)).

Lemma eqset_isL : ∀ x y, isL(eq_set x y).
Global Hint Resolve eqset_isL.

Lemma eq_set_intro x y :
  (∀ i, exists j, eq_set (elts x i) (elts y j)) ->
  (∀ j, exists i, eq_set (elts x i) (elts y j)) ->
  eq_set x y.

Lemma eq_set_refl : ∀ x, eq_set x x.

Lemma eq_set_sym : ∀ x y,
  eq_set x y -> eq_set y x.

Lemma eq_set_trans : ∀ x y z,
  eq_set x y -> eq_set y z -> eq_set x z.

Definition in_set x y :=
  #exists j, eq_set x (elts y j).

Lemma inset_isL : ∀ x y, isL (in_set x y).
Global Hint Resolve inset_isL.

Notation "x ∈ y" := (in_set x y) (at level 60).
Notation "x == y" := (eq_set x y) (at level 70).

Lemma eq_set_ax : ∀ x y,
  x == y <-> (∀ z, z ∈ x <-> z ∈ y ).

Lemma in_reg : ∀ x x' y,
  x == x' -> x ∈ y -> x' ∈ y.

Lemma eq_intro : ∀ x y,
  (∀ z, z ∈ x -> z ∈ y) ->
  (∀ z, z ∈ y -> z ∈ x) ->
  x == y.

Lemma eq_elim : ∀ x y y',
  x ∈ y ->
  y == y' ->
  x ∈ y'.

Instance in_set_morph : Proper (eq_set ==> eq_set ==> iff) in_set.

Qed.

Definition el (x:set) := {z|z ∈ x }.
Definition eli x y (h:y ∈ x): el x := exist (fun z=>z ∈ x) y h.

Definition elts' (x:set) (i:idx x) : el x.
Defined.

Lemma eq_elim1 x y : el x -> x == y -> el y.

Lemma incl_elim1 x y :
  el x -> (∀ z, z ∈ x -> z ∈ y) -> el y.

Set induction

Lemma wf_ax :
  ∀ (P:set->Prop),
  (∀ x, isL (P x)) ->
  (∀ x, (∀ y, y ∈ x -> P y) -> P x) ->
  ∀ x, P x.

Empty set

Definition empty :=
sup False (fun x => match x with end).

Lemma empty_ax : ∀ x, x ∈ empty -> #False.

Singleton and pairs

Definition singl x := sup unit (fun _ => x).

Definition pair x y :=
  sup bool (fun b => if b then x else y).

Lemma pair_ax : ∀ a b z,
  z ∈ pair a b <-> #(z == a \/ z == b ).

Lemma pair_morph :
  ∀ a a', a == a' -> ∀ b b', b == b' ->
  pair a b == pair a' b'.

Union

Record union_idx x := mkUi {
  un_i : idx x;
  un_j : idx(elts x un_i)
}.

Definition union (x:set) :=
  sup (union_idx x)
    (fun p => elts (elts x (un_i _ p)) (un_j _ p)).

Lemma union_ax : ∀ a z,
  z ∈ union a <-> #exists2 b, z ∈ b & b ∈ a.

Lemma union_morph :
  ∀ a a', a == a' -> union a == union a'.

Separation axiom

Record subset_idx x (P:set->Prop) := mkSi {
  sb_i : idx x;
  sb_spec : #exists2 x', elts x sb_i == x' & P x'
}.

Definition subset (x:set) (P:set->Prop) :=
  sup (subset_idx x P) (fun y => elts x (sb_i _ _ y)).

Lemma subset_ax : ∀ x P z,
  z ∈ subset x P <->
  z ∈ x /\ #exists2 z', z == z' & P z'.

Power-set axiom

Definition power (x:set) :=
  sup (idx x->Prop)
   (fun P => subset x
         (fun y => #exists2 i, y == elts x i & P i)).

Lemma power_ax : ∀ x z,
  z ∈ power x <->
  (∀ y, y ∈ z -> y ∈ x ).

Lemma power_morph : ∀ x x', x == x' -> power x == power x'.

Infinity

Fixpoint num (n:nat) : set :=
  match n with
  | 0 => empty
  | S k => union (pair (num k) (pair (num k) (num k)))
  end.

Definition infinite := sup _ num.

Lemma infinity_ax1 : empty ∈ infinite.

Lemma infinity_ax2 : ∀ x, x ∈ infinite ->
  union (pair x (pair x x)) ∈ infinite.

Functional Replacement

Definition replf (x:set) (F:set->set) :=
  sup _ (fun i => F (elts x i)).

Lemma replf_ax : ∀ x F z,
  (∀ z z', z ∈ x -> z == z' -> F z == F z') ->
  (z ∈ replf x F <-> #exists2 y, y ∈ x & z == F y).

Functional replacement with domain information

Definition repl1 (x:set) (F:el x->set) :=
  sup _ (fun i => F (elts' x i)).

Lemma repl1_ax : ∀ x F z,
  (∀ z z', proj1_sig z == proj1_sig z' -> F z == F z') ->
  (z ∈ repl1 x F <-> #exists y, z == F y).

Lemma repl1_mono x y F G :
  (∀ z, z ∈ x -> z ∈ y) ->
  (∀ x' y', proj1_sig x' == proj1_sig y' -> F x' == G y') ->
  (∀ z, z ∈ repl1 x F -> z ∈ repl1 y G).

Lemma repl1_morph : ∀ x y F G,
  x == y ->
  (∀ x' y', proj1_sig x' == proj1_sig y' -> F x' == G y') ->
  repl1 x F == repl1 y G.

Section WellFoundedRecursion.
Variable f : set -> set.
Hypothesis fm : Proper (eq_set ==>eq_set) f.

Fixpoint WFR (x:set) (p:Acc in_set x) {struct p} : set :=
  f (repl1 x (fun (y:el x) =>
               WFR (proj1_sig y) (Acc_inv p (proj2_sig y)))).
Lemma WFR_eqn x p : WFR x p == f (repl1 x (fun y => WFR _ (Acc_inv p (proj2_sig y)))).

Lemma WFR_irrel x p x' p' : x ==x' -> WFR x p == WFR x' p'.

End WellFoundedRecursion.

Relational replacement

We only use the following instance of TTRepl for replacement:

Axiom ttrepl_ax : ttrepl eq_set.

Section NotClassical.

Record repl_dom a (R:set->set->Prop) := mkRi {
rd_i : idx a;
rd_dom : #exists y, R (elts a rd_i) y
}.

Showing that TTRepl implies Replacement. This proofs requires that we are in the intuitionistic fragment. If L is classical logic, we would have a model of ZF in Coq+TTRepl.

Hypothesis intuit : ∀ P:Prop, (#P) -> P.

Lemma weak_uniq_R : ∀ a (R:set->set->Prop),
    (∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') ->
    (∀ x y y', x ∈ a -> R x y -> R x y' -> y == y') ->
    (∀ x x' y y', x ∈ a -> R x y -> R x' y' -> x == x' -> y == y').

Lemma intuit_repl_ax a (R:set->set->Prop) :
    (∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') ->
    (∀ x y y', x ∈ a -> R x y -> R x y' -> y == y') ->
    exists b, ∀ x, x ∈ b <-> #exists2 y, y ∈ a & R y x.
End NotClassical.

Collection

TTColl is stronger than TTRepl

Lemma ttrepl_from_ttcoll : ttcoll eq_set -> ttrepl eq_set.

We now show that TTColl implies (set-theoretical) collection

Axiom ttcoll_axiom : ttcoll eq_set.

Lemma ttcoll_set A (R:set->set->Prop) :
  Proper (eq_set ==>eq_set ==>iff) R ->
  exists z, ∀ i, (exists w, R (elts A i) w) ->
            exists j, R (elts A i) (elts z j).

Lemma collection_ax : ∀ A (R:set->set->Prop),
    Proper (eq_set ==>eq_set ==>iff) R ->
    exists B, ∀ x, x ∈ A ->
      (#exists y, R x y) ->
      (#exists2 y, y ∈ B & R x y).

Lemma collection_ax' : ∀ A (R:set->set->Prop),
    Proper (eq_set ==>eq_set ==>iff) R ->
    (∀ x, x ∈ A -> (#exists y, R x y)) ->
    exists B, ∀ x, x ∈ A -> #exists2 y, y ∈ B & R x y.

Comparison of replacement and collection

Definition mkRel (R:set->set->Prop) x y :=
  exists2 x', x ==x' & exists2 y', y ==y' & R x' y'.

Instance mkRel_morph R : Proper (eq_set ==>eq_set ==>iff) (mkRel R).

Qed.

Lemma repl_from_collection : ∀ a (R:set->set->Prop),
    (∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') ->
    (∀ x y y', x ∈ a -> R x y -> R x y' -> y == y') ->
    exists b, ∀ x, x ∈ b <-> #exists2 y, y ∈ a & R y x.

Lemma empty_ex: #exists empty, ∀ x, x ∈ empty -> Tr False.

Lemma pair_ex: ∀ a b,
  #exists c, ∀ x, x ∈ c <-> Tr(x == a \/ x == b).

Lemma union_ex: ∀ a, #exists b,
    ∀ x, x ∈ b <-> #exists2 y, x ∈ y & y ∈ a.

Lemma subset_ex : ∀ a P, #exists b,
    ∀ x, x ∈ b <-> x ∈ a /\ #exists2 x', x == x' & P x'.

Lemma power_ex: ∀ a, #exists b,
     ∀ x, x ∈ b <-> (∀ y, y ∈ x -> y ∈ a ).

Lemma infinity_ex: #exists2 infinite,
    (#exists2 empty, (∀ x, x ∈ empty -> Tr False ) & empty ∈ infinite) &
    (∀ x, x ∈ infinite ->
     #exists2 y,
       (∀ z, z ∈ y <-> #(z == x \/ z ∈ x )) &
       y ∈ infinite).

Definition repl_ex :=
  fun a R Rm Ru => TrI(repl_from_collection a R Rm Ru).

Definition coll_ex :=
  fun a R Rm => TrI(collection_ax a R Rm).

Fixpoint

Record wfrec_dom x y := mkWi {
  wf_i : idx x;
  wf_eq : elts x wf_i == y
}.

Fixpoint wfrec (F:(set->set)->set->set) (x:set) : set :=
  F (fun y => union (sup (wfrec_dom x y)
               (fun i => wfrec F (elts x (wf_i _ _ i))))) x.
Section FixRec.
Hypothesis F : (set->set)->set->set.
Hypothesis Fext : ∀ x x' f f',
  (∀ y y', y ∈ x -> y == y' -> f y == f' y') ->
  x == x' ->
  F f x == F f' x'.

Instance wfrecm : Proper (eq_set ==>eq_set) (wfrec F).

Qed.

Lemma wfrec_eqn x :
  wfrec F x == F (wfrec F) x.

End FixRec.

Showing that in classical logic, collection can be made deterministic, by building the smallest element of Veblen hierarchy containing the images

Section ClassicalCollection.

Veblen cumulative hierarchy (applied to any set)

Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))).

Lemma V_morph : ∀ x x', x == x' -> V x == V x'.

Lemma V_def : ∀ x z,
  z ∈ V x <-> #exists2 y, y ∈ x & z ∈ power (V y).

Lemma V_trans : ∀ x y z,
  z ∈ y -> y ∈ V x -> z ∈ V x.

Lemma V_pow : ∀ x, power (V x) == V (singl x).

Lemma V_mono : ∀ x x',
  x ∈ x' -> V x ∈ V x'.

Lemma V_sub : ∀ x y y',
  y ∈ V x -> y' ∈ power y -> y' ∈ V x.

Lemma V_compl : ∀ x z, z ∈ V x <-> V z ∈ V x.

Lemma V_comp2 x y : x ∈ power (V y) -> V x ∈ power (V y).

Lemma V_intro : ∀ x, x ∈ power (V x).

Lemma V_idem : ∀ x, V (V x) == V x.

Lemma rk_induc :
  ∀ P:set->Prop,
  (∀ x, isL (P x)) ->
  (∀ x, (∀ y, y ∈ V x -> P y) -> P x) ->
  ∀ x, P x.

Hypothesis EM : ∀ A, #(A \/ (A->#False )).

Classical proof that the rank of a set is totally ordered

Lemma V_total : ∀ x y, #(V x ∈ V y \/ V y ∈ power (V x)).

Definition lst_rk (P:set->Prop) (y:set) :=
  P y /\
  y == V y /\
  ∀ x, x == V x -> P x -> y ∈ power(V x).

Lemma lst_rk_morph :
  ∀ (P P':set->Prop),
  (∀ x x', x == x' -> (P x <-> P' x')) ->
  ∀ y y', y == y' -> lst_rk P y -> lst_rk P' y'.

Lemma lst_incl : ∀ P y, lst_rk P y -> P y.

Lemma lst_fun : ∀ P y y', lst_rk P y -> lst_rk P y' -> y == y'.

Proof that if P is true for some Veblen universe, then we can find the least rank satisfying P.

Lemma lst_ex : ∀ (P:set->Prop),
  Proper (eq_set ==>iff) P ->
  (#exists x, P (V x)) ->
  (#exists x, lst_rk P x).

Definition coll_spec A R B :=
  lst_rk (fun B =>
      ∀ x, x ∈ A ->
      (#exists y, R x y) ->
      (#exists2 y, y ∈ B & R x y)) B.

Lemma coll_ax_uniq : ∀ A (R:set->set->Prop),
    Proper (eq_set ==> eq_set ==> iff) R ->
    #exists B, coll_spec A R B.

Lemma coll_ax_mono : ∀ A A' (R:set->set->Prop) B B',
    Proper (eq_set ==> eq_set ==> iff) R ->
    coll_spec A R B ->
    coll_spec A' R B' ->
    (∀ z, z ∈ A -> z ∈ A') ->
    (∀ z, z ∈ B -> z ∈ B').

End ClassicalCollection.

End Ensembles.

Module Ens := Ensembles CoqSublogicThms.
Import Ens.

Proving that ttrepl + EM => ttcoll If we could avoid EM, we would have that ttrepl gives Coq the strength of ZF

Lemma ttcoll_from_ttrepl_em : (∀ P,P \/~P) -> ttrepl eq_set -> ttcoll eq_set.