Publication details

Saarland University Computer Science

Formal Costruction of a Set Theory in Coq

Jonas Kaiser

Master's Thesis, Programming Systems Lab, Saarland University, 2012

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.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy