Dominik Kirst

Saarland University Computer Science

Formalised Set Theory: Well-Orderings and the Axiom of Choice

Author: Dominik Kirst
Advisor: Jonas Kaiser
Supervisor: Prof. Dr. Gert Smolka


In this thesis, we give a substantial formalisation of classical set theory in the proof system Coq. We assume an axiomatisation of ZF and present a development of the theory containing relations, functions and ordinals. The implementation follows the structure of standard text books. In the context of this theory, we prove Zermelo's Well-Ordering Theorem and the Axiom of Choice equivalent. In addition, we examine the history and development of modern set theory and compare Zermelo's original versions of the proof. We prove that both of them lead to the same ordering.

Attached Documents

Dominik Kirst, Fri Mar 10 12:07:38 2017