Springe direkt zu Inhalt

Computational Metaphysics

Christoph Benzmüller bei der Verleihung des Lehrpreises.

Christoph Benzmüller bei der Verleihung des Lehrpreises.
Bildquelle: Manuel Krane

Manuskript des Mathematikers Kurt Gödel, der die Existenz Gottes mit einem komplizierten Formelgebilde bewiesen hat.

Manuskript des Mathematikers Kurt Gödel, der die Existenz Gottes mit einem komplizierten Formelgebilde bewiesen hat.
Bildquelle: Freie Universität

Screenshot eines Beweis-Assistenz-Systems: Christoph Benzmüller verwendete es zur Bestätigung des Gottesbeweises von Gödel.

Screenshot eines Beweis-Assistenz-Systems: Christoph Benzmüller verwendete es zur Bestätigung des Gottesbeweises von Gödel.
Bildquelle: Christoph Benzmüller

Antragsteller: PD Dr. Christoph Benzmüller, Max Wisniewski und Alexander Steen, Institut für Informatik

Das Lehrvorhaben „Computational Metaphysics“ richtet sich an Masterstudierende aus den Studiengängen Philosophie, Mathematik und Informatik. In allen drei Studiengängen werden bereits im Grund- bzw. Bachelorstudium Grundlagen der formalen Logik gelehrt, auf die in der Lehrveranstaltung aufbaut wird. 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.

Das Projekt setzt sich aus einer Vorlesung und einer Übung zusammen. Die Vorlesung soll die heterogene Wissensbasis bei den Studierenden der unterschiedlichen Fachbereiche Philosophie, Mathematik und Informatik angleichen. Zusätzlich werden auch renommierte Spezialisten für Gastvorträge zu den behandelten Themen eingeladen.

In der Übung werden sich die Studierenden unter Anleitung bzw. Moderation selbstständig in Gruppen mit aktuellen Forschungsthemen beschäftigen. Nach erfolgreicher Einarbeitung in die theoretischen Grundlagen und die zum Einsatz vorgesehenen Beweisassistenzsysteme sollen die Teilnehmer/innen dazu befähigt werden, die erwähnten Arbeiten zur Verifikation des ontologischen Gottesbeweises mit einem Computersystem selbst nachzuvollziehen. Das Leitmotiv des ontologischen Gottesbeweises eignet sich besonders als roter Faden des Lehrvorhabens, da es einerseits ein philosophisch höchst anspruchsvolles und belebtes Thema ist und andererseits wichtige Konzepte der Modallogik verständlich demonstriert. Bis zum Ende des Semesters Zeit werden die Studierenden an einem ausgewählten Projekt zu arbeiten, das sie im Rahmen der Abschlussprüfung als Gruppe präsentieren.

PD Dr. Christoph Benzmüller ist seit 2012 Privatdozent an der Freien Universität Berlin. Ebenfalls 2012 erhielt er ein Heisenberg-Stipendium der Deutschen Forschungsgemeinschaft. Seit Oktober 2015 ist er für ein Jahr Visiting Scholar an der Stanford University.