|
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-15 (bis inkl. Definition 0.18)
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.
Abschluss von "Kapitel 0: Einleitung" - heute:
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
neu: Ein präziser Begriff der Substitution (von Variablen durch Terme) in Formeln der Logik erster Stufe
Material:
Skript-Fragmente,
Seiten 15-27
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.
Start mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Wiederholung aus "Logik in der Informatik": abstrakter Begriff eines Kalküls und der Menge der aus einem Kalkül ableitbaren Elemente; Begriffe: Sequenz, Korrektheit einer Sequenz, Sequenzenregeln, Korrektheit einer Sequenzenregel; Wunschliste von Eigenschaften, die der im Folgenden eingeführte Sequenzenkalkül haben soll (Korrektheit, Vollständigkeit, Effektivität); Beginn der Einführung der Regeln des Sequenzenkalküls; hierbei jeweils direkt die Korrektheit und Effektivität der jeweiligen Regeln bewiesen
Material:
Skript-Fragmente,
Seiten 28-31 (bis inkl. Regel (W)) und Seite 33
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: restliche Regeln des Sequenzenkalküls eingeführt und deren Korrektheit und Effektivität nachgewiesen; Beispiele für Ableitungen im Sequenzenkalkül; Begriffsdefinition: Formel φ ist aus Formelmenge Φ im Sequenzenkalkül beweisbar; Formulierung der ersten Aussage des Vollständigkeitssatzes: eine Formel φ ist aus einer Formelmenge Φ im Sequenzenkalkül ableitbar genau dann wenn die Formel φ aus der Formelmenge Φ folgt; Definition des Begriffs ableitbare Regel im Sequenzenkalkül; Formulierung und Beweisidee von Lemma 1.17
Material:
Skript-Fragmente:
Seiten 31-35 (bis inkl. Lemma 1.17)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: ableitbare Regeln im Sequenzenkalkül; Eigenschaften widerspruchsvoller bzw. widerspruchsfreier Formelmengen; Formulierung des Vollständigkeitssatzes; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas; Ausblick zum Beweis des Erfüllbarkeitslemmas; Termstruktur und Terminterpretation
Material:
Skript-Fragmente:
Seiten 35-43
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: kurze Wiederholung der bisher eingeführten Definitionen (inkl. der Definitionen "Termstruktur" und "Terminterpretation"); reduzierte Termstruktur und reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; Formulierung des Satzes von Henkin
Material:
Skript-Fragmente:
Seiten 43-46
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Beweis des Satzes von Henkin; Beginn des Beweises von Lemma 1.39 (Erweiterung einer widerspruchsfreien Formelmenge zu einer widerspruchsfreien Formelmenge, die Beispiele enthält — für abzählbare Signaturen)
Material:
Skript-Fragmente:
Seiten 46-48 (bis inkl. Induktionsanfang der Behauptung)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Abschluss des Beweises von Lemma 1.39; 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 48-51
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel 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; Beginn des Beweises von Lemma 1.40' (unter Verwendung des Zornschen Lemmas)
Material:
Notizen zu Kapitel 1
(Exkurs) Seiten 8 und 10-18 (also die Seiten 1 und 3-11 der pdf-Datei)
Weitere Lektüre:
Lehrbuch [E]: Kapitel III.7, IV.2 und VIII.
Abschluss von "Kapitel 1: Der Vollständigkeitssatz" - heute: 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; die Axiomatisierbarkeit der Unendlichkeit;
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
Material:
Notizen zu Kapitel 1
(Exkurs): Seiten 8 und 17-19 (also die Seiten 1 und 10-12 der pdf-Datei)
und 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: die Nicht-Axiomatisierbarkeit der Überabzählbarkeit; der absteigende Satz von Löwenheim und Skolem; 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 57-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;
Anforderungen an eine Kodierung von Formeln durch Worte über einem geeigneten Alphabet;
Lemma über die Aufzählbarkeit der beweisbaren Sätze
Material:
Skript-Fragmente:
Seiten 60-62
Notizen zu
Kapitel 3 - heute Seiten 1-8 der PDF-Datei (d.h.
Seitennummern 287-293; bis unmittelbar vor Lemma 9.2)
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel VI und X; Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln; 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 (Aussage des Lemmas)
Material:
Notizen zu
Kapitel 3 - heute Seiten 8-23 der PDF-Datei (d.h.
Seitennummern 293-308)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: Beweis des Lemmas über die β-Funktion
Material:
Notizen zu
Kapitel 3 - heute Seiten 22-27 der PDF-Datei
(also Seitennummern 307-312)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: 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; die Unentscheidbarkeit der Arithmetik; Erfüllbarkeit im Endlichen; der Satz von Trakhtenbrot (Трахтенброт) Formulierung und Beweis, dass die Menge der im Endlichen erfüllbaren Sätze rekursiv aufzählbar ist.
Material:
Notizen zu
Kapitel 3 - heute Seiten 28-41 der PDF-Datei
(also Seitennummern 313-325.2)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute:
Abschluss Beweis des Satzes von Trakhtenbrot
und Folgerungen daraus für das endliche Erfüllbarkeitsproblem,
das endliche Allgemeingültigkeitsproblem
und das endliche Ordnungsinvarianzproblem.
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 41-55 der PDF-Datei
(also Seitennummern 325.2-325.16) 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
Weiter mit "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: der Σ1-Transfersatz: Formulierung und Beweis des Satzes; 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.
Material:
Notizen zu
Kapitel 4 - heute Seiten 8-19 der PDF-Datei
(also Seitennummern 330-341)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18