|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die in der Vorlesung verwendeten Folien, Teile des Skripts und gelegentlich auch Korrekturen und sonstige ergänzende Bemerkungen.
Eröffnungsveranstaltung. Start mit "Kapitel 0: Einleitung" - heute: Einführung ins Thema und ein historischer Überblick. Klärung von Organisatorischem (entlang der Webseite der Vorlesung). Wiederholung von Grundbegriffen und Schreibweisen, die bereits in der Veranstaltung "Logik in der Informatik" behandelt wurden: Strukturen und Syntax der Logik erster Stufe.
Material:
Skript-Fragmente,
Seiten 1-13 und
Skript der Vorlesung "Logik in der Informatik":
Seiten 101-120
Weitere Lektüre:
Lehrbuch [EFT]: Vorwort und Kapitel I-III.
Viele Beispiele zur Bedeutung der Logik in der Informatik finden
sich in dem Artikel "On the unusual effectiveness of
logic in computer science" von Halpern, Harper, Immerman, Kolaitis, Vardi
und Vianu, Bulletin of Symbolic Logic 7(2):213-236 (2001). Eine
Vorabversion des Artikels finden Sie hier.
Weiter in der Wiederholung von Grundbegriffen und Schreibweisen, die bereits in der Veranstaltung "Logik in der Informatik" behandelt wurden: Semantik der Logik erster Stufe und das Koinzidenzlemma.
Material:
Skript-Fragmente,
Seiten 14-20 (bis direkt vor Def 0.30) und
Skript der Vorlesung "Logik in der Informatik":
Seiten 101-127
Weitere Lektüre:
Lehrbuch [EFT]: Vorwort und Kapitel I-III.
Viele Beispiele zur Bedeutung der Logik in der Informatik finden
sich in dem Artikel "On the unusual effectiveness of
logic in computer science" von Halpern, Harper, Immerman, Kolaitis, Vardi
und Vianu, Bulletin of Symbolic Logic 7(2):213-236 (2001). Eine
Vorabversion des Artikels finden Sie hier.
Weiter in der Wiederholung von Grundbegriffen: Redukte und Expansionen von Strukturen; das Isomorphielemma; der Sequenzenkalkül (allgemeine Schreibweisen und Fakten zu Ableitungsregeln und Kalkülen; Sequenzen; Korrektheit von Sequenzen; Wunsch nach Vollständigkeit, Korrektheit und Effektivität eines Kalküls; Beginn der Einführung der Regeln des Sequenzenkalküls inkl. Diskussion zu deren Korrektheit und Effektivität)
Material:
Skript-Fragmente,
Seiten 20-21 (von Def 0.30 bis inkl. Korollar 0.33) und
Seiten 28-31, sowie
Skript der Vorlesung "Logik in der Informatik":
Seiten 177-193 (Folien 294-320)
Weitere Lektüre:
Lehrbuch [EFT]: Vorwort und Kapitel I-III.
Ein präziser Begriff von Substitutionen; Abschluss der Wiederholung von Grundbegriffen: der Sequenzenkalkül (Einführung der restlichen Regeln des Sequenzenkalküls inkl. Diskussion zu deren Korrektheit und Effektivität
Material:
Skript-Fragmente,
Seiten 21-25 (Abschnitt "0.3: Substitutionen") und
Seiten 31-34 (bis direkt vor Def. 1.14), sowie
Skript der Vorlesung "Logik in der Informatik":
Seiten 194-199 (Folien 321-328)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Ein mittels Ableitungen im Sequenzenkalkül kS definierter Begriff der Beweisbarkeit von Formeln aus Formelmengen; widerspruchsfreie und widerspruchsvolle Formelmengen; der Vollständigkeitssatz und das Erfüllbarkeitslemma; Ausblick zum Beweis des Erfüllbarkeitslemmas; ableitbare Regeln im Sequenzenkalkül; Eigenschaften widerspruchsvoller bzw. widerspruchsfreier Formelmengen.
Material:
Skript-Fragmente,
Seiten 35-41 (bis einschl. Lemma 1.24), sowie
Skript der Vorlesung "Logik in der Informatik":
Seiten 199/200 (Folien 328-331)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: weitere Eigenschaften widerspruchsfreier und widerspruchsvoller Formelmengen; das syntaktische Endlichkeitslemma; Termstrukturen und Terminterpretationen; reduzierte Termstrukturen und reduzierte Terminterpretationen; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; Formulierung des Satzes von Henkin
Material:
Skript-Fragmente:
Seiten 41-46
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Beweis des Satzes von Henkin
Material:
Skript-Fragmente:
Seiten 46-47
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Beweis von Lemma 1.39 (Erweiterung einer widerspruchsfreien Formelmenge zu einer widerspruchsfreien Formelmenge, die Beispiele enthält — für abzählbare Signaturen); Beweis von Lemma 1.40 (Erweiterung einer widerspruchsfreien Formelmenge zu einer widerspruchsfreien Formelmenge, die negationstreu ist — für abzählbare Signaturen); Beweis des Erfüllbarkeitslemmas und des Vollständigkeitssatzes für abzählbare Signaturen
Material:
Skript-Fragmente:
Seiten 47-50
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Formulierung von Varianten der Lemmas 1.39 und 1.40, die auch für nicht-abzählbare Signaturen gelten: Lemma 1.39' und Lemma 1.40'; Beweis des Erfüllbarkeitslemmas und des Vollständigkeitssatzes für beliebige Signaturen unter Verwendung des Lemmas 1.39' und 1.40'; Beweis von Lemma 1.39'
Material:
Notizen zu Kapitel 1
(nicht-abzählbare Signaturen) Seiten 1-7 und
Notizen zu Kapitel 1
(Exkurs) Seiten 8-9 (also die ersten beiden Seiten der pdf-Datei)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel V.
Abschluss von "Kapitel 1: Der Vollständigkeitssatz" - heute: Exkurs: das Auswahlaxiom, der Wohlordnungssatz und das Zornsche Lemma; Beweis von Lemma 1.40' (unter Verwendung des Zornschen Lemmas)
Material:
Notizen zu Kapitel 1
(Exkurs) Seiten 10-19 (also die Seiten 3-12 der pdf-Datei)
Weitere Lektüre:
Lehrbuch [E]: Kapitel III.7, IV.2 und VIII.
Beginn mit "Kapitel 2: Der Endlichkeitssatz und die Sätze von Löwenheim und Skolem" - heute: der Endlichkeitssatz; Modellklassen und Axiomatisierbarkeit; Begriffe zur Mächtigkeit von Mengen; Beispiele für die Anwendung des Endlichkeitssatzes: die Nicht-Axiomatisierbarkeit der Klasse aller endlichen sigma-Strukturen und Beweis der Aussage, dass Formelmengen, die beliebig große endliche Modelle besitzen, auch unendliche Modelle besitzen; noch ein Beispiel für die Anwendung des Endlichkeitssatzes: die Nicht-Axiomatisierbarkeit der Klasse ZG aller zusammenhängenden (endlichen oder unendlichen) gerichteten Graphen; der Satz von Löwenheim und Skolem
Material:
Skript-Fragmente:
Seiten 53-56
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel V und VI
Weiter mit "Kapitel 2: Der Endlichkeitssatz und die Sätze von Löwenheim und Skolem" - heute: der absteigende Satz von Löwenheim und Skolem; der aufsteigende Satz von Löwenheim und Skolem; der Begriff der elementaren Äquivalenz zweier sigma-Strukturen; der Begriff der Theorie einer sigma-Struktur; Nichtstandardmodelle der linear geordneten natürlichen Zahlen; Verwendung der Erkenntnisse dazu zum Beweis, dass es keinen FO-Satz gibt, der von genau denjenigen endlichen linearen Ordnungen erfüllt wird, deren Universum eine gerade Anzahl von Elementen enthält (Beweis von Martin Otto, 2011)
Material:
Skript-Fragmente:
Seiten 56-60
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel VI
Abschluss von "Kapitel 2: Der Endlichkeitssatz und die Sätze von Löwenheim und
Skolem" - heute:
Nichtstandardmodelle der Standardarithmetik; der Satz von Skolem über die
Existenz abzählbarer Nichtstandardmodelle der Standardarithmetik
Beginn mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute:
Wiederholung der Begriffe "entscheidbar", "semi-entscheidbar", "rekursiv
aufzählbar", "berechenbar"; einige Vereinbarungen zur Kodierung der Syntax
von FO-Formeln;
die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln;
Vorüberlegungen zur Gödelisierung von FO[σAr]
Material:
Skript-Fragmente:
Seiten 60-62
Notizen zu
Kapitel 3 - heute bis inkl. "Zahlterme" und "Arithmetisierung" (Seiten 1-10 der PDF-Datei;
Seitennummern 287-296)
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel VI und X; Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: Gödelisierung von FO[σAr]; Lemma über die Berechenbarkeit der Gödelnummern von Zahltermen; 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 (Formulierung und Beginn des Beweises)
Material:
Notizen zu
Kapitel 3 - heute bis zum Ende des Beweises von Behauptung 2 im Beweis von Lemma 3.15 (Seiten 11-25 der PDF-Datei;
Seitennummern 296-310)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: Abschluss des Beweises des Lemmas über die β-Funktion; deterministische 1-Band Turingmaschinen
Material:
Notizen zu
Kapitel 3 - heute: Seiten 25-31 der PDF-Datei;
Seitennummern 310-316
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: Δ0-Definierbarkeit der Kodierung einer Konfiguration einer Turingmaschine; Δ0-Definierbarkeit von Turingmaschinen-Berechnungen; die Klasse Σ1; die Σ1-Definierbarkeit der berechenbaren partiellen Funktionen und der rekursiv aufzählbaren Relationen
Material:
Notizen zu
Kapitel 3 - heute Seiten 31-38 der PDF-Datei
(also Seitennummern 318-323)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Abschluss von "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: die Unentscheidbarkeit der Arithmetik; der Satz von Trakhtenbrot (Трахтенброт) und Folgerungen daraus für's endliche Erfüllbarkeitsproblem und das endliche Allgemeingültigkeitsproblem
Material:
Notizen zu
Kapitel 3 - heute Seiten 38-51 der PDF-Datei
(also Seitennummern 323-324 und 325.1-325.12)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Start mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: Theorien und Axiomatisierbarkeit; die Minimale Arithmetik Q; Formulierung von Gödels 1. Unvollständigkeitssatz; der Σ1-Transfersatz: Formulierung des Satzes; Formulierung und Beweis des technischen Lemmas 4.6; Bemerkung 4.7 zum Vergleich zwischen der Standardarithmetik und anderen Modellen von Q; Formulierung (heute noch ohne Beweis) des technischen Lemmas 4.8; Beweis des Σ1-Transfersatzes unter Verwendung von Lemma 4.8)
Material:
Notizen zu
Kapitel 4 - heute Seiten 1-13 und 15 der PDF-Datei
(also Seitennummern 326-335 und 337)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: Beweis von Lemma 4.8; Repräsentierbarkeit von Relationen und Funktionen; Satz über die Repräsentierbarkeit (in der minimalen Arithmetik Q) der TM-berechenbaren totalen Funktionen und der entscheidbaren Relationen; Beweis von Lemma 4.12 a.) & b.) (ein technisches Lemma, das zum Beweis des Satzes über die Repräsentierbarkeit (in der minimalen Arithmetik Q) der TM-berechenbaren totalen Funktionen und der entscheidbaren Relationen benutzt wird)
Material:
Notizen zu
Kapitel 4 - heute Seiten 20-25 der PDF-Datei
(also Seitennummern 342-347)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: Wiederholung der bisher in Kapitel 4 erreichten Meilensteine; der Fixpunktsatz (Formulierung und Beweis)
Material:
Notizen zu
Kapitel 4 - heute Seiten 8-31 der PDF-Datei
(also Seitennummern 330-353)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: 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 FO[σAr]; Beweis von Gödels erstem Unvollständigkeitssatz
Material:
Notizen zu
Kapitel 4 - heute Seiten 32-38 der PDF-Datei
(also Seitennummern 354-360)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: die Existenz von Beweisbarkeitsformeln und Gödelsätzen; Präzisierung von Gödels erstem Unvollständigkeitssatz der Konsistenzsatz WfreiT für eine Theorie T
Material:
Notizen zu
Kapitel 4 - heute Seiten 38-44 und 48 der PDF-Datei
(also Seitennummern 360-366 und 369)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Abschluss von "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: die Peano-Arithmetik; Formulierung von Gödels zweitem Unvollständigkeitssatz und Beweis unter Verwendung des Satzes von Löb; Anmerkungen zum Beweis des Satzes von Löb
Weitere Lektüre:
Eine ausführliche Erklärung des im Beweis des Satzes von Löb verwendeten
Arguments finden Sie auf den
Seiten 235-238 in [BBJ].
Weitere Details sowie Verweise zur Literatur finden sich
in [S].
Wiederholung und Zusammenfassung der in Vorlesung und Übung behandelten Themen, sowie Tipps zur Vorbereitung auf die mündliche Modulabschlussprüfung