|
Logik in der Informatik
Prof. Dr. Nicole Schweikardt |
|
Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, Tipps zum Weiterlesen und gelegentlich 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 bzgl. Syntax und Semantik der Logik erster Stufe (die bereits in der Veranstaltung "Logik in der Informatik" behandelt wurden). Beginn des Abschnitts über Substitutionen.
Material:
Skript der Vorlesung "Logik in der Informatik":
Seiten 101-137
und
Skript-Fragmente,
Seiten 1-22 (bis zum Ende von Beispiel 0.34)
Weitere Lektüre:
Vorlesungsskript [S-LI]: Kapitel 3;
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: Substitutionen. Beginn mit "Kapitel 1: Der Vollständigkeitssatz" - heute: allgemeine Schreibweisen und Fakten zu Ableitungsregeln und Kalkülen; Sequenzen; Korrektheit von Sequenzen; Wunsch nach Vollständigkeit, Korrektheit und Effektivität eines Kalküls
Material:
Skript der Vorlesung "Logik in der Informatik":
Seiten 178-185
und Skript-Fragmente:
Seiten 22-30
Weitere Lektüre:
Vorlesungsskript [S-LI]: Kapitel 4;
Lehrbuch [EFT]: Vorwort und Kapitel I-III.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Einführung und Korrektheit des Sequenzenkalküls kS; Anmerkungen zur Effektivität des Sequenzenkalküls kS; Beispiele für Ableitungen im Sequenzenkalküls kS
Material:
Skript der Vorlesung "Logik in der Informatik":
Seiten 185-199
und Skript-Fragmente:
Seiten 30-34
Weitere Lektüre:
Vorlesungsskript [S-LI]: Kapitel 4;
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Anmerkung zum Thema Substitutionen (siehe Aufgabe 3 auf Blatt 2); 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; Beweis des Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas; Ausblick zum Beweis des Erfüllbarkeitslemmas; ableitbare Regeln im Sequenzenkalkül
Material:
Skript der Vorlesung "Logik in der Informatik":
Seiten 199-203
und Skript-Fragmente:
Seiten 34-38 (bis zum Ende des Beweises von Lemma 1.19)
Weitere Lektüre:
Vorlesungsskript [S-LI]: Kapitel 4;
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: weitere ableitbare Regeln im Sequenzenkalkül; Terminterpretation und reduzierte Terminterpretation; negationstreue Formelmengen; Formelmengen, die Beispiele enthalten; der Satz von Henkin
Material:
Skript-Fragmente:
Seiten 38-39 und 43-46
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: Abschluss des Beweises des Satzes von Henkin; Formulierung und Beweis eines Korollars, das besagt, dass die Aussage des Vollständigkeitssatzes gilt, wenn die betrachtete Formelmenge zusätzlich negationstreu ist und Beispiele enthält; Beweis 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-49
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel IV-V.
Weiter mit "Kapitel 1: Der Vollständigkeitssatz" - heute: 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; Formulierung eines Lemmas, das einfache Charakterisierungen von widerspruchsfreien Formelmengen liefert; Überlegung dazu, wie die reduzierte Terminterpretation einer widerspruchsvollen Formelmenge aussieht
Material:
Skript-Fragmente:
Seiten 49-50 und 40-41 (Lemma 1.24(c) und Lemma 1.25(b))
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
Material:
Notizen zu Kapitel 1
(Exkurs) Seiten 10-16 (also die Seiten 3-9 der pdf-Datei)
Weitere Lektüre:
Lehrbuch [E]: Kapitel III.7, IV.2 und VIII.
Abschluss von "Kapitel 1: Der Vollständigkeitssatz" - heute: Beweis von Lemma 1.40 (unter Verwendung des
Zornschen Lemmas)
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
Material:
Notizen zu Kapitel 1
(Exkurs) Seiten 17-19 (also die Seiten 10-12 der pdf-Datei) und
Skript-Fragmente:
Seiten 53-55
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: 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; der aufsteigende Satz von Löwenheim und Skolem; der Begriff der elementaren Äquivalenz zweier sigma-Strukturen; der Begriff der Theorie einer sigma-Struktur
Material:
Skript-Fragmente:
Seiten 55-58
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel VI
Weiter mit "Kapitel 2: Der Endlichkeitssatz und die Sätze von Löwenheim und Skolem" - heute: 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 58-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
Material:
Skript-Fragmente:
Seiten 60-62
Notizen zu
Kapitel 3 - heute bis inkl. Annahme 9.1(d) (Seite 5 der PDF-Datei;
Seitennummer 290)
Weitere Lektüre:
Lehrbuch [EFT]:
Kapitel VI und X; Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: weitere Vereinbarungen zur Kodierung der Syntax von FO-Formeln; die rekursive Aufzählbarkeit der allgemeingültigen FO-Formeln; Gödelisierung von FO[σAr]; Lemma über die Berechenbarkeit der Gödelnummern von Zahltermen
Material:
Notizen zu
Kapitel 3 - heute bis inkl. Lemma 9.10 (Seiten 6-17 der PDF-Datei;
Seitennummern 291-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
Material:
Notizen zu
Kapitel 3 - heute bis zum Ende des Beweises von Behauptung 1 im Beweis von Lemma 3.15 (Seiten 17-24 der PDF-Datei;
Seitennummern 302-309)
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
Material:
Notizen zu
Kapitel 3 - heute bis zum Ende von Lemma 8.18 (Seiten 25-32 der PDF-Datei;
Seitennummern 310-317)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Weiter mit "Kapitel 3: Die Grenzen der Berechenbarkeit" - heute: Δ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
Material:
Notizen zu
Kapitel 3 - heute Seiten 33-39 der PDF-Datei
(also Seitennummern 318-324)
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 (Трахтенброт)
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 40-52 der PDF-Datei
(also Seitennummern 325.1-325.12)
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; 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
Material:
Notizen zu
Kapitel 4 - heute Seiten 8-20 der PDF-Datei
(also Seitennummern 330-342)
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 (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); der Fixpunktsatz
Material:
Notizen zu
Kapitel 4 - heute Seiten 20-31 der PDF-Datei
(also Seitennummern 342-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; die Existenz von Beweisbarkeitsformeln und Gödelsätzen; Präzisierung von Gödels erstem Unvollständigkeitssatz
Material:
Notizen zu
Kapitel 4 - heute Seiten 32-43 der PDF-Datei
(also Seitennummern 354-365)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Abschluss von "Kapitel 4: Gödels Unvollständigkeitssätze" - heute: Anmerkungen zu Hilberts Programm; der Konsistenzsatz WfreiT für eine Theorie T; 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
Material:
Notizen zu
Kapitel 4 - heute Seiten 44-57 der PDF-Datei
(also Seitennummern 366-378)
Weitere Lektüre:
Lehrbuch [EFT]: Kapitel X;
Lehrbuch [BBJ]: Kapitel 15-18
Eine ausführliche Erklärung des im Beweis des Satzes von Löb verwendeten
Arguments finden Sie auf den
Seiten 235-238 in [BBJ].
Wiederholung und Zusammenfassung der wichtigsten Erkenntnisse aus Kapitel
4.
Start mit "Kapitel 5: Ordnungsinvarianz" - heute:
Ordnungs-invariante, Additions-invariante und Arb-invariante Formeln;
Beispiele; Trennung der Ausdrucksstärke zwischen Ordnungs-invariantem FO,
Additions-invariantem FO, (+,.)-invariantem FO und Arb-invariantem FO;
Formulierung des Satzes von Ginsburg und Spanier (der zur Trennung der
Ausdrucksstärke von Additions-invariantem FO und (+,.)-invariantem FO
genutzt wird
Material:
Folien zu
Kapitel 5 - heute Folien 1-7
Weitere Lektüre:
Weitere Details sowie Verweise zur Literatur finden sich
in [S].
Details zum Satz von Ginsburg und Spanier (und zum Thema
"Quantorenelimination der Presburger-Arithmetik) finden sich in dem
Buch Logical Number Theory I von Craig Smorynski
(Springer-Verlag, 1991). [Zur Info: In der Bibliothek der HU Berlin
scheint ein Online-Exemplar des Buchs verfügbar zu sein.]
Weiter mit "Kapitel 5: Ordnungsinvarianz" - heute: Unentscheidbarkeit der Ordnungs-invarianz von FO-Formeln über der Signatur {E,C,<}; Entscheidbarkeit der Ordnungs-invarianz von FO-Formeln über unären Signaturen mit <; Unentscheidbarkeit der Additions-invarianz von FO-Formeln über der Signatur {C,+}
Material:
Folien zu
Kapitel 5 - heute Folien 8-12
Weitere Lektüre:
Weitere Details sowie Verweise zur Literatur finden sich in [S].
Abschluss von "Kapitel 5: Ordnungsinvarianz" - heute: 3 Methoden zum Nachweis, dass Ordnungs-invariantes FO ausdurcksstärker ist als FO: die Beweise von Gurevich, Potthoff und Otto; Beweis von Niemistö zum Nachweis, dass Ordnungs-invariantes FO+MOD2 ausdrucksstärker ist als FO+MOD2
Material:
Folien zu
Kapitel 5 - heute Folien 13-19
Weitere Lektüre:
Weitere Details sowie Verweise zur Literatur finden sich
in [S].
Mehr Infos zu Niemistös Beweis finden sich in dem Artikel
On the locality of arb-invariant
first-order logic with modulo counting quantifiers von Frederik Harwath
und Nicole Schweikardt (Proc. CSL 2013, pp. 363-379)