Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage Prädikatenlogik höherer Stufe von jener erster Stufe abzugrenzen. Studierende werden dann auch in der Lage sein, komplexe mathematische Sätze in Systemen der Higher-order Logik zu formalisieren und zu verifizieren. Die Lehrveranstaltung wird zu einem vertieften Verständnis der arithmetischen Theorien und der natürlichen Zahlen führen und selbständige Forschungsarbeit auf diesem Gebiet ermöglichen.

• Resultate zur Prädikatenlogik erster Stufe (Vollständigkeitssatz, Unvollständigkeitssätze, Kompaktheit, Satz von Löwenheim-Skolem)
• Prädikatenlogik zweiter Stufe
• Modelltheorie der Prädikatenlogik zweiter Stufe
• Theorie der Arithmetik in der Prädikatenlogik zweiter Stufe
• Einfache Typtheorie
• Prädikatenlogik höherer Stufe
• Modelltheorie der Prädikatenlogik höherer Stufe
• Ansätze zur Wiedererlangung eines Vollständikeitssatzes für Prädikatenlogik höherer Stufe
• Automatisches Beweisen in Prädikatenlogik höherer Stufe

Präsentation in der Vorlesung, Übungen und Diskussion der Lösungen

Weiterführende Literatur:

• G. Takeuti: Proof Theory, 2nd Edition, 1987, North Holland

Mündliche Prüfung und Beurteilung der Mitarbeit in Übungen und Diskussionen

Gute Kenntnisse der Logik erster Stufe