Selected Topics in Mathematical Logic (V5A8)
Type Theory and the Formalization of Mathematics
Lecturer
- Prof. Dr. Peter Koepke
Time and place
- Lecture: Thursday 14:15 - 16:00, N 0.003. Start: 04. April.
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:
- Jeremy Avigad, "Theorem Proving in Lean" (https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf)
- Robert Constable, "Naive Computational Type Theory" (http://www.nuprl.org/documents/Constable/NaiveTypeTheoryPreface.html)
- "Homotopy Type Theory" (https://homotopytypetheory.org/book/)
- Rob Nederpelt and Herman Geuvers, "Type Theory and Formal Proof", CUP (see also http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf)
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.