Hilbert-Bernays Summer School on Logic and Computation 2017

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. 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) that are complemented with a historical excursus.


  • Term Rewriting Systems (Franz Baader, Dresden)
    The area of Term Rewriting Systems is an important branch of theoretical computer science that covers elements of logic and mathematics. Term Rewriting Systems can realize computations in structures defined by equality. They have important applications in automated reasoning, algebraic specification, and functional programming. This course introduces fundamental properties of Term Rewriting Systems such as termination and confluence; studies how these properties can effectively be verified; and finally describes how one can (sometimes) turn non-confluent systems into confluent ones by applying Knuth-Bendix completion.

  • 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.

  • Proof Theory and the Art of Ordinal Analysis (Michael Rathjen, Leeds)
    A central theme running through all the main areas of modern Mathematical Logic is the classification of sets, functions, theories or models, by means of transfinite hierarchies whose ordinal levels measure their "rank" or "complexity" in some sense appropriate to the underlying context. Such hierarchy classifications differ widely of course, in their modes of construction and their intended application, but they often provide the means to discover deep connections between areas which may on the surface seem quite unrelated. In Proof Theory, from the work of Gentzen in the 1930's up to the present time, this central theme is manifest in the assignment of "proof theoretic ordinals" to theories, measuring their "consistency strength" and "computational power", and providing a scale against which those theories may be compared and classified. In this course we present the foundations of proof theory and its ordinal-theoretic orientation.

  • Geometric Logic - Topos Theory (Ulrich Stuhler, Göttingen)
    The categories of set valued presheaves or sheaves on a topological space form a so called topos, which can also be seen as a kind of generalized set theory with a variable basis. This rather flexible approach offers many new viewpoints and in particular allows to construct new interesting models of set theory. Using these concepts it is also possible to give a simpler line of arguments towards the results of P. Cohen and others on the continuum hypothesis and other foundational results. Here the constructions brought together in the "sheafication process" allow to make the relevant proofs more transparent.