Mathematische Logik
Zeit und Ort
Vorlesung: Mo,Mi 8:30-10, A027.
Am 2. Februar fällt die Vorlesung aus.
Übung: Fr 8:30-10, A027.
Beginn: Freitag 17. 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.
Übungen
Bitte melden Sie sich
hier an.
Übungsblätter werden in uni2work und ebenfalls an dieser Stelle
veröffentlicht.
ueb02,
hwk02,
ueb02.scm (Lösungshilfe für Minlog-Aufgaben),
Link für
Minlogweb,
ueb03,
hwk03,
ueb03.scm (Lösungshilfe für Minlog-Aufgaben),
drinker.scm (Minlog-Demo),
ueb04,
hwk04,
ueb04.scm (Lösungshilfe für Minlog-Aufgaben),
ueb05,
hwk05,
ueb05.scm (Lösungshilfe für Minlog-Aufgaben),
ueb06,
hwk06,
ueb06.scm (Lösungshilfe für Minlog-Aufgaben),
ueb07,
hwk07,
ueb07.scm (Lösungshilfe für Minlog-Aufgaben),
ueb08,
hwk08,
ueb08.scm (Lösungshilfe für Minlog-Aufgaben),
ueb09,
hwk09,
ueb09.scm (Lösungshilfe für Minlog-Aufgaben),
ueb10,
hwk10,
ueb10.scm (Lösungshilfe für Minlog-Aufgaben),
ueb11,
hwk11,
ueb11.scm (Lösungshilfe für Minlog-Aufgaben),
ueb12,
hwk12,
ueb12.scm (Lösungshilfe für Minlog-Aufgaben),
ueb13, hwk13, ueb13.scm (Lösungshilfe für Minlog-Aufgaben).
Die Lösungen werden in der Übungsstunde präsentiert.
Sprechstunden
- Luis Gambarte. Bitte anmelden, gambarte[at]math.lmu.de
- Valentin Herrmann. Bitte anmelden, valentin.herrmann[at]math.lmu.de, B414.
- Helmut Schwichtenberg, Mi 13-14, B434.
- Katharina Wendler. Bitte anmelden, Wendler.Katharina[at]campus.lmu.de
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 von
git 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.
Minlogweb (von Valentin Herrmann) erlaubt das bequeme Arbeiten mit Minlog im Browser. Eine Alternative mit gleichem Ziel ist Minlogpad. Minlogpad hat zwar mehr Features, ist aber auch wesentlich schwerer zu benutzen und benötigt eine Internetverbindung.
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.
Minlog (english)
Many parts of the theory developed in the lecture course are implemented
in the proof assistant Minlog. In some homework problems this
can be tried in simple cases. Information on
Minlog
is available in the tutorial which is part of the package. A detailed
introduction (by Franziskus Wiesnet) is
here. If git is installed on your computer you may
download the current version of Minlog by executing
git clone http://www.math.lmu.de/~minlogit/git/minlog.git.
Please work with the dev branch (git checkout dev). A concrete introduction
(by Nils Köpp) is
ueb00.scm.
Minlogweb (by
Valentin Herrmann) allows to work conveniently with Minlog in a browser.
An alternative with the same goal is
Minlogpad.
It has more features, but is not as easy to work with and needs
an internet connection.
To chat on Minlog, ask questions or answer them you can join the Minlog
community on Zulip (minlog.zulipchat.com). Zulip runs directly in a browser
but is also available as a desktop application or as an app. In the community
you may ask questions in the #questions stream and may help others.
Prüfungsform
Mündliche Prüfung am Montag, dem 23. Februar 2026.
Ein Nachholtermin wird am Anfang des Sommersemesters angeboten, voraussichtlich
am Montag dem 13.\ April 2026 ab 12:00.
Studienordnungen
Die Vorlesung (mit Übung) kann unter WP 6 (Ausgewähltes Thema der reinen Mathematik) in der Bachelorstudienordnung Mathematik (2021) mit 9 ECTS Punkten angerechnet werden.
Letzte Änderung
4. Februar 2026