Computer Program Attempts to Prove the Existence of God
The existence or non-existence of God is likely one of life's great unanswerable questions, but that hasn't stopped philosophers from crafting well-reasoned and logically valid arguments that he exists. Anselm's ontological thesis is one such argument, although it has often been criticized as neither well-reasoned nor logically valid. Then, Stanford researchers Paul Oppenheimer and Edward Zalta, who research within a field called "computational theology," used a computer program called Prover9 in order to formulate a logically valid proof from Anselm's argument.
Anselm defined God as "...that than which nothing greater can be conceived." Since we conceive of this "greatest" being, he exists in our minds. But if he only existed in our minds, then he wouldn't actually be greater than anything we can conceive, because we would be able to conceive of a greater being that exists in reality. Essentially, God must exist because existing is greater than failing to exist. Many famous arguments against Anselm have arisen over the years; the first, Gaunilo of Marmoutiers, employed reductio ad absurdum by proving that Anselm's argument (later called the ontological argument) could be used to prove the existence of anything, illustrated with the example of the "perfect island." One of the other most famous arguments came from Immanuel Kant, who asserted that Anselm's argument was not logically valid because it did not follow that the greatest being would be less great if it didn't exist.
The Prover9 did not perfect this extremely flawed and non-logical argument, but it made it logically valid and reduced its non-logical premises from three to one. In other words, two out of the three assertions that are needed to draw the conclusion are true in and of themselves. The third is a non-logical statement that would need its own separate argument to be proven. So they still don't believe that the argument is sound, but the program was able to distill it into its most logical form in order to allow for the most precise examination of the argument, and it demonstrated the unexpected level of elegance in a long-derided theory.
The refined argument in plain language reads something like this:
1. Nothing greater is conceivable than the conceivable thing than which nothing greater is conceivable.
2. If the conceivable thing than which nothing greater is conceivable fails to exist, then something greater than it is conceivable.
3. Therefore, the conceivable thing than which nothing greater is conceivable does not fail to exist.
From the paper: "Anselm's ontological argument has come in for criticism ever since it was first proposed. But we think that the focus on finding flaws in the argument may have hindered progress in logically representing the argument in its most elegant form. We hope to show that computational techniques offer a new insight into Anselm's ontological argument and demonstrate that there is much beauty inherent in its logic."