Hilbert Bernays Summer School on Logic and Computation 2016

Die Sommerschule richtet sich an Studierende der Mathematik, Philosophie, Informatik und anderer mathematik-naher Disziplinen mit Grundkenntnissen in Logik. Die Sommerschule vermittelt Einblicke in aktuelle Forschungsthemen in den Gebieten Logik und Berechenbarkeit. Das wissenschaftliche Programm besteht aus Minikursen (mit Vorlesungen, Übungen und Projekten), die durch einen historischen Exkurs ergänzt werden.

Mini-courses



  • From Hilbert to Gentzen and beyond (Reinhard Kahle, Lisbon)
    In this course, both the mathematical and the philosophical ideas behind Hilbert's programme are introduced. Then it will be explained how Gentzen developed modern proof theory from Gödel's results. Finally, contemporary questions about mathematical and philosophical aspects of proof theory are discussed.


  • Proof mining (Ulrich Kohlenbach, Darmstadt)
    In the 1950's Georg Kreisel suggested to apply proof-theoretic transformations to concrete (ineffective) proofs in order to gain additional (new) information. In recent years this approach has successfully been applied to nonlinear analysis. Typically, methods used here are extensions and/or adaptations of Gödel's functional interpretation ("Dialectica interpretation").


  • lambda-calculus (Simona Ronchi della Rocca, Turin)
    Originally developed as logical system, lambda-calculus nowadays serves as base of virtually all functional programming languages. In this course both, the logical background as well as programming techniques are discussed.


  • Computational contents of proofs (Helmut Schwichtenberg, Munich)
    A constructive proof of a formula A can be considered as a solution of the problem given by A. Such a solution is a computable function of a type determined by A. We present a theory of "realisation", based on Gentzen's calculus of natural deduction, and an implemented "proof assistant" which allows to extract computational content from formalized proofs.