Logbuch zur Vorlesung Logik in der Informatik
Wintersemester 2009/2010

 

Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden sowie gelegentlich ergänzende Bemerkungen.

  1. Di, 13.10.2009:
    Einführung ins Thema und Klärung von Organisatorischem. Definition der Begriffe "Signatur" und "Struktur"; viele Beispiele für Strukturen; Festlegung einiger Notationen; Definition des Begriffs "Isomorphismus"; Beispiele für Isomorphismen.
    Material: Einführung ins Thema sowie Kapitel 1, Seiten 1–12
    Weitere Lektüre: 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.

  2. Do, 15.10.2009:
    Syntax und Semantik der Logik erster Stufe; Beispiele.
    Material: Kapitel 1, Seiten 13–30.
    Weitere Lektüre: Kapitel 2 und Kapitel 3.2, 3.3 und 3.6 in [EFT].

  3. Di, 20.10.2009:
    Koinzidenzlemma; Isomorphielemma; Äquivalenz und Folgerung; Substitutionen. Übungsblatt 1 ausgeteilt.
    Material: Kapitel 1, Seiten 30–37 und Kapitel 2, Seiten 38–44.
    Weitere Lektüre: 3.4, 3.5 und 3.8 in [EFT].

  4. Do, 22.10.2009:
    Substitutionslemma; pränexe Normalform; termreduzierte Formeln.
    Material: Kapitel 2, Seiten 44–55.
    Weitere Lektüre: Kapitel 3.8, 8.1 und 8.4 in [EFT].

  5. Di, 27.10.2009:
    Relationale Signaturen; Auswertungskomplexität der Logik erster Stufe auf endlichen Strukturen. Übungsblatt 2 ausgeteilt.
    Material: Kapitel 2, Seiten 55-60 und Kapitel 3, Seiten 60.1-60.7.
    Weitere Lektüre: Kapitel 4.2 und 4.3 in [FG], Kapitel 6.1 und 6.2 in [L].

  6. Do, 29.10.2009:
    EF-Spiele: Spielgregeln, Gewinnbedingung, Gewinnstrategien, viele Beispiele.
    Material: Kapitel 4, Seiten 61-69.
    Weitere Lektüre: Kapitel 3.2 in [L] sowie Kapitel 2.1 bis 2.3 in [EF].

  7. Di, 03.11.2009:
    Das EF-Spiel auf zwei linearen Ordnungen; der Satz von Ehrenfeucht; Folgerungen aus dem Satz von Ehrenfeucht; Vorarbeiten zum Beweis des Satzes von von Ehrenfeucht (Hintikka-Formeln). Übungsblatt 3 ausgeteilt.
    Material: Kapitel 4, Seiten 69-79.
    Weitere Lektüre: Kapitel 3.1 bis 3.4 in [L] sowie Kapitel 2.1 und 2.2 in [EF].

  8. Do, 05.11.2009:
    Beweis des Satzes von von Ehrenfeucht; Gewinnstrategien für Spoiler.
    Material: Kapitel 4, Seiten 80-88
    Weitere Lektüre: Kapitel 3.5 und 3.6 in [L], sowie Kapitel 2.2 und 2.3 in [EF].

  9. Di, 10.11.2009:
    Logische Reduktionen; der Satz von Hanf; Beginn des Beweises des Satzes von Hanf. Übungsblatt 4 ausgeteilt.
    Material: Kapitel 4, Seiten 88-99.
    Weitere Lektüre: Kapitel 3.6 und 4.1 bis 4.3 in [L], Kapitel 8.2 in [EFT], sowie Kapitel 2.4 in [EF].

  10. Do, 12.11.2009:
    Schluss des Beweises des Satzes von Hanf; Hanf-Lokalität der Logik erster Stufe; Vorarbeiten zum Satz von Fraïssé.
    Material: Kapitel 4, Seiten 100-109.
    Weitere Lektüre: Kapitel 4.1 bis 4.3 in [L] sowie Kapitel 2.3 und 2.4 in [EF].

  11. Di, 17.11.2009:
    Beweis des Satzes von Fraïssé; Beispiel-Anwendung des Satzes von Fraïssé; Vorarbeiten zum Satz von Gaifman. Übungsblatt 5 ausgeteilt.
    Material: Kapitel 4, Seiten 109-113 und Kapitel 5, Seiten 114-121.
    Weitere Lektüre: Kapitel 2.3 und 2.5 in [EF] sowie Kapitel 3.5 in [L].

  12. Do, 19.11.2009:
    Gaifman-Normalform; Formulierung und Beginn des Beweises des Satzes von Gaifman (bis Seite 134).
    Material: Kapitel 5, Seiten 122-134
    Weitere Lektüre: Kapitel 2.5 in [EF] sowie Gaifmans Originalarbeit [Gaifman].

  13. Di, 24.11.2009:
    Abschluss des Beweises des Satzes von Gaifman; Gaifman-Lokalität der Logik erster Stufe; Formulierung des Satzes von Seese über Klassen von Graphen von beschränktem Grad. Übungsblatt 6 ausgeteilt.
    Material: Kapitel 5, Seiten 134-148
    Weitere Lektüre: Kapitel 2.5 in [EF] sowie Kapitel 4.1 bis 4.3, 4.5 und 6.6 in [L].

  14. Do, 26.11.2009:
    Beweis des Satzes von Seese über Klassen von Graphen von beschränktem Grad, eine untere Schranke für Formeln in Gaifman-Normalform, Vorarbeiten zum Satz von McNaughton und Papert.
    Material: Kapitel 5, Seiten 148-162 und Kapitel 6, Seiten 163-166.
    Weitere Lektüre: Kapitel 6.6 und 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.

  15. Di, 01.12.2009:
    Der Satz von McNaughton und Papert. Beginn mit Kapitel 7: Der Vollständigkeitssatz; heute: Beweiskalküle. Übungsblatt 7 ausgeteilt.
    Material: Kapitel 6, Seiten 166-177 und Kapitel 7, Seiten 202-203.
    Weitere Lektüre: Kapitel 7.5 in [L], Kapitel 6.4 in [EF] und Kapitel 4.1 in [EFT].

  16. Do, 03.12.2009:
    Beweiskalküle, ein Sequenzenkalkül für die Logik erster Stufe, Korrektheit des Sequenzenkalküls.
    Material: Kapitel 7, Seiten 203-219.
    Weitere Lektüre: Kapitel 4 in [EFT].

  17. Di, 08.12.2009:
    ableitbare Regeln im Sequenzenkalkül; Widerspruchsfreiheit.
    Material: Kapitel 7, Seiten 219-231.
    Weitere Lektüre: Kapitel 4 in [EFT].

  18. Do, 10.12.2009:
    Widerspruchsfreiheit; das syntaktische Endlichkeitslemma; Formulierung des Vollständigkeitssatzes; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas; Termininterpretationen; eine Kongruenzrelation.
    Material: Kapitel 7, Seiten 232-245.
    Weitere Lektüre: Kapitel 4 und 5 in [EFT].

  19. Di, 15.12.2009:
    die reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; der Satz von Henkin
    Material: Kapitel 7, Seiten 246-259.
    Weitere Lektüre: Kapitel 5 in [EFT].

  20. Do, 17.12.2009:
    Beweis des Erfüllbarkeitslemmas und Abschluss des Beweises des Vollständigkeitssatzes.
    Beginn mit Kapitel 8: der Kompaktheitssatz (bzw Endlichkeitssatz); die Begriffe Modellklasse, Axiomatisierbarkeit, endliche Axiomatisierbarkeit; Axiomatisierbarkeit der Klasse aller unendlichen Strukturen; Nicht-Axiomatisierbarkeit der Klasse aller endlichen Strukturen.
    Material: Kapitel 7, Seiten 260-265 und Kapitel 8, Seiten 266-272.
    Weitere Lektüre: Kapitel 5 und 6 in [EFT].

  21. Di, 12.01.2010:
    Nicht-Axiomatisierbarkeit der Klasse aller zusammenhängenden Graphen; der Satz von Löwenheim und Skolem; elementare Äquivalenz und Nichtstandardmodelle der Arithmetik.
    Material: Kapitel 8, Seiten 272-281.
    Weitere Lektüre: Kapitel 6 in [EFT].

  22. Do, 14.01.2010:
    Abschluss von Kapitel 8: der Satz von Skolem; ein alternativer Beweis dafür, dass es keinen FO-Satz gibt, der von genau denjenigen endlichen geordneten Strukturen erfüllt wird, deren Länge gerade ist (ein Beweis von Martin Otto, der nur auf den in Kapitel 7 und 8 erarbeiteten Methoden beruht, ohne Rückgriff auf EF-Spiele).
    Material: Kapitel 8, Seiten 272-286 sowie 283.1-283.8.
    Weitere Lektüre: Kapitel 6.4 in [EFT] sowie Martin Ottos Artikel "Model theoretic methods for fragments of FO and special classes of (finite) structures" (das in Bemerkung 8.19 und 8.20 vorgestellte Material findet sich auf Seite 17 des Artikels).

  23. Di, 19.01.2010:
    Beginn mit Kapitel 9: Die Grenzen der Berechenbarkeit: Entscheidbarkeit und rekursive Aufzählbarkeit; die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln; Gödelisierung von FO[σAr]
    Material: Kapitel 9, Seiten 287-299
    Weitere Lektüre: Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].

  24. Do, 21.01.2010:
    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.
    Material: Kapitel 9, Seiten 300-312.
    Weitere Lektüre: Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].

  25. Di, 26.01.2010:
    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; Vorarbeiten zum Satz von Trakhtenbrot (Трахтенброт).
    Material: Kapitel 9, Seiten 313-325.1
    Weitere Lektüre: Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].

  26. Do, 28.01.2010:
    der Satz von Trakhtenbrot (Трахтенброт); Folgerungen aus dem Satz von Trakthenbrot; Ordnungsinvarianz.
    Material: Kapitel 9, Seiten 325.2-325.16.
    Weitere Lektüre: Kapitel 10 in [EFT]; Kapitel 9.1 sowie 5.1 und 5.2 in [L]; Kapitel 7.2.1 in [EF].

  27. Di, 03.02.2010:
    Theorien und Axiomatisierbarkeit; die Minimale Arithmetik; Formulierung von Gödels erstem Unvollständigkeitssatz; der Σ1-Transfersatz.
    Material: Kapitel 10, Seiten 326-337.
    Weitere Lektüre: Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].

  28. Do, 05.02.2010:
    Repräsentierbarkeit von Relationen und Funktionen; Satz über die Repräsentierbarkeit (in Q) der berechenbaren Funktionen und der entscheidbaren Relationen; der Fixpunktsatz; Satz über die Unmöglichkeit der Selbstrepräsentierbarkeit
    Material: Kapitel 10, Seiten 338-355.
    Weitere Lektüre: Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].

  29. Di, 09.02.2010:
    der Satz von Tarski über die Nichtdefinierbarkeit der Wahrheit; die Unentscheidbarkeit der minimalen Arithmethik; die Unentscheidbarkeit der Menge aller allgemeingültigen FO[&sigmaAr]-Sätze; Beweis von Gödels erstem Unvollständigkeitssatz; die Existenz von Gödelsätzen.
    Material: Kapitel 10, Seiten 356-365.
    Weitere Lektüre: Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].

  30. Do, 11.02.2010:
    Hilberts Programm; 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 2010.
    Material: Kapitel 10, Seiten 366-379
    Weitere Lektüre: Kapitel 15-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 und 236 in [BBJ].

 

Last modified: 02/11/2010 17:56:02
Nicole Schweikardt