Contribution: IZF

Intuitionistic Zermelo-Fraenkel Set Theory in Coq

Authors

Description

This development contains the set-as-pointed-graph interpretation of Intuitionistic Zermelo Frankel set theory in system F_omega.2++ (F_omega + one extra universe + intuitionistic choice operator), which is described in chapter 9 of the author's PhD thesis (for IZ) and in the author's CSL'03 paper (for the extension IZ -> IZF).

Keywords

intuitionistic set theory, pointed graphs, type theory, intuitionistic choice operator, set theory, zermelo fraenkel

README

Intuitionistic Zermelo-Frankel set theory in Coq
================================================

These Coq-files contain the set-as-pointed graph interpretation of
Intuitionistic Zermelo Frankel set theory in type theory, which is
described in chapter 9 of the author's PhD thesis (for IZ) and in
the author's CSL'03 paper (for the extension IZ -> IZF).

Contents
========

  IZF_logic.v:  Definition of universes, connectives (2nd-order
    encoding), quantifiers, Leibniz equality, etc.

  IZF_base.v: Basic principles of the sets-as-pointed-graphs
    interpretation: set-theoretic equality as bisimilarity,
    membership as shifted bisimilarity, extensionality.

  IZF_pair.v:  Translation of the pairing axiom.

  IZF_select.v:  Translation of the selection scheme.

  IZF_power.v:  Translation of the powerset axiom.

  IZF_union.v:  Translation of the union axiom.

  IZF_coll.v:  Translation of the intuitionistic collection scheme.
    The corresponding proofs rely on some extra-axioms that define
    the intuitionisitic version of Hilbert's choice operator, such
    as described in the author's LICS'03 submitted paper.

  IZF_nat.v:  An implementation of Chuch numerals in the second
    predicative universe.  Translation of Peano axioms.

  IZF_omega.v:  Translation of the set-theoretic axiom of infinity.
    Construction of a pointed graph representing the ordinal omega.

Author
======
Alexandre Miquel (Alexandre.Miquel@lri.fr)

Available files