Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der
einzelnen Vorlesungsstunden sowie gelegentlich ergänzende Bemerkungen.
Di, 15.10.2013
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".
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.
Do, 17.10.2013, 14h15-15h45
Beispiele für Isomorphismen;
Syntax und Semantik der Logik erster Stufe.
Semantik der Logik erster Stufe; Beispiele;
Koinzidenzlemma; Isomorphielemma; einführendes Beispiel zum Thema Substitutionen.
Übungsblatt 1 ausgeteilt.
Die Auswertungskomplexität von FO in endlichen Strukturen;
Spielregeln des Ehrenfeucht-Fraisse Spiels (kurz:
EF-Spiel); partielle Isomorphismen; Beispiele zum EF-Spiel.
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].
Do, 31.10.2013
Gewinnstrategien; das EF-Spiel auf zwei linearen Ordnungen.
Übungsblatt 3 ausgeteilt.
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.
Kapitel 3.3, 3.4 und 3.5
in [L],
Kapitel 2.1 bis 2.3
in [EF].
Do, 07.11.2013
Gewinnstrategien für Spoiler; logische Reduktionen; Nachweis, dass
Graph-Zusammenhang und Erreichbarkeit nicht FO-definierbar sind; Vorarbeiten
zum Satz von Hanf.
Übungsblatt 4 ausgeteilt.
Kapitel 2.5
in [EF],
Kapitel 4.1-4.3 und 4.5
in [L].
Di, 26.11.2013
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.
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.
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.
Do, 28.11.2013, 16h15-17h30
Beweis des Satzes von McNaughton und Papert.
Übungsblatt 7 ausgeteilt.
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.
Ableitbare Sequenzenregeln;
Widerspruchsfreiheit; das syntaktische
Endlichkeitslemma; der Vollständigkeitssatz; Beweis des
Vollständigkeitssatzes unter Verwendung des Erfüllbarkeitslemmas.
Terminterpretation und reduzierte Terminterpretation;
negationstreue Formelmengen; Formelmengen, die Beispiele
enthalten; der Satz von Henkin.
Übungsblatt 8 ausgeteilt.
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.
Kapitel 5
in [EFT]. Ein
Beweis des Erfüllbarkeitslemma für
überabzählbare Signaturen findet sich in Kapitel 5.3 von [EFT].
Do, 12.12.2013, 16h15-17h45
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.
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.
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.
Die rekursive Aufzählbarkeit der allgemeingültigen
FO-Formeln;
Gödelisierung von FO[σAr];
die rekursive Aufzählbarkeit einiger definierbarer Zahlenmengen.
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.
Kapitel 10 in [EFT]; Kapitel 9.1 sowie 5.1 und 5.2 in [L]; Kapitel 7.2.1 in [EF].
Do, 30.01.2014, 16h15-17h45
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.
Kapitel 10 in [EFT]; Kapitel 9.1 sowie 5.1 und 5.2 in [L]; Kapitel 7.2.1 in [EF].
Di, 04.02.2014
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.
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.
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.
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.