The authors evaluate the soundness of the ontological argument they developed in their 1991 paper. They focus on Anselm’s first premise, which asserts that there is a conceivable thing than which nothing greater can be conceived. After casting doubt on the argument Anselm uses in support of this premise, the authors show that there is a formal reading on which it is true. Such a reading can be used in a sound reconstruction of the argument. After this reconstruction is developed (...) in precise detail, the authors show that the conclusion, a reading of the claim “God exists”, does not quite achieve the end Anselm desired. (shrink)

By a `denoting phrase' I mean a phrase such as any one of the following: a man, some man, any man, every man, all men, the present King of England, the present King of France, the center of mass of the solar system at the first instant of the twentieth century, the revolution of the earth round the sun, the revolution of the sun round the earth. Thus a phrase is denoting solely in virtue of its form. We may distinguish (...) three cases: (1) A phrase may be denoting, and yet not denote anything; e.g., `the present King of France'. (2) A phrase may denote one definite object; e.g., `the present King of England' denotes a certain man. (3) A phrase may denote ambiguously; e.g. `a man' denotes not many men, but an ambiguous man. The interpretation of such phrases is a matter of considerably difficulty; indeed, it is very hard to frame any theory not susceptible of formal refutation. All the difficulties with which I am acquainted are met, so far as I can discover, by the theory which I am about to explain. (shrink)

In this paper, the authors show that there is a reading of St. Anselm's ontological argument in Proslogium II that is logically valid (the premises entail the conclusion). This reading takes Anselm's use of the definite description "that than which nothing greater can be conceived" seriously. Consider a first-order language and logic in which definite descriptions are genuine terms, and in which the quantified sentence "there is an x such that..." does not imply "x exists". Then, using an ordinary logic (...) of descriptions and a connected greater-than relation, God's existence logically follows from the claims: (a) there is a conceivable thing than which nothing greater is conceivable, and (b) if <em>x</em> doesn't exist, something greater than x can be conceived. To deny the conclusion, one must deny one of the premises. However, the argument involves no modal inferences and, interestingly, Descartes' ontological argument can be derived from it. (shrink)

In this paper, the authors describe their initial investigations in computational metaphysics. Our method is to implement axiomatic metaphysics in an automated reasoning system. In this paper, we describe what we have discovered when the theory of abstract objects is implemented in PROVER9 (a first-order automated reasoning system which is the successor to OTTER). After reviewing the second-order, axiomatic theory of abstract objects, we show (1) how to represent a fragment of that theory in PROVER9's first-order syntax, and (2) how (...) PROVER9 then finds proofs of interesting theorems of metaphysics, such as that every possible world is maximal. We conclude the paper by discussing some issues for further research. (shrink)