# Formal Developments of Set Theory in Coq

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:

• Map Replacement takes a set and a meta-level function and returns the image set.
• Total Replacement takes a set and a total functional meta-level relation and returns the image set.
• Partial Replacement takes a set and a functional meta-level relation and returns the image set. (I first saw a replacement axiom in this form in Barras 2010 [Bar10].)
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.

• The first file defines a module type to make it clear what a model of ZF must satisfy: html version (Coq file)
• The second file contains the construction and the proof that it gives a module (model of ZF): html version (Coq file)

## References:

• [Ack37] Wilhelm Ackermann. Die Widerspruchsfreiheit der allgemeinen Mengenlehre. Mathematische Annalen 114: 305-315, 1937
• [Acz77] Peter Aczel. The type theoretic interpretation of constructive set theory. In A. MacIntyre, L. Pacholski, and J. Paris, editors, Logic Colloquium '77, pages 55-66. NorthHolland, 1978.
• [Bar10] Barras, B. Sets in Coq, Coq in Sets. Journal Of Formalized Reasoning, 3(1), 29-48. 2010.
• [Wer97] Benjamin Werner. Sets in types, types in sets. In Proceedings of TACS '97, pages 530-546. Springer-Verlag, 1997.