A Computationally-Discovered Simplification of the Ontological Argument
Paul E. Oppenheimer and Edward N. Zalta
Australasian Journal of Philosophy, 89/2 (June 2011): 333–349.
The authors investigate the ontological argument computationally. The
premises and conclusion of the argument are represented in the syntax
understood by the automated reasoning engine PROVER9.
Using the logic of definite descriptions, the authors developed a
valid representation of the argument that required three non-logical
premises. PROVER9, however, discovered a simpler valid
argument for God's existence from a single non-logical premise.
Reducing the argument to one non-logical premise brings the
investigation of the soundness of the argument into better focus.
Also, the simpler representation of the argument brings out clearly
how the ontological argument constitutes an early example of a
‘diagonal argument’ and, moreover, one used to establish a
positive conclusion rather than a paradox.
[Preprint available online in PDF]