Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der
einzelnen Vorlesungsstunden sowie gelegentlich ergänzende Bemerkungen.
Di, 25.10.2011
Eröffnungsveranstaltung.
Einführung ins Thema und Klärung von Organisatorischem. Definition
der Begriffe "Signatur" und "Struktur"; Beispiele für
Strukturen; Festlegung einiger Notationen; Definition des Begriffs
"Isomorphismus"; Beispiele für Isomorphismen.
Kapitel 1 und Kapitel 3.1 in [EFT]. Einen Überblick über die
Rolle der Logik in der Informatik gibt [HHIKVV]; der Artikel
ist
online hier
verfügbar.
Einen Einblick in die Geschichte der logischen Grundlagen der
Mathematik gibt der
Comic [Logicomix];
weitere Informationen dazu finden Sie hier.
Do, 27.10.2011, 14h15-15h45
Syntax und Semantik der Logik erster Stufe; Beispiele.
Auswertungskomplexität der Logik erster Stufe auf endlichen
Strukturen; Spielregeln des Ehrenfeucht-Fraisse Spiels (kurz:
EF-Spiel); Beispiele zum EF-Spiel.
Übungsblatt 2 ausgeteilt.
Kapitel 4.2 und 4.3 in [FG],
Kapitel 6.1, 6.2, 6.5 und 3.2 in [L].
Insbesondere enthält Kapitel 6.5
von [L] einen Beweis der PSPACE-Vollständigkeit des Auswertungproblems
für FO auf FIN.
Di, 08.11.2011
EF-Spiele: Gewinnbedingung, Gewinnstrategien, das EF-Spiel auf zwei linearen Ordnungen
Der Satz von Ehrenfeucht; Methode zum Nachweis, dass bestimmte Klassen von
Strukturen nicht FO-definierbar sind; Nachweis, dass die Klasse
aller endlichen linearen Ordnungen gerader Länge nicht
FO-definierbar ist
Übungsblatt 3 ausgeteilt.
Kapitel 2.5
in [EF],
Kapitel 4.1-4.3 und 4.5
in [L].
Do, 01.12.2011
Beweis und Anwendungen der Gaifman-Lokalität der Logik erster
Stufe;
der Satz von Seese über das Auswertungsproblem der Logik erster
Stufe auf Klassen von Graphen von beschränktem Grad
Übungsblatt 6 ausgeteilt.
Anwendungen des Satzes von Seese über das Auswertungsproblem der Logik erster
Stufe auf Klassen von Graphen von beschränktem Grad;
eine untere Schranke für Formeln in Gaifman-Normalform;
Beginn des Beweises des Satzes von McNaughton und Papert
Kapitel 7.5
in [L].
Die Originalarbeit mit der unteren Schranke für Formeln in
Gaifman-Normalform finden
Sie hier;
eine Vorabversion ist
auch
hier erhältlich. Einen Überblick über so genannte
Algorithmische Metatheoreme finden
Sie hier.
Do, 08.12.2011
Abschluss des Beweises des Satzes von McNaughton und Papert;
Beweiskalküle; Sequenzen
Übungsblatt 7 ausgeteilt.
Kapitel 7.5
in [L],
Kapitel 6.4 in [EF] und Kapitel 4.1 in [EFT].
Di, 13.12.2011
Definition und Korrektheit des Sequenzenkalküls; Formulierung des
Vollständigkeitssatzes; Beispiele für Beweise im Sequenzenkalkül;
Ableitbare aussagenlogische Sequenzenregeln
Weitere ableitbare Sequenzenregeln: Quantorenaustauschregeln,
Gleichheitsregeln; Widerspruchsfreiheit; das syntaktische
Endlichkeitslemma; der Vollständigkeitssatz; Beweis des
Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas
Übungsblatt 8 ausgeteilt.
Terminterpretation und reduzierte Terminterpretation;
negationstreue Formelmengen; Formelmengen, die Beispiele
enthalten; Beginn des Beweises des Satzes von Henkin
Abschluss des Beweises des Satzes von Henkin; Beweis des
Erfüllbarkeitslemmas für abzählbare Signaturen; Abschluss des
Kapitels über den Vollständigkeitssatz
Übungsblatt 9 ausgeteilt.
Kapitel 5
in [EFT]. Ein
Beweis des Erfüllbarkeitslemma für
überabzählbare Signaturen findet sich in Kapitel 5.3 von [EFT].
Di, 10.01.2012
Der Kompaktheitssatz (Endlichkeitssatz); Axiomatisierbarkeit von Unendlichkeit;
Nicht-Axiomatisierbarkeit von Endlichkeit und
Graphzusammenhang; der Satz von Löwenheim und Skolem;
Nicht-Axiomatisierbarkeit von Überabzählbarkeit
Abschluss von Kapitel 8: Absteigender und aufsteigender Satz von
Löwenheim und Skolem; elementare Äquivalenz; Nichtstandardmodelle
der Arithmetik; der Satz von Skolem: ein abzählbares
Nichtstandardmodell der Arithmetik
Übungsblatt 10 ausgeteilt.
Beginn mit Kapitel 9: Die Grenzen der Berechenbarkeit:
Entscheidbarkeit, Semi-Entscheidbarkeit und rekursive
Aufzählbarkeit; die rekursive Aufzählbarkeit der allgemeingültigen
FO-Formeln; Gödelisierung von FO[σAr]
Die rekursive Aufzählbarkeit einiger definierbarer Zahlenmengen; FO-Definierbarkeit von Relationen und Funktionen; die Klasse Δ0 aller beschränkten FO[σAr]-Formeln;
das Lemma über die β-Funktion
Übungsblatt 11 ausgeteilt.
Turingmaschinen als formales Berechnungsmodell; die Klasse aller Σ1-Formeln; Beweis der
Σ1-Definierbarkeit aller TM-berechenbaren
partielle Funktionen und aller TM-rekursiv aufzählbaren
Relationen; die Unentscheidbarkeit der Theorie der Standardarithmetik
Übungsblatt 12 ausgeteilt.
Erfüllbarkeit und Allgemeingültigkeit im Endlichen; der Satz von Trakhtenbrot (Трахтенброт); Folgerungen aus dem Satz von Trakthenbrot; Ordnungsinvarianz.
Übungsblatt 12 ausgeteilt.
Kapitel 10 in [EFT]; Kapitel 9.1 sowie 5.1 und 5.2 in [L]; Kapitel 7.2.1 in [EF].
Di, 24.01.2012
Beginn mit Kapitel 10: Gödels Unvollständigkeitssätze:
Theorien und Axiomatisierbarkeit;
die Minimale Arithmetik;
Formulierung von Gödels erstem Unvollständigkeitssatz;
der Σ1-Transfersatz.
Repräsentierbarkeit von Relationen und Funktionen; Satz über die
Repräsentierbarkeit (in Q) der berechenbaren Funktionen und der
entscheidbaren Relationen; der Fixpunktsatz (hier zunächst noch
ohne Beweis); der Satz über die
Unmöglichkeit der Selbstrepräsentierbarkeit; der Satz von Tarski
über die Nichtdefinierbarkeit der Wahrheit; die
Unentscheidbarkeit der minimalen Arithmethik
Übungsblatt 13 ausgeteilt.
Beweis des Fixpunktsatzes; die Unentscheidbarkeit der Menge aller allgemeingültigen FO[&sigmaAr]-Sätze;
Beweis von Gödels erstem Unvollständigkeitssatz; die Existenz
von Gödelsätzen; Anmerkungen zu Hilberts Programm
Konsistenzsatz für T; die Peano-Arithmetik;
Gödels zweiter Unvollständigkeitssatz; der Satz von Löb.
Zusammenfassung der in der Vorlesung bzw. Übung behandelten Themen; Hinweise zur Prüfungsvorbereitung;
Ausblick auf das Seminar "Logik in der Informatik" im SoSe 2012.
Übungsblatt 14 ausgeteilt.
Kapitel 18
in [BBJ]
sowie Kapitel 10
in [EFT].
Eine ausführliche Erklärung des im Beweis des Satzes von Löb verwendeten Arguments finden Sie auf den Seiten 235-236 in [BBJ].