# Publication details

##
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

@MASTERSTHESIS{Kaiser:2012:Formal,
title = {Formal Costruction of a Set Theory in Coq},
author = {Jonas Kaiser},
year = {2012},
school = {Programming Systems Lab, Saarland University},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009