01301 Klassische Prädikatenlogik |
Dieser Kurs wendet sich an Studenten mit Hauptfach Mathematik oder Informatik vom 2. Studienjahr an.
Er setzt keine konkreten mathematischen Vorkenntnisse voraus, wohl aber eine gewisse Bekanntschaft mit mathematischen Schlussweisen.
Einleitend wird die Sprache, Semantik (Gültigkeitsbegriff) und Syntax (Herleitungsbegriff) der Prädikatenlogik dargestellt.
Auf ein systematisches Studium der Syntax in Gestalt eines schnittfreien Sequenzenkalküls folgen
zwei methodisch sehr verschiedene Beweise des Vollständigkeitssatzes,
mit dem die Äquivalenz von Gültigkeit und Herleitbarkeit etabliert wird.
Daran schließen grundlegende Ergebnisse der Modelltheorie an: Der Kompaktheitssatz, die Löwenheim-Skolem-Satzgruppe
sowie der Satz von Los und Tarski über offene Axiomatisierbarkeit.
Auf dieser Basis führen wir in die Modelltheorie spezieller Theorien wie der Theorie der dichten linearen Ordnungen
und der Zahlentheorie der ersten und zweiten Stufe ein.
Besonderes Gewicht erhält das Kapitel zur Beweistheorie der Prädikatenlogik,
weil der hier verwendete schnittfreie Sequenzenkalkül besonders einfache und transparente Beweise
des Satzes von Herbrand und von Craigs Interpolations-Lemma und damit einer größeren Gruppe wichtiger Ergebnisse gestattet.
Als Thema aus der theoretischen Informatik untersuchen wir schließlich im gleichen sprachlichen Rahmen Kalküle
des automatischen Beweisens, besonders den Resolutionskalkül.
Allgemeine Informationen |
Kursautor | Justus Diller |
Betreuung | Prof. Dr. Reinhard Börger (E-Mail: Reinhard.Boerger@fernuni-hagen.de) |
Kursmaterial (nichtöffentlicher Bereich) |
Kurs Gesamtkurs |
Der Gesamtkurs liegt als PDF-Datei (KlassPraedlogik.pdf, ca. 2 MB) vor. Zum Ansehen und Ausdrucken der PDF-Datei benötigen Sie den Adobe Reader. Die Seitennummerierung entspricht nicht der gedruckten Fassung, außerdem hat Herr Diller einige Änderungen vorgenommen. |
Aktuell im Sommersemester 2006 |