|
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 Themen die bereits in der Veranstaltung
"Logik in der Informatik" bzw. "Einführung in die formale Logik für IMP" behandelt wurden: Semantik
der Logik erster Stufe, Isomorphielemma, Koinzidenzlemma, die Regeln des Sequenzenkalküls, Korrektheit und Effektivität des Sequenzenkalküls.
Ein präziser Begriff der Substitution (von Variablen durch Terme) in Formeln der Logik erster Stufe
Material:
Skript-Fragmente,
Seiten 14-35 (bis zum Ende von Kapitel 1.2) und
Skript der Vorlesung "Logik in der Informatik":
Seiten 101-137 und 178-199.
Weitere Lektüre:
Lehrbuch [EFT]: Vorwort und Kapitel I-III und Kapitel IV-V.
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 mit "Kapitel 1: Der Vollständigkeitssatz" - heute: 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-42, sowie
Skript der Vorlesung "Logik in der Informatik":
Seiten 200-203
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Termstruktur und Terminterpretation; reduzierte Termstruktur und reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; der Satz von Henkin
Material:
Skript-Fragmente:
Seiten 43-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.
Weiter mit "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.
Abschluss des Beweises von Lemma 1.40'.
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 σ-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; der absteigende 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 aufsteigende Satz von Löwenheim und Skolem; der Begriff der elementaren Äquivalenz zweier σ-Strukturen; der Begriff der Theorie einer σ-Struktur; Nichtstandardmodelle der linear geordneten natürlichen Zahlen; Verwendung der Erkenntnisse hierzu 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; Überlegungen dazu, welche Eigenschaften ein Nichstandardmodell der Standardarithmetik hat
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
Material:
Skript-Fragmente:
Seiten 60-62
Notizen zu
Kapitel 3 - heute Seiten 1-3 der PDF-Datei (d.h.
Seitennummern 287-288)
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel VI und X; Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: Anforderungen an eine Kodierung von Formeln durch Worte über einem geeigneten Alphabet; die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln; Vorüberlegungen zur Gödelisierung von FO[σAr] Gödelisierung von FO[σAr]; Lemma über die Berechenbarkeit der Gödelnummern von Zahltermen
Material:
Notizen zu
Kapitel 3 - heute Seiten 4-17 der PDF-Datei (d.h.
Seitennummern 289-302)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: 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: Seiten 17-25 der PDF-Datei;
Seitennummern 302-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; Δ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 26-38 der PDF-Datei
(also Seitennummern 311-323)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute:
die Unentscheidbarkeit der Arithmetik.
Der Abschnitt "3.4: Der Satz von Trakhtenbrot" wird erst nächste Woche in der Vorlesung behandelt.
Start mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute:
Theorien und Axiomatisierbarkeit; die Minimale Arithmetik Q;
Formulierung von Gödels 1. Unvollständigkeitssatz
Material:
Notizen zu
Kapitel 3 - heute Seiten 38-39 der PDF-Datei
(also Seitennummern 323-324) und
Notizen zu
Kapitel 4 - heute Seiten 1-8 der PDF-Datei
(also Seitennummern 326-330)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Abschluss von "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: der Satz von Trakhtenbrot (Трахтенброт) und Folgerungen daraus für das endliche Erfüllbarkeitsproblem, das endliche Allgemeingültigkeitsproblem und das endliche Ordnungsinvarianzproblem
Material:
Notizen zu
Kapitel 3 - heute Seiten 40-55 der PDF-Datei
(also Seitennummern 325.1-325.16)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: der Σ1-Transfersatz: Formulierung und Beweis des Satzes
Material:
Notizen zu
Kapitel 4 - heute Seiten 8-15 der PDF-Datei
(also Seitennummern 330-337)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: Repräsentierbarkeit von Relationen und Funktionen; Formulierung des Satzes 4.11 über die Repräsentierbarkeit (in der minimalen Arithmetik Q) der TM-berechenbaren totalen Funktionen und der entscheidbaren Relationen; Formulierung von Lemma 4.12 (ein technisches Lemma, das zum Beweis von Satz 4.11 verwendet wird); Beweis von Lemma 4.12(a).
Material:
Notizen zu
Kapitel 4 - heute Seiten 16-18 und 20-23 der PDF-Datei
(also Seitennummern 338-340 und 342-345)
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.12 (b) und (c); Beweis von Satz 4.11; Formulierung des Fixpunktsatzes
Material:
Notizen zu
Kapitel 4 - heute Seiten 18-20 und 24-28 der PDF-Datei
(also Seitennummern 340-342 und 346-350)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: Beweis des Fixpunktsatzes; Formulierung und Beweis von Satz 4.14 (Unmöglichkeit der Selbstrepräsentierbarkeit); Satz 4.15 (Satz von Tarski über die Nichtdefinierbarkeit der Wahrheit)
Material:
Notizen zu
Kapitel 4 - heute Seiten 28-34 der PDF-Datei
(also Seitennummern 350-356)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: die Unentscheidbarkeit der minimalen Arithmethik (Satz 4.16); die Unentscheidbarkeit des Allgemeingültigkeitsproblems für FO[σAr]; Beweis von Gödels erstem Unvollständigkeitssatz; 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 34-43 und 48 der PDF-Datei
(also Seitennummern 356-365 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].