„Der Gott der Logiker“ – F.A.Z. berichtet über die Gödel-Tagung an der BBAW
Unter dem Titel „Der Gott der Logiker“ berichtet Ulf von Rauchhaupt in der Frankfurter Allgemeinen Zeitung (Feuilleton, 30. September 2026) über die dreitägige Tagung „Kurt Gödel, ›Gott‹ und ›Teufel‹“, die Eva-Maria Engelen (Universität Konstanz) und Alexander Englert (University of Richmond) vom 29. bis 31. Juli 2026 an der Berlin-Brandenburgischen Akademie der Wissenschaften (BBAW) veranstaltet haben.
Der Beitrag beleuchtet Gödels philosophische Notizbücher und seine Neufassung des ontologischen Arguments in einer höherstufigen Modallogik. In diesem Zusammenhang würdigt die F.A.Z. auch die Arbeiten von Christoph Benzmüller: Als einer der beiden Informatiker, die diesen Beweis 2014 erstmals computergestützt verifizierten, stellte er auf der Tagung neuere Untersuchungen zu Varianten des Gödel’schen Beweises vor.
Die computergestützte Analyse des Gödel’schen Arguments ist Gegenstand fortlaufender, aktiver Forschung am Lehrstuhl für KI-Systementwicklung (AISE); am Zentrum für innovative Anwendungen der Informatik (ZIAI) gehören sie zur AG Digitale Überlieferung. Untersucht werden unter anderem, wie logische Interpretationsentscheidungen den sogenannten modalen Kollaps beeinflussen, wie sich die formalen Modelle in unterschiedliche Beweisassistenten übertragen lassen und wie sich die zentralen Aussagen möglichst elementar und maschinengeprüft absichern lassen.
Aktuelle Materialien (frei verfügbar):
- C. Benzmüller & D. S. Scott, „Notes on Gödel’s and Scott’s variants of the ontological argument“, Monatshefte für Mathematik 208 (2025), S. 569–611. doi.org/10.1007/s00605-025-02078-x
- Isabelle/HOL-Datensatz im Archive of Formal Proofs – die maschinengeprüfte Formalisierung. isa-afp.org
- „A Comment on Modal Collapse and Ultrafilters in Gödel’s Ontological Argument“ (arXiv:2608.07578, 2026). arxiv.org/abs/2608.07578
- „Gödel’s and Scott’s Variants of the Ontological Argument in Lean 4 and TPTP THF“ (arXiv:2609.26806, 2026). arxiv.org/abs/2609.26806
- „Proofs Without Nominals: …“ (arXiv:2609.36279, 2026). arxiv.org/abs/2609.36279
Aktuelle Vorträge zum Thema:
- ESSLLI 2026 (Karls-Universität Prag, 10.–14. August 2026): Kurs „Experimenting with the LogiKEy Framework & Methodology“ (mit Luca Pasetto, Universität Luxemburg). logikey.org
- World Congress on Logic and Religion (WCLR 2026), Vancouver, September 2026: Vortrag „From Oracle to Auditor“. Folien (PDF)
Der Artikel erschien zunächst in der Printausgabe (F.A.Z. Nr. 227, S. 12); ein Link zur Online-Fassung wird ergänzt, sobald er verfügbar ist.