Mathematische Logik
Zeit und Ort
Vorlesung: Mo,Mi 8-10, A027. Übung: Fr 8:30-10, A027.Inhalt
- Minimallogik und Einbettung der klassischen und intuitionistischen Logik. Gentzens Kalkül des natürlichen Schliessens.
- 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, Vollständigkeit der reellen Zahlen. Dabei Einsatz des Beweisassistenten Minlog.
Skriptum
Der aktuelle Stand wird hier veröffentlicht.Übungen
Bitte melden Sie sich hier an. Übungsblätter werden in uni2work und ebenfalls an dieser Stelle veröffentlicht.Die Lösungen werden in der Übungsstunde präsentiert.
Sprechstunden
- Valentin Herrmann. 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.
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.