Aidan Ewart

---

Viewing IZF.v

The source for this file is available here.

Require Import Program.

Create HintDb zf.

Module Type IZF.
  Parameter set : Type.

  Notation "A ≡ B" := (A = B) (at level 70).
  Axiom K : forall {x y: set} (p p0: x ≡ y), p = p0.

  Parameter member : set -> set -> Prop.
  Notation "A ∈ B" := (member A B) (at level 70).
  Parameter equiv_ext :
    forall {x y}, (forall {z}, z ∈ x <-> z ∈ y) -> x ≡ y.
  Notation "A ∉ B" := (A ∈ B -> False) (at level 70).
  Hint Resolve equiv_ext : zf.
  Axiom M : forall {x y} (p p0: x ∈ y), p = p0.

  Definition subset A B := forall x, x ∈ A -> x ∈ B.
  Notation "A ⊆ B" := (subset A B) (at level 70).

  Parameter empty : set.
  Notation "∅" := empty.
  Parameter empty_prop : forall {x}, x ∉ ∅.
  Hint Resolve empty_prop : zf.

  Parameter insert : set -> set -> set.
  Notation "x +> y" := (insert x y) (at level 60).
  Parameter insert_propH :
    forall {x y z}, z ∈ x +> y -> z ∈ y \/ z ≡ x.
  Parameter insert_propG :
    forall {x y z}, z ∈ y \/ z ≡ x -> z ∈ x +> y.
  Hint Resolve insert_propH insert_propG : zf.
  
  Parameter union : set -> set.
  Notation "⋃ X" := (union X) (at level 60).
  Parameter union_propG :
    forall {x z}, (exists y, y ∈ x /\ z ∈ y) -> z ∈ ⋃x.
  Parameter union_propH :
    forall {x z}, z ∈ ⋃x -> exists y, y ∈ x /\ z ∈ y.
  Hint Resolve union_propH union_propG : zf.

  Definition ordered_pair x y :=
    insert (insert x ∅) (insert (insert x (insert y ∅)) ∅).
  Notation "⟨ x , y ⟩" := (ordered_pair x y).

  Definition Suc x := x +> x.
  
  Parameter infinity : set.
  Notation "'ω'" := infinity (at level 60).
  Parameter infinity_propZ : ∅ ∈ ω.
  Parameter infinity_propS :
    forall {x}, x ∈ ω -> Suc x ∈ ω.
  Hint Resolve infinity_propZ infinity_propS : zf.

  Parameter selection : (set -> Prop) -> set -> set.
  Parameter selection_propH : forall {P x y},
      x ∈ selection P y -> x ∈ y /\ P x.
  Parameter selection_propG : forall {P x y},
      x ∈ y /\ P x -> x ∈ selection P y.
  Hint Resolve selection_propH selection_propG : zf.
  
  Definition formula {D} := {P: set -> set -> Prop | forall x, x ∈ D -> exists y, P x y}.
  
  Parameter collection : forall {D}, @formula D -> set.
  Parameter collection_propH : forall {D P x},
      x ∈ @collection D P -> exists i, i ∈ D /\ proj1_sig P i x.
  Parameter collection_propG : forall {D P x},
      (exists i, i ∈ D /\ proj1_sig P i x) -> x ∈ @collection D P.
  Hint Resolve collection_propH collection_propG : zf.

  Parameter ϵ_induction :
    forall {P}, (forall x, (forall y, y ∈ x -> P y) -> P x) ->
           forall x, P x.
  
  Parameter ω_induction :
    forall {P}, (forall x, x ∈ ω -> P x -> P (Suc x)) ->
           P ∅ ->
           forall x, x ∈ ω -> P x.
  
  Parameter ϵ_rec : (forall x, (forall y, y ∈ x -> set) -> set) -> set -> set.  
  Axiom ϵ_rec_prop : forall {H x}, ϵ_rec H x = H x (fun y _ => ϵ_rec H y).
End IZF.