Einführung in die Mathematische Logik (V2A2)
- Doodle für neuen Termin der Donnerstags-Übung: https://doodle.com/poll/wwmnvmb5ee2dkk4q#calendar . Bitte füllen Sie das Doodle aus, auch wenn Ihnen der jetzige Termin passt! Danke.
- Das Skript zur Vorlesung ist ab heute nur auf eCampus verfügbar. Die Videos werden heute auf eCampus verlinkt.
- Slides zur Einfüuhrung in formale Beweise in Naproche sind auf eCampus verfügbar.
- Help Desk für Studentinnen im Bachelor- und Master-Studium: http://www.hcm.uni-bonn.de/de/gender-equality/
Dozenten
-
PD Dr.
Philipp Schlicht
- Übungen: Adrian De Lon, Moritz Hartlieb, Sebastian Meyer, Thomas v. Campenhausen
Zeit und Ort
-
Vorlesung:
- Montags 14:15-16:00
- Mittwochs 13:30-15:00
-
Übungen:
- Montags 08:15-10:00, Thomas v. Campenhausen
- Dienstag 12:15-14:00, Moritz Hartlieb
- Freitag 14:15-16:00, Sebastian Meyer
-
Tutorial zu formalen Beweisen in Naproche
- Donnerstag 16:15-18:00, Adrian De Lon
-
Sprechstunde Philipp Schlicht:
- Montags 16:00-16:45
- Mittwochs 15:00-15:45
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
- Strukturen und Formeln
- Prädikatenlogik
- Ordinal- und Kardinalzahlen
- Transfinite Induktion
- Hilberts Beweiskalkül
- Vollständigkeit des Beweiskalküls (Gödel)
- Kompaktheitssatz und Anwendungen
- Testen von formalen Beweisen mittels Naproche in den Übungen
- Gödels erster Unvollständigkeitssatz
- Satz von Löwenheim-Skolem
- Axiomatisierbare Klassen von Strukturen
- Quantorenelimination
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.