Intuitionistic Zermelo-Fraenkel Set Theory in Coq
- Alexandre Miquel
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).
intuitionistic set theory, pointed graphs, type theory, intuitionistic choice operator, set theory, zermelo fraenkel
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)