Computational Theology
In computer science and mathematics, there is a long tradition of computational proof: using a computer program to derive mathematical proofs from a series of axioms. So two philosophers decided to connect this to Anselm. When they set out to have a computer program prove the ontological argument, not only were they successful, they actually made his argument more elegant. As described in Wikipedia:
Paul Oppenheimer and Edward Zalta used an automated theorem prover—Prover9—to validate Anselm’s ontological thesis. Prover9 subsequently discovered a simpler, formally valid (if not necessarily sound) ontological argument from a single non-logical premise.
Separate from whether the proof “works,” it’s quite impressive that a computer program was able to distill this argument to its simplest form, allowing one to examine it as clearly as possible. In this case, the entire argument rests on the premise “if the conceivable thing than which nothing greater is conceivable fails to exist, then something greater than it is conceivable”, which the authors find wanting. But as the philosophers wrote in their 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.
http://www.wired.com/2014/09/computational-theology/
= new reply since forum marked as read
