Current entry

Logfile: Logik in der Informatik - Einführung in die formale Logik

Lecture  in Winter 2013/14

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


  1. Di, 15.10.2013
  2. 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".
    Material:
    Skript Kapitel 0: "Einleitung" und Kapitel 1: "Syntax und Semantik der Logik erster Stufe" bis inkl. Definition 1.8.
    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. Einen Einblick in die Geschichte der logischen Grundlagen der Mathematik gibt der Comic [Logicomix]; weitere Informationen dazu finden Sie hier.
  3. Do, 17.10.2013, 14h15-15h45
  4. Beispiele für Isomorphismen; Syntax und Semantik der Logik erster Stufe.
    Material:
    Skript Kapitel 1: "Syntax und Semantik der Logik erster Stufe" bis inkl. Definition 1.23.
    Weitere Lektüre:
    Kapitel 2 und Kapitel 3.2, 3.3 und 3.6 in [EFT].
  5. Do, 17.10.2013, 16h15-17h45
  6. Semantik der Logik erster Stufe; Beispiele; Koinzidenzlemma; Isomorphielemma; einführendes Beispiel zum Thema Substitutionen.
    Übungsblatt 1 ausgeteilt.
    Material:
    Skript Kapitel 1: "Syntax und Semantik der Logik erster Stufe" bis inkl. Beispiel 1.38.
    Weitere Lektüre:
    Kapitel 3.4, 3.5 und 3.8 in [EFT].
  7. Di, 22.10.2013
  8. Substitutionen; Substitutionslemma; Äquivalenz und Folgerung; pränexe Normalform.
    Material:
    Skript Rest von Kapitel 1: "Syntax und Semantik der Logik erster Stufe" sowie Kapitel 2: "Normalformen" bis inkl. Beispiel 2.5.
    Weitere Lektüre:
    Kapitel 3.8, 8.1 und 8.4 in [EFT].
  9. Do, 24.10.2013
  10. Pränexe Normalform; termreduzierte Formeln; relationale Signaturen; die Breite einer Formel.
    Übungsblatt 2 ausgeteilt.
    Material:
    Skript Rest von Kapitel 2: "Normalformen" und Kapitel 3: "Die Auswertungskomplexität von FO in endlichen Strukturen" Definition 3.7 und Beobachtung 3.8.
    Weitere Lektüre:
    Kapitel 3.8, 8.1 und 8.4 in [EFT].
  11. Di, 29.10.2013
  12. Die Auswertungskomplexität von FO in endlichen Strukturen; Spielregeln des Ehrenfeucht-Fraisse Spiels (kurz: EF-Spiel); partielle Isomorphismen; Beispiele zum EF-Spiel.
    Material:
    Kapitel 3: "Die Auswertungskomplexität von FO in endlichen Strukturen" und Kapitel 4: "Ehrenfeucht-Fraisse Spiele" bis inkl. Beispiel 3.3.
    Weitere Lektüre:
    Kapitel 4.2 und 4.3 in [FG], Kapitel 6.1, 6.2 und 6.5 von [L] (insbes. enthält Kapitel 6.5 einen Beweis der PSPACE-Vollständigkeit des Auswertungproblems für FO auf FIN), Kapitel 3.2 in [L], Kapitel 2.1 bis 2.3 in [EF].
  13. Do, 31.10.2013
  14. Gewinnstrategien; das EF-Spiel auf zwei linearen Ordnungen.
    Übungsblatt 3 ausgeteilt.
    Material:
    Kapitel 4 "Ehrenfeucht-Fraisse Spiele" bis inkl. Satz 4.11.
    Weitere Lektüre:
    Kapitel 3.2 in [L], Kapitel 2.1 bis 2.3 in [EF].
  15. Di, 05.11.2013
  16. 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.
    Material:
    Kapitel 4 (bis inkl. Satz 4.21).
    Weitere Lektüre:
    Kapitel 3.3, 3.4 und 3.5 in [L], Kapitel 2.1 bis 2.3 in [EF].
  17. Do, 07.11.2013
  18. Gewinnstrategien für Spoiler; logische Reduktionen; Nachweis, dass Graph-Zusammenhang und Erreichbarkeit nicht FO-definierbar sind; Vorarbeiten zum Satz von Hanf.
    Übungsblatt 4 ausgeteilt.
    Material:
    Kapitel 4 (bis inkl. Bemerkung 4.26).
    Weitere Lektüre:
    Kapitel 3.4, 3.6 und 4.1 in [L], Kapitel 2.1 bis 2.4 und 12.3 ("Logical Reductions") in [EF].
  19. Di, 12.11.2013
  20. Der Satz von Hanf.
    Material:
    Kapitel 4 "Ehrenfeucht-Fraisse Spiele" bis zum Ende des Beweises des Satzes von Hanf (d.h. Satz 3.28).
    Weitere Lektüre:
    Kapitel 4.1 bis 4.3 in [L], Kapitel 2.4 in [EF].
  21. Do, 14.11.2013
  22. Die Hanf-Lokalität der Logik erster Stufe; Hin- und Her-Systeme und der Satz von Fraisse.
    Übungsblatt 5 ausgeteilt.
    Material:
    Kapitel 4 "Ehrenfeucht-Fraisse Spiele" komplett.
    Weitere Lektüre:
    Kapitel 4.1-4.3 und 3.5-3.6 in [L], Kapitel 2.4 und 2.3 in [EF].
  23. Di, 19.11.2013
  24. Gaifman-Normalform und der Satz von Gaifman.
    Material:
    Kapitel 5 "Gaifman-Normalform" bis Seite 124.
    Weitere Lektüre:
    Kapitel 2.5 in [EF], Kapitel 4.1-4.3 und in [L].
  25. Do, 21.11.2013
  26. Beweis des Satzes von Gaifman.
    Übungsblatt 6 ausgeteilt.
    Material:
    Kapitel 5 "Gaifman-Normalform" bis Seite 137.
    Weitere Lektüre:
    Kapitel 2.5 in [EF], Kapitel 4.1-4.3 und 4.5 in [L].
  27. Di, 26.11.2013
  28. Die 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.
    Material:
    Kapitel 5 (bis Seite 150).
    Weitere Lektüre:
    Kapitel 4 und 6.6 in [L].
  29. Do, 28.11.2013, 14h15-15h45
  30. Beweis und 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; Vorarbeiten zum Satz von McNaughton und Papert.
    Material:
    Kapitel 5 (komplett) und Kapitel 6 (bis Seite 168).
    Weitere Lektüre:
    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.
  31. Do, 28.11.2013, 16h15-17h30
  32. Beweis des Satzes von McNaughton und Papert.
    Übungsblatt 7 ausgeteilt.
    Material:
    Kapitel 6 (komplett) und
    Weitere Lektüre:
    Kapitel 7.5 in [L], Kapitel 6.4 in [EF].
  33. Di, 03.12.2013
  34. Beweiskalküle; Sequenzen; Definition des Sequenzenkalküls und Nachweis der Korrektheit; Beispiele für Beweise im Sequenzenkalkül; Formulierung des Vollständigkeitssatzes; Ableitbare Regeln im Sequenzenkalkül.
    Material:
    Kapitel 7 (bis inkl. Definition 7.16)
    Weitere Lektüre:
    Kapitel 4 in [EFT].
  35. Do, 05.12.2013
  36. Ableitbare Sequenzenregeln; Widerspruchsfreiheit; das syntaktische Endlichkeitslemma; der Vollständigkeitssatz; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas.
    Material:
    Kapitel 7 (bis direkt vor Definition 7.29)
    Weitere Lektüre:
    Kapitel 4 in [EFT].
  37. Di, 10.12.2013
  38. Terminterpretation und reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; der Satz von Henkin.
    Übungsblatt 8 ausgeteilt.
    Material:
    Kapitel 7 (bis zum Ende des Beweises des Satzes von Henkin)
    Weitere Lektüre:
    Kapitel 5 in [EFT].
  39. Do, 12.12.2013, 14h15-15h45
  40. Beweis des Erfüllbarkeitslemmas für abzählbare Signaturen; Abschluss des Kapitels über den Vollständigkeitssatz.
    Der Kompaktheitssatz (Endlichkeitssatz), Modellklassen und Axiomatisierbarkeit; Axiomatisierbarkeit der Unendlichkeit; Nicht-Axiomatisierbarkeit der Endlichkeit.
    Material:
    Kapitel 7 (komplett) und Kapitel 8 (bis inkl. Satz 8.8).
    Weitere Lektüre:
    Kapitel 5 in [EFT]. Ein Beweis des Erfüllbarkeitslemma für überabzählbare Signaturen findet sich in Kapitel 5.3 von [EFT].
  41. Do, 12.12.2013, 16h15-17h45
  42. Nicht-Axiomatisierbarkeit von Graphzusammenhang; der Satz von Löwenheim und Skolem; Nicht-Axiomatisierbarkeit von Überabzählbarkeit; Theorien und elementare Äquivalenz; Existenz von Nichtstandardmodellen der Arithmetik.
    Übungsblatt 9 wird nächste Woche in der Übungsstunde ausgeteilt.
    Material:
    Kapitel 8 (bis inkl. Bemerkung 8.17, sowie Definition 8.20)
    Weitere Lektüre:
    Kapitel 6 in [EFT].
  43. Di, 14.01.2014
  44. Abschluss von Kapitel 8: Ein Nichtstandardmodell der natürlichen Zahlen mit linearer Ordnung; alternativer Beweis (Martin Otto, 2011) dafür, dass endliche lineare Ordnungen gerader Kardinalität nicht FO-definierbar sind in der Klasse aller endlichen linearen Ordnungen; der Satz von Skolem: ein abzählbares Nichtstandardmodell der Arithmetik.
    Material:
    Kapitel 8 (komplett)
    Weitere Lektüre:
    Kapitel 6 in [EFT].
  45. Do, 16.01.2014
  46. Beginn mit Kapitel 9: Die Grenzen der Berechenbarkeit: Entscheidbarkeit, Semi-Entscheidbarkeit und rekursive Aufzählbarkeit; Vereinbarung zur Kodierung der Syntax von FO-Formeln.
    Übungsblatt 10 ausgeteilt.
    Material:
    Kapitel 9 (bis inkl. Seite 292)
    Vortragsfolien zum Thema "Berechenbarkeit": Seiten 1-19 und 53-63 (dies ist "Kapitel 4: Berechenbarkeit" der Veranstaltung Theoretische Informatik 2 aus dem Sommersemester 2012)
    Weitere Lektüre:
    Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
  47. Di, 21.01.2014
  48. Die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln; Gödelisierung von FO[σAr]; die rekursive Aufzählbarkeit einiger definierbarer Zahlenmengen.
    Material:
    Kapitel 9 (bis inkl. Seite 304)
    Weitere Lektüre:
    Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
  49. Di, 28.01.2014
  50. FO-Definierbarkeit von Relationen und Funktionen; die Klasse Δ0 aller beschränkten FO[σAr]-Formeln; das Lemma über die β-Funktion.
    Material:
    Kapitel 9 (bis inkl. Seite 312)
    Weitere Lektüre:
    Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
  51. Do, 30.01.2014, 14h15-15h45
  52. 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.
    Material:
    Kapitel 9 (bis inkl. Seite 322)
    Weitere Lektüre:
    Kapitel 10 in [EFT]; Kapitel 9.1 sowie 5.1 und 5.2 in [L]; Kapitel 7.2.1 in [EF].
  53. Do, 30.01.2014, 16h15-17h45
  54. Die Unentscheidbarkeit der Theorie der Standardarithmetik; Erfüllbarkeit und Allgemeingültigkeit im Endlichen; der Satz von Trakhtenbrot (Трахтенброт): Unentscheidbarkeit des Endlichen Erfüllbarkeitsproblems für FO; Folgerung aus dem Satz von Trakthenbrot: die im Endlichen allgemeingültigen FO-Sätze sind nicht rekursiv aufzählbar.
    Übungsblatt 11 ausgeteilt.
    Material:
    Kapitel 9 (bis inkl. Seite 325.12)
    Weitere Lektüre:
    Kapitel 10 in [EFT]; Kapitel 9.1 sowie 5.1 und 5.2 in [L]; Kapitel 7.2.1 in [EF].
  55. Di, 04.02.2014
  56. Abschluss von Kapitel 9: Folgerung aus dem Satz von Trakthenbrot: die im Endlichen ordnungsinvarianten FO-Sätze sind nicht rekursiv aufzählbar.
    Beginn mit Kapitel 10: Gödels Unvollständigkeitssätze: Theorien und Axiomatisierbarkeit; die Minimale Arithmetik Q; Formulierung von Gödels erstem Unvollständigkeitssatz; der Σ1-Transfersatz.
    Material:
    Kapitel 9 (komplett) und Kapitel 10 (bis inkl. Seite 337 - aus Zeitgründen wird der Beweis von Lemma 10.8 in der nächsten Stunde nachgetragen)
    Weitere Lektüre:
    Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
  57. Do, 06.02.2014
  58. Weiter mit Kapitel 10: Abschluss des Beweises des Σ1-Transfersatzes (d.h. Beweis von Lemma 10.8); Repräsentierbarkeit von Relationen und Funktionen; Satz über die Repräsentierbarkeit (in der minimalen Arithmetik Q) der berechenbaren totalen Funktionen und der entscheidbaren Relationen.
    Übungsblatt 12 ausgeteilt.
    Material:
    Kapitel 10 (Seiten 335-350)
    Weitere Lektüre:
    Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
  59. Di, 11.02.2014
  60. Der Fixpunktsatz; der Satz über die Unmöglichkeit der Selbstrepräsentierbarkeit; der Satz von Tarski über die Nichtdefinierbarkeit der Wahrheit; die Unentscheidbarkeit der minimalen Arithmethik; die Unentscheidbarkeit des Allgemeingültigkeitsproblems für FOFO[σAr]; Beweis von Gödels erstem Unvollständigkeitssatz.
    Material:
    Kapitel 10 (Seite 350-360)
    Weitere Lektüre:
    Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].
  61. Do, 13.02.2014
  62. Existenz von Gödelsätzen und Präzisierung von Gödels erstem Unvollständigkeitssatz; Anmerkungen zu Hilberts Programm; die Peano-Arithmetik; Formulierung von Gödels zweitem Unvollständigkeitssatz; Hinweise zur Prüfungsvorbereitung.
    Material:
    Kapitel 10 (Seite 361-371)
    Weitere Lektüre:
    Kapitel 15-18 in [BBJ] sowie Kapitel 10 in [EFT].