Is to prove God like music to prove

Free University of Berlin

The consistency of Gödel's basic assumptions was proven by the computer. The scientists were also able to show that the nontrivial evidence can be generated fully automatically by the computer for the most part. The two scientists hadn't expected that. Beyond the use of theorem provers in philosophy and mathematics, such systems could be used in dialogue systems in the future, so that computers can understand and even supplement human argumentation patterns.

The “logical formalism” used by Gödel - a so-called higher-level modal logic that uses terms such as “necessary” and “possible” - was previously considered to be too complex and difficult to map and automate on the computer. Available theorem provers are mostly based on much simpler formalisms. To get around this problem, the scientists used a method that enabled them to automate Gödel's higher-level modal logic using existing theorem provers. This trick is in turn based on theoretical work by Benzmüller and Paulson from the University of Cambridge in the UK. Several theorem provers have been developed for classical higher-level logic in the last two decades. These could now be used successfully in the work of Benzmüller and Woltzenlogel Paleo. A theorem prover developed by Benzmüller was also used.

Kurt Gödel's mathematized proof of God was published after his death. It belongs to the class of so-called ontological proofs, which have a long tradition in philosophy: As constructions of pure thinking, they have been and have been discussed very controversially in the professional world. Starting from abstract concepts that abstract from experience, the existence of God is inferred from a few basic assumptions (axioms) in an ontological proof of God with the help of a logical argument. Conversely, one can say that the existence of God is reduced to the validity of axioms and abstract concepts.

Well-known philosophers have dealt intensively with ontological proofs of God, including St. Anselm, Descartes, Leibniz and Kant. Two questions are important for such proofs: (A) Are the respective basic assumptions valid and sensibly chosen? (B) Is the logical line of reasoning actually flawless? The preoccupation with question (A) is the task of philosophy and theology, and ontological proofs of God have often and rightly been heavily criticized on this point. Dealing with question (B) is the task of mathematical and philosophical logic. Especially for Gödel's proof of God, however, the logic formalism used and Gödel's argumentation are not trivial. The analysis of the logical aspects has so far been carried out exclusively - laborious and error-prone - with paper and pencil.

The two scientists now want to investigate Gödel's proof further, including more recent work that criticizes deeper logical aspects of Gödel's work. They also want to use their method to check other ontological proofs of God for their logical validity in the future. Logical formalism and basic assumptions can then be understood as changeable parameters. The scientists then want to experiment with these parameters in the theorem prover in order to gain new insights into the logical structure of the arguments. In this respect, the scientists are convinced that there are interesting perspectives for a computer-assisted theoretical philosophy and metaphysics; Scientists expect to be able to effectively and flexibly check the validity of conclusions based on basic assumptions.

The age-old question about the existence of God naturally remains unanswered and depends on the meaningfulness and reality of the chosen basic assumptions. However, Gödel's chain of arguments is verifiably correct - according to the scientists, the computer has now shown that much.

A translation of Gödel's proof sketch (in the version of Gödel's student Dana Scott) from formal logic into natural language:

  • Assumption 1: Either a property or its negation is positive.
  • Assumption 2: A quality that is necessarily implied by a positive quality is positive.
  • Theorem 1: Positive properties possibly apply to an existing entity.
  • Definition 1: A god-like entity has all the positive qualities.
  • Assumption 3: The quality of being godlike is positive.
  • Conclusion: God may exist.
  • Assumption 4: Positive qualities are necessarily positive.
  • Definition 2: A property is the essence of an entity if it belongs to the entity and necessarily implies all properties of the entity.
  • Theorem 2: Being godlike is an essence of every godlike entity.
  • Definition 3: An entity necessarily exists if and only if all of its essences are necessarily realized in an existent entity.
  • Assumption 5: Necessarily existing is a positive quality.
  • Theorem 3: God necessarily exists.