Mathematische Logik
Zeit und Ort
Vorlesung: Mo,Mi 8:30-10, A027. Ü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.
- Aufbau des Zahlensystems.
Skriptum
1. Logic. 03-22 (Stand 3. November 2025).Übungen
Bitte melden Sie sich hier an. Übungsblätter werden in uni2work und ebenfalls an dieser Stelle veröffentlicht.ueb01, hwk01.
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).
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 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.
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 executinggit 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.