Inhalt
Die Formale Logik ist gleichermaßen beheimatet in der Philosophie, der Mathematik und der Informatik. Mit leicht unterschiedlicher Ausprägung ist sie in all diesen Disziplinen sowohl auf Anfänger- als auch auf Fortgeschrittenen-Niveau in Lehrveranstaltungen der jeweiligen Studiengänge vertreten. Kernthemen wie z.B. Aussagen- und Prädikatenlogik oder der Kalkül des natürlichen Schließens werden
nicht selten mehrfach angesprochen, andere wichtige Themen aus Zeitgründen oft übergangen.
Mit unserer Lehrveranstaltung richten wir uns deshalb gleichzeitig an Studierende der Philosophie, Mathematik und Informatik. Ziel ist es, eine fachübergreifende Einführung in verschiedene (theoretische) Logikformalismen mit einer praktisch motivierten Einführung in moderne, computer-basierte Beweisassistenzsysteme zu kombinieren.
Zu Beginn werden wir die zentrale Idee der Veranstaltung näher beleuchten, in die theoretischen Grundlagen einführen und die zum praktischen Einsatz vorgesehenen Beweisassistenzsysteme vorstellen. Als einen ersten Höhepunkt werden wir dann Varianten des ontologischen Gottesbeweises mit einem Computersystem selbst nachvollziehen. Anschließend widmen wir uns weiteren relevanten
Themen, beispielsweise Zalta's Theorie abstrakter Objekte als Grundlage für die Metaphysik, und untersuchen erneut die Formalisierbarkeit am Computer.
Abschließend soll fachübergreifend die Bedeutung dieser Arbeiten diskutiert werden, insbesondere im Hinblick auf eine computationale Metaphysik und die sich andeutende (und zum Teil bereits nachgewiesene) Möglichkeit der formalen Verifikation von Publikationen in diesem Bereich.
In Projektarbeiten sollen die Studierenden versuchen, die erlernten Techniken auf weitere, ähnliche Argumente in der Metaphysik zu übertragen und anzuwenden. Dabei soll aber auch der enge übergeordnete Bezug zu verwandten, aber technisch weitaus komplexeren Arbeiten in der Mathematik (Beweis der Kepler'schen Vermutung) beleuchtet werden. Jede gute Arbeit kann potenziell in einer wissenschaftlichen Publikation münden, für dessen Veröffentlichung die Gruppen weiterführende Betreuung erhalten.
Qualifikationsziele:
Nach Abschluss der Lehrveranstaltung sollen die Studierenden die Grundbegriffe der modernen Logik kennen. Sie verstehen die üblichen Resultate der klassischen Logiken (Aussagenlogik und Prädikatenlogik erster und höherer Stufe). Die Studierenden verstehen den Zweck von nicht-klassischen Logiken (wie Modallogik, Temporallogik, Konditionallogik, ...) und können insbesondere deren Verwendung in der (philosophischen) Argumentation beurteilen. Die Studierenden können mit Hilfe von Beweisassistenzsystemen formale Aussagen verifizieren oder widerlegen. Sie können fachsprachliche Texte über logische Grundlagen und Techniken aus dem Bereich der Informatik und Philosophie verstehen und sind in der Lage, Zusammenhänge zu bereits kennengelernten Themen selbstständig zu
erkennen. Am Ende der Veranstaltung sind die Studierenden in der Lage ausgewählte Themen der theoretischen Philopohie auf ihre logischen Kerninhalte zu reduzieren und mit Hilfe von geeigneten Techniken und Werkzeugen selbstständig zu formalisieren.
Veranstaltungsseite
Die Veranstaltungsseite ist unter http://www.inf.fu-berlin.de/users/lex/lehre/compmeta/ erreichbar.