Proof Theory at the University of Munich
People
Proof theory, originally designed by David Hilbert as a framework for securing the foundations of mathematics and formalizing mathematical reasoning, is now concerned with the study of proofs as formal objects and with a broad range of related topics. It is one of the central fields of mathematical logic and has applications in many areas of mathematics, philosophy and computer science. In the last two decades proof theory has become increasingly important for computer science, and proof theory and theoretical computer science are nowadays considered as being very closely related. Research Interests
- Proof and computation
- Normalization techniques
- Lambda calculus
- Infinitary Proofs
- Ordinal Analysis
- Interactive Theorem Proving and Program Extraction
Infinitary proofs
Infinitary proofs are one of the main technical tools in Ordinal Analysis. Among other things they provide a perspicuous explanation of certain rather complicated and involved operations on finite (formal) proofs, or they make it possible to dispense with such operations at all.
Ordinal Analysis
The concern of Ordinal Analysis is to characterize the strength of particular (mathematically relevant) axiom systems in terms of their provable wellorderings. Usually the ordinal analysis of a formal system T provides a lot of important information about T, e.g., a concrete representation of the proof-theoretic ordinal of T (which is the supremum of the order types of all provable wellorderings of T), a reduction of T to primitive recursive arithmetic PRA plus transfinite induction (up to each ordinal below the proof-theoretic ordinal of T), a classification of the provably recursive functions of T, a description of partial models of T, combinatorial independence results. Of special importance in this area are concrete representations of ordinals, so-called ordinal notation systems. The study of ordinal notation systems also has applications in term rewriting theory, a field on the borderline between proof-theory and theoretical computer science.
Interactive Theorem Proving and Program Extraction
It is well known that it is undecidable in general whether a given program meets its specification. In contrast, it can be checked easily by a machine whether a formal proof is correct, and from a constructive proof one can automatically extract a corresponding program, which by its very construction is correct as well. This - at least in principle - opens a way to produce correct software, e.g. for safety-critical applications. Moreover, programs obtained from proofs are ``commented'' in a rather extreme sense. Therefore it is easy to maintain them, and also to adapt them to particular situations.
Inductive data types
The natural numbers are the simplest example of an inductive type. If one extends the simply typed lambda calculus by recursion on this type, one obtains Gödel's system T. Lists and (countably branching) trees are further examples of inductive types. More `wild' inductive types mostly have their roots in proof theory; a prominent example are `continuations', i.e. continuations of computations (as `first-class citizens') in functional programming languages, that can then be studied in the context of typed lambda calculus.