God or Gödel - Did computer scientists prove that God exists?

 

Holy Logic: Computer Scientists 'Prove' God Exists

Anything of substance behind that catchy headline, or is it just a red herring?

Two scientists have formalized a theorem regarding the existence of God penned by mathematician Kurt Gödel.

 

But the God angle is somewhat of a red herring -- the real step forward is the example it sets of how computers can make scientific progress simpler.

 

As headlines go, it's certainly an eye-catching one. "Scientists Prove Existence of God," German daily Die Welt wrote last week.

 

But unsurprisingly, there is a rather significant caveat to that claim.

 

Not God but Gödel's theorem

 

In fact, what the researchers in question say they have actually proven is a theorem put forward by renowned Austrian mathematician Kurt Gödel -- and the real news isn't about a Supreme Being, but rather what can now be achieved in scientific fields using superior technology.

 

Even at the time, the argument was not exactly a new one. For centuries, many have tried to use this kind of abstract reasoning to prove the possibility or necessity of the existence of God.

 

But the mathematical model composed by Gödel proposed a proof of the idea. Its theorems and axioms -- assumptions which cannot be proven -- can be expressed as mathematical equations.  And that means they can be proven.

 

Proving God's existence with a MacBook

 

That is where Christoph Benzmüller of Berlin's Free University and his colleague, Bruno Woltzenlogel Paleo of the Technical University in Vienna, come in.

 

Using an ordinary MacBook computer, they have shown that Gödel's proof was correct -- at least on a mathematical level -- by way of higher modal logic.

 

Their initial submission on the arXiv.org research article server is called "Formalization, Mechanization and Automation of Gödel's Proof of God's Existence."

 

The fact that formalizing such complicated theorems can be left to computers opens up all kinds of possibilities, Benzmüller told SPIEGEL ONLINE.

 

"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," he said.

 

Who was Gödel?

 

The name Gödel may not mean much to some, but among scientists he enjoys a reputation similar to the likes of Albert Einstein -- who was a close friend.

 

Born in 1906 in what was then Austria-Hungary and is now the Czech city of Brno, Gödel later studied in Vienna before moving to the United States after World War II broke out to work at Princeton, where Einstein was also based.

 

The first version of this ontological proof is from notes dated around 1941, but it was not until the early 1970s, when Gödel feared that he might die, that it first became public.

 

A catchy headline always helps

 

Now Benzmüller hopes that using such a headline-friendly example can help draw attention to the method.

 

"I didn't know it would create such a huge public interest but (Gödel's ontological proof) was definitely a better example than something inaccessible in mathematics or artificial intelligence," the scientist added. 

 

"It's a very small, crisp thing, because we are just dealing with six axioms in a little theorem. … There might be other things that use similar logic. Can we develop computer systems to check each single step and make sure they are now right?"

 

The scientists, who have been working together since the beginning of the year, believe their work could have many practical applications in areas such as artificial intelligence and the verification of software and hardware.

 

Read more - http://www.spiegel.de/international/germany/scientists-use-computer-to-mathematically-prove-goedel-god-theorem-a-928668.html

 

****************************************************************************