Kurt Gödel (1906-1978) proposed an argumentation formalism to prove the necessary existence of God. In a current collaboration we have succeeded to formalise, mechanize and (partly) automate Gödel's ontological argument with modern higher-order theorem provers on a computer. This work has attracted significant media attention in recent weeks.

Attempts to prove the existence (or non-existence) of God by means of abstract, ontological arguments are an old tradition in Philosophy. Before Gödel, already St. Anselm, Descartes und Leibniz have presented similar arguments. What motivated Gödel as a logician was the question, whether it is possible to deduce the existence of God from a small number of (debatable) foundational axioms and definitions, with a mathematically precise and logically formal argumentation chain.

The core proposition, the necessary existence of God, was divided in our work in four argumentation steps, as proposed by Gödel, and each step was proved and verified with an automated theorem prover. Also the consistency of the axioms and definitions was analyzed and established automatically with the help of a computer.

In theoretical philosophy, formal logical confrontations with ontological arguments had been so far limited to pen and paper. Up to now, the use of computers was prevented, because the "logics" of the available theorem proving systems were not expressive enough to formalize the abstract concepts adequately. Gödel's proof uses, for example, a complex higher-order modal logic to handle concepts such as "possible" and "necessary".

Recent works of Benzmüller and Larry Paulson (Cambridge University, UK) show that many expressive logics, including higher-order modal logics, can be embedded into the classical higher-order logic, which can be seen as a universal logic. For this universal logic, efficient automated theorem provers have been developed in recent years, and these systems were now employed in our work on Gödel's proof.

Our approach opens up new perspectives for a computer-assisted theoretical philosophy. The critical discussion of the underlying concepts, definitions and axioms remains a human responsibility. But the computer can help to avoid mistakes of a logical nature: the computer can check the argumentation chain and partially fulfill Leibniz' dictum in case of logical disputes: Calculemus --- Let us calculate! 

Hompepage Bruno Woltzenlogel Paleo                                                          

Homepage Christoph Benzmüller