Bonn Mathematical Logic Group

Einführung in die Mathematische Logik  (V2A2)


Aktuelles:

Dozenten

Zeit und Ort

Ablauf

Die Vorlesung findet live zu den geplanten Zeiten via zoom statt. (Zoom-Link: siehe weiter oben.) Mindestens bis Pfingsten finden die Vorlesung und Übungen online statt.

Inhalt

Alle mathematischen Aussagen lassen sich durch Verknüpfungen und Quantoren als formale logische Aussagen schreiben. Zum Beispiel wird die Stetigkeit von Funktionen in der Analysis oft in einer epsilon-delta Schreibweise mit Quantorensymbolen definiert. Mathematische Beweise können als Folgen von Aussagen aufgefasst werden, die sich durch logische Schlüsse aus Axiomen ergeben. Dadurch können Beweise selbst mathematisch untersucht werden.

In dem Modul wird die logische Begründung der Mathematik durch Aussagen, Theorien und Beweise vorgestellt. Ein zentrales Ergebnis ist der Gödelsche Vollständigkeitssatz: `Wenn jedes Beispiel das A erfüllt auch B erfüllt, dann kann man aus A die Aussage B formal beweisen.

Ein wichtiges Thema ist die Unvollständigkeit von Axiomensystemen. Gödels Unvollständigkeitssätze zeigen, dass jede `sinnvolle' Axiomatisierung der natürlichen Zahlen manche Aussagen offen lässt.

Wir werden auch kurze Einleitungen in die Mengenlehre und Modelltheorie sehen. Die Mengenlehre bildet die Grundlage der Mathematik, und die Modelltheorie beschäftigt sich unter anderem mit Anwendungen der mathematischen Logik in der Algebra.

Wir möchten in den Übungsaufgaben konkrete Formalisierungen mit Hilfe von Natural Proof Checking (Software: Naproche) ansehen. Prof. Peter Koepke wird dazu im Rahmen der Vorlesung einen einleitenden Vortrag halten.

Die wichtigsten Informationen zur Vorlesung finden sie in diesem Überblick.

Formale Beweise in Naproche

In der mathematischen Logik wird gezeigt, dass mathematisches Formulieren und Beweisen durch formale Sprachen und durch syntaktisches Operieren in diesen Sprachen erfasst werden kann. Durch die praktische Implementation dieser Operationen gelangt man zu interaktiven Beweisassistenten, die das Schreiben und die logische Überprüfung formaler Texte unterstützen.

Ein Teil der Übungen zur Vorlesung sollen mit Hilfe des Beweisassistenten Naproche (Natural Proof Checking) bearbeitet werden, der in der Logik-Gruppe in Bonn entwickelt wird. Dazu installieren Sie bitte möglichst bald die Beweiserplattform Isabelle auf Ihrem Computer. Naproche wird als Komponente von Isabelle mitgeliefert. Besonderes Merkmal von Naproche ist eine Eingabesprache, die die übliche mathematische Sprache approximiert. Hier finden Sie eine Einführung in Naproche.

Vorkenntnisse

Die Vorlesung setzt Grundkenntnisse aus dem 1. Studienjahr Mathematik voraus.

Begleitseminar und andere Vorlesungen

Begleitend zur Vorlesung findet ein Hauptseminar über formale Mathematik und Mengenlehre statt.

Aufbauend auf der Vorlesung ist im Winter 2021 eine Vorlesung über Modelltheorie von Prof. Philipp Hieronymi geplant.

Vorlesungsthemen

Vorlesungsskript

Das Vorlesungsskript is nur auf eCampus verfügbar und wird vor jeder Vorlesung dort hochgeladen.

Übungen

Die Übungsblätter werden wöchentlich am Freitag (oder Wochenende) auf eCampus hochgeladen (Beginn: 16.04.). Die Deadline für die Abgabe auf eCampus ist Montags (eine runde Woche nach Ausgabe).
Sie können Ihre Lösungen in Gruppen von 3 Studenten abgeben. Getippte oder eingescannte Lösungen sind möglich.
Zur Teilnahme an der Klausur benötigen Sie insgesamt 60% der möglichen Punkte der Aufgaben ohne Naproche. Die Aufgaben zu Naproche zählen als Zusatzpunkte, mit denen Sie die 60% schneller erreichen können.

Klausur

Die Klausurtermine sind 31.07. und 21.09. Formale Beweise in Naproche werden in der Klausur nicht vorkommen.

Last changed: 02 Mai, 2021