# Dominik Kirst

## Foundations of Mathematics: A Discussion of Sets and Types

**Author:** Dominik Kirst

**1st Advisor:** Prof. Holger Sturm

**2nd Advisor:** Prof. Ulrich Nortmann

## Abstract

The aim of this thesis is to provide an introductory discussion of the two most
common modern foundations of mathematics: axiomatic set theory and dependent
type theory. To provide a basis, we begin by explaining the main concepts
of and motivations for the respective systems in their standard formulation. This
includes a brief outline of first-order logic and ZF set theory on the one side, and
of simply typed lambda calculus and Martin-Lof type theory on the other side.
Subsequently sketching an ongoing debate, both approaches are compared with
respect to general criteria for practicality, their respective philosophical justification,
and their approximate consistency strength. We argue that, despite being
similarly expressive for the purposes of formal mathematics, dependent type
theory is based on the more convincing constructivist view and advantageous
for computer-assisted proving. To illustrate its potential for modern applications,
some parts of the mathematical development are formally verified using the Coq
proof assistant.

## Attached Documents

- Coq Demo (Peano Arithmetic): Browse
- Coq Demo (Sets-as-Trees): Browse
- Slides from Colloquium Talk: Download
- Submitted thesis (graded with 1.3): Download

Legal notice, Privacy policy