Hauptseminar Mathematische Logik (S2A2) - Formale Mathematik und Mengenlehre

Dozenten

• Prof. Dr. Peter Koepke
• Dr. Philipp Schlicht

Zeit und Ort

• Dienstag, 10.15-12.00 Uhr, online
• Beginn: 20.04.2021

Thema: Formale Mathematik und Mengenlehre
Link zu den Seminarsitzungen
Meeting ID: 711 725 4154, Passcode: Naproche
Zwei Einführungen in das System Naproche: Introduction, Tutorial
Weitere Links zu Naproche

Vorträge

• 20.04. Einleitung in Naproche, Peter Koepke: Formalize! (Vortrag)
  
• 27.04. Naproche-Formalisierung von Euklids Satz, Tim Lichtnau
• 04.05. Ordinalzahlen, Lisa Burgmeier
• 11.05. Auswahlaxiom, Tjark Sterk
• 18.05. Kardinalzahlen und Alephs, Maximilian Keßler
• 08.06. Kardinalzahlarithmetik und Mostowski-Satz (Teil 1), Carl Jacobsen
• 15.06. Kardinalzahlarithmetik und Mostowski-Satz (Teil 2), Matthias Franz
• 22.06. Konfinalität bis Satz von König, Josia Pietsch
• 29.06. Verallgemeinerte Kontinuumshypothese, Lucas Valle Thiele
• 06.07. Stationäre Mengen und Satz von Silver (Teil 1), Dmytro Solodovnichenko
• 13.07. Stationäre Mengen und Satz von Silver (Teil 2), Carl Rueger

Inhalt

In der Vorlesung "Einführung in die Mathematische Logik" wird gezeigt, dass sich mathematische Beweise im Prinzip als endliche Folgen von vollkommen formalen symbolischen Aussagen führen lassen, die durch einfache syntaktische Umformungen auseinander hervorgehen. Die Formale Mathematik entwickelt Software-Systeme, mit denen diese prinzipielle Möglichkeit praktisch umgesetzt werden kann; die damit interaktiv erstellten formalen Beweise sind absolut vollständig und korrekt im Sinne der Umformungsregeln. Mit derartigen "Beweis-Assistenten" kann man seit einigen Jahren auch anspruchsvolle Theoreme bis hin zur aktuellen Forschungsmathematik formalisieren.
An der Universität wird der Beweis-Assistent "Naproche" (Natural Proof Checking) entwickelt, bei dem die formale Eingabesprache zugleich Teil der natürlichen mathematischen Sprache ist. Naproche- Formalisierungen sind damit normal lesbare mathematische Texte. Eine aktuelle Vorversion von Naproche findet sich als Teil der Beweiser-Plattform Isabelle.
In dem Seminar wollen wir zunächst das System Naproche kennenlernen. Anschließend bilden die Seminarvorträge eine Einführung in die klassische Mengenlehre als Grundlage der modernen Mathematik, wobei begleitend Naproche-Formalisierungen von Grundbegriffe und ihren Eigenschaften diskutiert und eventuell auch selbst erstellt werden. Die mengentheoretischen Vorträge folgen (einem Anfangsstück) des Skriptums Set Theory.