Mathematische Logik
Zeit und Ort
Vorlesung: Mo,Mi 8-10, A027. Beginn: Montag 16. Oktober.Übung: Fr 8:30-10, A027. Beginn: Freitag 27. Oktober
Inhalt
Minimallogik und Einbettung der klassischen und intuitionistischen Logik. Gentzens Kalkül des natürlichen Schliessens. Semantik, Vollständigkeit der Prädikatenlogik erster Stufe. Grundlagen der Theorie der Berechenbarkeit, Churchsche These, Unentscheidbarkeit der Prädikatenlogik. Gödelsche Sätze über die Unvollständigkeit von Erweiterungen der elementaren Zahlentheorie.Skriptum
Das vollständige Skript mit Inhaltsverzeichnis, Bibliographie und Index finden Sie hier.Zum Logikkapitel gehört die Datei temp20231113.scm.
Übungen
Bitte melden Sie sich hier an. Übungsblätter werden in uni2work und ebenfalls an dieser Stelle veröffentlicht.ueb01,
ueb02, ueb02.scm (Lösungshilfe für Minlog-Aufgaben),
ueb03, ueb03.scm (Lösungshilfe für Minlog-Aufgaben),
ueb04, ueb04.scm (Lösungshilfe für Minlog-Aufgaben),
ueb05, ueb05.scm (Lösungshilfe für Minlog-Aufgaben),
ueb06, ueb06.scm (Lösungshilfe für Minlog-Aufgaben),
ueb07,
ueb08, ueb08.scm (Lösungshilfe für Minlog-Aufgaben),
ueb09,
ueb10,
ueb11,
ueb12.
Die Lösungen werden in der Übungsstunde präsentiert. Dort werden auch die korrigierten Übungsblätter verteilt; danach können sie im B414 abgeholt werden. Abgabe wahlweise elektronisch oder physisch (in der Vorlesung). Gemeinsame Lösungen sind zugelassen.
Sprechstunden
- Nils Köpp [koepp[at]math.lmu.de], Mi 11-12, B414.
- Philippe Vollmuth [ph.vollmuth[at]campus.lmu.de], B414. Bitte anmelden.
- Helmut Schwichtenberg, Mi 13-14, B434.
Literatur
- Schwichtenberg/Wainer, Proofs and Computations. Cambridge 2012
- Troelstra/Schwichtenberg, Basic Proof Theory. Cambridge 2000
- van Dalen, Logic and Structure. Berlin 1980
- Ebbinghaus, Flum, Thomas, Einführung in die mathematische Logik. Darmstadt 1978
- Shoenfield, Mathematical Logic. Reading 1967
Minlog
Viele Teile der in der Vorlesung entwickelten Theorie sind in dem Beweisassistenten Minlog implementiert. In einigen Übungsaufgaben wird die Möglichkeit geboten, dies in einfachen Fällen auszuprobieren. Die Verwendung von Minlog ist ein Zusatzangebot (also kein Gegenstand der Prüfung). Über Minlog kann man sich in dem mitgelieferten Tutorium informieren. Eine ausführliche Einführung (von Franziskus Wiesnet) ist hier. Falls git auf Ihrem Rechner installiert ist, können Sie die jeweils aktuelle Version von Minlog erhalten durch Ausführen vongit clone http://www.math.lmu.de/~minlogit/git/minlog.git.
Bitte arbeiten Sie mit dem dev-Zweig (durch Ausführen von git checkout dev). Eine konkrete Einführung (von Nils Köpp) ist ueb00.scm.
Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert. Um die CIP-Pools benutzen zu können brauchen die Studierenden eine entsprechende Kennung. Um eine Kennung zu erhalten ist die vollständige Teilnahme an einem ca. einstündigen Einführungskurs zwingende Voraussetzung. Sie können sich hier für einen Kurs anmelden.
Minlogpad (von Valentin Herrmann) erlaubt das Arbeiten mit Minlog ohne das System zu installieren.
Um sich über Minlog auszutauschen, Fragen zu stellen oder auch Fragen zu beantworten, können Sie der Minlog Community auf Zulip (minlog.zulipchat.com) beitreten. Zulip läuft direkt im Browser, ist aber auch als Desktopanwendung oder App erhältlich. In der Community können Sie beispielsweise im #questions Stream Fragen stellen und andere Minlognutzer dabei unterstützen, ihre Wissenslücken zu schliessen.
Prüfungsform
Es wird eine 2-stündige Klausur geschrieben. und zwar am Montag 26. Februar 2024, 09:00 - 11:00 Uhr im B138. Hilfsmittel (Bücher, Skripten etc.) sind in der Klausur nicht zugelassen; Schreibpapier wird gestellt. Bitte einen Lichtbildausweis mitbringen.Eine Nachklausur findet statt am Montag 18. März 2024, auch 09:00 - 11:00 Uhr im B138.
Die Klausur ist korrigiert und die Ergebnisse sind auf uni2work einsehbar. Eine Klausureinsicht ist möglich am Freitag, dem 1. März, 10:00-11:00 im Raum B414.