The summer school is addressed at students of mathematics, philosophy, computer science and other subjects that are related to mathematics with basic knowledge in logics. Preference will be given to undergraduate students in their final year and graduate students. The summer school conveys insight into current research topics in the areas of logics and computability. The scientific program consists of mini courses (with lectures, exercises and projects). English is the teaching language.
- From abstract mathematics to verified programs (Ulrich Berger, Swansea)
One often says that from a constructive mathematical proof of a theorem one can read-off an algorithm provided one has a representation of the mathematical objects involved. For example, the Intermediate Value Theorem states that every continuous function on the reals that is negative at 0 and positive at 1 has a zero between 0 and 1. With some extra conditions on the function the proof of the IVT can be done constructively and an algorithm for finding the zero can be read-off. This presupposes a representation of (exact) real numbers and a representation of continuous functions (with extra conditions). The example suggests that this 'reading-off' process is rather ad-hoc and heavily dependent on the particular problem area the theorem is about. In fact this is not so. I will present a uniform theory for reading-off (or 'extracting') algorithms from proofs that applies to a wide range of abstract axiomatic mathematics. The theory provides automatically representations of mathematical objects and formal proofs of the correctness of the extracted algorithms (which can be represented as executable programs in any higher-order functional programming language). The lectures will be accompanied by examples and practical program extraction exercises in the proof system Minlog.
- Gödel's Incompleteness Theorems (Reinhard Kahle, Lisbon)
Gödel's Incompleteness Theorems make part of the general mathematical culture. They concern the unprovability of certain formal statements in axiomatic theories. Their understanding, however, is often clouded by philosophical and technical inaccuracies. The aim of this course is to give a concise introduction to these results, their proofs and their relevance. We will, in particular, focus on the fundamental distinction between syntax and semantic.
- Ordinal analysis (Wolfram Pohlers, Münster)
It follows from the compactness theorem for first order logic that an infinite structure cannot be fully characterized by a set of first order sentences. Moreover Kurt Gödel has shown that for any sufficiently strong recursive axiom system for an infinite structure there is a sentence which is true in the structure but cannot be decided by the axiom system. So a first order axiom system can never grasp the whole structure.
By an ordinal analysis of an axiom system we try to measure its reach in terms of transfinite ordinals. This is customarily obtained by using calculi with infinitary inference rules for which the restrictions of the compactness theorem for first order logic do not apply. This mini–course will study the methods of infinitary proof theory on the example of an axiom system for the structure of natural numbers.
- Proof-Theoretic Semantics (Peter Schroeder-Heister, Tübingen, Luca Tranchini, Tübingen)
Proof-theoretic semantics is an alternative to truth-condition semantics. It is based on the fundamental assumption that the central notion in terms of which meanings are assigned to certain expressions of our language, in particular to logical constants, is that of proof rather than truth. In this sense proof-theoretic semantics is semantics in terms of proof, which also applies to the semantics of proofs. In the first half of the course, the general framework of proof-theoretic semantics including its background in general proof theory will be presented. In the second half we will deal with applications such as the proof-theoretic treatment of semantical and mathematical paradoxes, the treatment of (various forms of) negation and aspects of substructural logics.