Bonn Mathematical Logic Group

Selected Topics in Mathematical Logic (V5A8)
Type Theory and the Formalization of Mathematics


Lecturer

Time and place

Contents

Type theory was founded by Bertrand Russell to avoid paradoxes in naive set theory as formalized by Gottlob Frege (Russell's paradox). Every variable in type theory has a type. Relations and functions only accept variables of certain types so that problematic formulas like x ∈ x are excluded from the language of type theory.

Various type theories were developed by Alonzo Church, Per Martin-Löf, and others. Type theories can be used to provide foundations of mathematics, or to provide a semantics for typed programming languages. A recent development is homotopy type theory which views types as topological spaces and functions as continuous functions.

Type theory is also employed in complete, computer-supported formalizations of mathematical statements and proofs ("Formal Mathematics"). Typing of mathematical objects helps in organizing the search spaces of automatic proving tools.

In this course, we shall give an introduction to some type theories, demonstrate their mathematical expressibility, and how they may be implemented in mathematical proof-checking software like LEAN ( https://leanprover.github.io/). This module is a Master course which should be accessible on the basis of the Bachelor module "Einführung in die Mathematische Logik".

We shall use material from the following sources:

There will be no exercise class for this course. The module will be examined orally.

This summer semester I shall also offer a number of places in a module Praktikum Mathematische Logic P2A1, or Practical Project in Mathematical Logic P4A1, respectively, about practical formalizations of mathematics using natural language. It may be advantageous to combine the lecture course with the practical module.

Last changed: 20. Januar 2019