Formal Developments of Set Theory in Coq

Saarland University Computer Science
Reconsidering Pairs and Functions as Sets

We start from axioms for intuitionistic (well-founded) Zermelo-Fraenkel set theory without an axiom of infinity. An epsilon recursion principle is proven. Using this ordered pairs and functions are defined in such a way that ordered pairs are the same as functions from the finite ordinal 2. This is written up in an article that has been submitted to a journal, with a technical report version available here.

Three Forms of Replacement

Three forms of replacement (as operators) are considered:

In an intuitionistic set theory without separation or replacement as axioms, we prove that partial replacement is equivalent to total replacement and separation. Also, total replacement is equivalent to map replacement and having a description operator.

Ackermann Encoding of Decidable Hereditarily Finite Sets

Following Ackermann 1937 [Ack37], a membership relation can be defined on the natural numbers and the Zermelo-Fraenkel axioms except infinity can be proven. Separation is limited to decidable predicates. Choice should also be provable, but is not considered in the file.

Model of ZF using a quotient of Aczel's Set Type, assuming Epsilon.

In the 1970s, Aczel gave an inductive type of trees on which an equivalence relation can be recursively defined [Acz77]. The trees behave as sets relative to the equivalence relation. In this Coq development, we assume classical logic, epsilon (a form of choice) and extensionality. After defining the Aczel type and the equivalence relation (following Werner's 1997 description [Wer97]), we use the choice operator to obtain canonical representatives. We then define the quotient using sigma types and canonical representatives. The Zermelo-Fraenkel axioms are proven. We do not consider the choice axiom, though it should be provable as well.


Legal notice, Privacy policy