1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.
!The following paper is forthcoming in the Australasian Journal