Logic and Proof Theory
3-4 hours of lectures per week.
Lecturer Ulrich Kohlenbach Content The first half of the course gives a graduate level introduction to the syntax and semantics of (first-order) predicate logic including a brief treatment of second-order, intuitionistic and modal logic.
The second half of the course offers an introduction to the area of proof theory which is concerned with effective proof transformations. We will treat both so-called structural proof theory (cut-elimination and normalization) as well as semantically motivated proof interpretations (realizability and functional interpretations).
We discuss how these techniques allow to extract effective data from purely existential proofs
proofs as programs.
Prerequisites Models and Logic useful but not necessary, some mathematical maturity.
Literature To be announced.
Examination Compulsory homework assignments + oral exa.