Zur erfolgreichen Belegung des Moduls benötigt man lediglich eine gewisse mathematische Reife und das Interesse, über mathematische Argumente mathematisch nachzudenken. Im letzten Teil der Vorlesung sind Grundkenntnisse in Kategorientheorie nötig, wie sie etwa durch die parallel stattfindende Vorlesung von Marc Nieper-Wißkirchen oder durch vergangene Pizzaseminar bereitgestellt werden.
Was genau liefert ein Beweis mehr als nur die Information, dass die bewiesene Aussage stimmt? Was hat man davon, wenn man auf das Axiom, jede Aussage sei wahr oder falsch, verzichtet?
In dieser Vorlesung möchten wir mathematische Beweise als eigenständige mathematische Objekte behandeln und von einem höheren Standpunkt aus betrachten. Das ist mit Gentzens Kalkül natürlichen Schließens möglich, welches erlaubt, informale Argumente zu formalisieren. Damit ausgerüstet können wir präzise untersuchen, auf welchen logischen Prinzipien gegebene Beweise beruhen.
Wir lernen intuitionistische Logik kennen, bei der das Prinzip vom ausgeschlossenen Dritten ("jede Aussage stimmt oder stimmt nicht") nicht verwendent wird, und verstehen Gödels Unvollständigkeitssatz, welcher in erster Näherung besagt, dass es wahre Aussagen gibt, die nicht beweisbar sind.
Anschließend behandeln wir Realisierbarkeitstheorie. Damit können wir eine Verbindung zwischen Logik und Berechenbarkeitstheorie aus der theoretischen Informatik herstellen und einsehen, in welchem Sinn gewisse Prinzipien gelten, die in klassischer Mathematik schlichtweg falsch sind: etwa die Behauptung, dass jede Funktion ℝ → ℝ stetig sei. Das werden wir nutzen, um proof mining zu betreiben: aus gegebenen Beweisen weitere Informationen wie obere Schranken zu extrahieren. Dies werden wir mit Anwendungen in der Analysis und Numerik beleuchten.
Schließlich erkunden wir die interne Sprache von Topoi, mathematischen Alternativuniversen, in denen nicht die üblichen Gesetze der Logik gelten. Wir werden sehen, wie man diese in Geometrie und Algebra gewinnbringend einsetzen kann. Auch der effektive Topos, der ein weiteres Bindeglied zur theoretischen Informatik darstellt und Realisierbarkeitstheorie gewissermaßen vergegenständlicht, wird thematisiert werden.
