The summer school was addressed at students of mathematics, philosophy, computer science and other subjects that are related to mathematics with basic knowledge in logics. The summer school conveyed insight into current research topics in the areas of logics and computability. The scientific program consisted of mini courses (with lectures, exercises and projects) that were complemented with a historical excursus.

Schedule for download (PDF), list of projects and presentations

**Mini-courses**

*Gödel's Incompleteness Theorems*(Reinhard Kahle, Lisbon/Tübingen)

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.*Recursion and Complexity*(Isabel Oitavem, Lisbon)

Computability theory provides us with theoretical results about what can be computed. However, just a fraction of the theoretically computable functions can be implemented through efficient algorithms. Complexity theory addresses this question, usually using machine models, like the Turing machine, and explicit bounds. In contrast, implicit characterizations of complexity classes avoid both machines and explicit complexity conditions and therefore allow a more mathematically description of complexity classes. In this minicourse different characterisations of complexity classes based on recursive schemes will be discussed.*Ordinal Analysis*(Wolfram Pohlers, Münster)

It follows from Gödel's Incompleteness Theorems that there is no axiom system which completely describes the standard structure of the natural numbers. The same holds for other standard structures, e.g. of the constructable set universe. Note that Gödel's Theorem only proves the existence of a theorem which is true in the standard structure but cannot be decided within the axiom system. In contrast, ordinal analysis, introduced by Gentzen, aims to determine the "amount of transfiniteness" of a given axiom system. This amount can be measured in terms of transfinite ordinal numbers. This minicourse is designed as introduction to infinitary methods of proof applying infinitary calculus to ordinal analysis.*Automatic Reasoning in the Automobile Industry*(Wolfgang Küchlin, Tübingen)

In recent years, important practical advances have been achieved in the reasoning method of Boolean Satisfiability Solving (SAT-Solving). This has made industrial applications possible, e.g. in the fields of microelectronic circuit verification, software verification, or for solving configuration problems. In this course we first present the algorithmic foundations of current SAT-Solvers, then we give an introduction to configuration problems in the automobile industry, and finally we show how they can be formulated as SAT problems and solved efficiently. On this example, students will be exposed to the application of Logic in an industrial context.*Hilbert and Bernays in Göttingen*(Ulrich Stuhler, Göttingen)

Göttingen is the place where Hilbert and Bernays have laid out the foundations of arithmetic. Their collaboration culminated in the two volume work "Grundlagen der Mathematik". This course is reminiscent of this historical development.