What happens when you get two scientists and a MacBook? A theorem that proves that God exists of course.
Christoph Benzmüller of Berlin's Free University and his colleague, Bruno Woltzenlogel Paleo of the Technical University in Vienna looked at a theorem from the late Austrian mathematician Kurt Gödel using a Macbook and came up with a theory that proves God exists.
Gödel, who died in 1978, left an interesting theory based on principles of modal logic - that a higher being must exist. The details of the mathematics involved in Gödel's ontological proof are complicated, but in essence the Austrian was arguing that, by definition, God is that for which no greater can be conceived. And while God exists in the understanding of the concept, we could conceive of him as greater if he existed in reality. Therefore, he must exist, according to his theory.
Benzmüller and Paleo published their conclusions in their submission to arXiv.org, "Formalization, Mechanization and Automation of Gödel's Proof of God's Existence."
"It's totally amazing that from this argument led by Gödel, all this stuff can be proven automatically in a few seconds or even less on a standard notebook," Benzmüller told Spiegel Online.
They add: "The following has been done (and in this order): A detailed natural deduction proof. A formalization of the axioms, definitions and theorems in the TPTP THF syntax. Automatic verification of the consistency of the axioms and definitions with Nitpick. Automatic demonstration of the theorems with the provers LEO-II and Satallax. A step-by-step formalization using the Coq proof assistant. A formalization using the Isabelle proof assistant, where the theorems (and some additional lemmata) have been automated with Sledgehammer and Metis."
