From philosophy to math: Gödel's proof of God's existence

Kurt Gödel was a famous mathematician and philosopher who later became friends with Albert Einstein.
http://en.wikipedia.org/wiki/Kurt_G%C3%B6del

A german group of mathematicians has translated Kurt Gödel's proof of God's existence into a formal logical language and tested it, by computing it with suitable software. The result was that Gödel's deduction was correct. Some further results on the behavior of that logical system were also yielded.
(An article said, that the computation itself took less than a minute.)

Excerpt:
"Gödel defines God as a being who possesses all positive properties. He does not extensively discuss what positive properties are, but instead he states a few reasonable (but debatable) axioms that they should satisfy. Various slightly different versions of axioms and definitions have been considered by Gödel and by several philosophers who commented on his proof."

The axioms:
A1 Either a property or its negation is positive, but not both:
A2 A property necessarily implied by a positive property is positive:
A3 The property of being God-like is positive:
A4 Positive properties are necessarily positive:

http://arxiv.org/abs/1308.4526
http://arxiv.org/pdf/1308.4526v3.pdf