University of Bamberg
open search form
You are here

Information Systems and Applied Computer Sciences

Chair for AI Systems Engineering (AISE)

  1.  University of bamberg
  2. Faculties
  3. Information Systems and Applied Computer Sciences
  4. Subject groups
  5. Applied Computer Science
  6. Chair for AI Systems Engineering (AISE)
  7. News
  8. "The God of the Logicians" – F.A.Z. Reports on the Gödel Conference at the BBAW
Headline of the F.A.Z. article “Der Gott der Logiker” (“The God of the Logicians”), Frankfurter Allgemeine Zeitung, 30 September 2026

"The God of the Logicians" – F.A.Z. Reports on the Gödel Conference at the BBAW

The Frankfurter Allgemeine Zeitung devotes a substantial feuilleton article to the Berlin conference on Kurt Gödel’s ontological argument for the existence of God – highlighting Christoph Benzmüller’s computer-supported work. This is part of ongoing, active research at the AISE chair and, at the Center for Innovative Applications of Computer Science (ZIAI), belongs to the working group AG Digitale Überlieferung.

Under the title „Der Gott der Logiker“ (“The God of the Logicians”), Ulf von Rauchhaupt reports in the Frankfurter Allgemeine Zeitung (feuilleton section, 30 September 2026) on the three-day conference „Kurt Gödel, ›Gott‹ und ›Teufel‹“ (“Kurt Gödel, God and Devil”), organised by Eva-Maria Engelen (University of Konstanz) and Alexander Englert (University of Richmond) at the Berlin-Brandenburg Academy of Sciences and Humanities (BBAW), 29–31 July 2026.

The article discusses Gödel’s philosophical notebooks and his reformulation of the ontological argument in a higher-order modal logic. In this context, the F.A.Z. also acknowledges the work of Christoph Benzmüller: as one of the two computer scientists who first verified this proof with a computer in 2014, he presented recent investigations into variants of Gödel’s proof at the conference.

The computer-supported analysis of Gödel’s argument is the subject of ongoing, active research at the Chair for AI Systems Engineering (AISE); at the Center for Innovative Applications of Computer Science (ZIAI) it belongs to the working group AG Digitale Überlieferung. Current questions include how logical interpretation choices affect the so-called modal collapse, how the formal models transfer across different proof assistants, and how the central claims can be established as elementarily and machine-checked as possible.

Current materials (freely available):

  • 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), pp. 569–611. doi.org/10.1007/s00605-025-02078-x
  • Isabelle/HOL dataset in the Archive of Formal Proofs – the machine-checked formalisation. 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

Recent talks on this topic:

  • ESSLLI 2026 (Charles University, Prague, 10–14 August 2026): the course “Experimenting with the LogiKEy Framework & Methodology” (with Luca Pasetto, University of Luxembourg). logikey.org
  • World Congress on Logic and Religion (WCLR 2026), Vancouver, September 2026: the talk “From Oracle to Auditor”. Slides (PDF)

The article first appeared in print (F.A.Z. no. 227, p. 12); a link to the online version will be added once available.