Jonas Kaiser

Saarland University Computer Science

Master's Thesis: Formal Construction of a Set Theory in Coq

Author: Jonas Kaiser
Advisor: Dr. Chad E. Brown
Supervisor: Prof. Dr. Gert Smolka


In this thesis we present a formalisation of Tarski-Grothendieck set theory, that is, Zermelo-Fraenkel set theory with Grothendieck universes. The development is executed in Coq, extended with the law of the excluded middle and a powerful choice principle. This yields a powerful metatheory where the inhabitance of every type is decidable. From the axiomatisation we develop the usual theory of sets, including restricted comprehension, ordered pairs, functions and finite ordinals.

The formalisation is designed to support the construction of proof-irrelevant, classical models for type theories like the Calculus of (co)inductive Constructions. The actual model constructions are left for future work.

Attached Documents

Legal notice, Privacy policy