This webpage has been updated (May 28, 2017) to correct the information that previously resided at this URL.
In what follows, we refer to four representations of Anselm's Ontological argument for the existence of God:
This updated webpage explains why we think Argument B is not a completely faithful representation of Argument A. Argument A assumes a language in which definite descriptions are genuine terms, and when we translated Argument A into PROVER9’s language (without descriptions) to obtain Argument B, our choices about how to eliminate the descriptions were not optimal. We now believe that there is a better way to eliminate the descriptions. The result is Argument C below.
However, our work on Argument B in the 2011 paper really did lead us to find that there is a simpler version of Anselm's Ontological Argument, in which God's existence becomes derivable from a single premise. This is Argument D below. When we input Argument B into PROVER9, it did find a proof that led us to realize that a single non-logical premise could be used to derive God's existence. Argument D emerged because the representational techniques we used to obtain Argument B from Argument A gave PROVER9 an edge. Once descriptions are properly eliminated from Argument A, PROVER9 needs all three premises to derive God’s existence. This is evidenced by Argument C below, which presents a new (and proper) representation of Argument A in PROVER9. Comparison of Argument C below with Argument B (found in the the earlier version of this page) may help one to see why we now prefer Argument C.
NOTE: The files below all work correctly with the June 2007 version of PROVER9 and with the graphical application. They may also work with later versions, but they were all checked with the June 2007 version. You can download these versions of PROVER9 from the following links:
Assuming that you have installed PROVER9, you can download the input and output files linked in below and process them. The standard command-line syntax for running PROVER9 is:
prover9 < theorem.in
or, if you want to append PROVER9’s output to a file:
prover9 < theorem.in > theorem.out
If you need further help in running PROVER9, you can consult the manual that goes with the June 2007 version of PROVER9, which can be accessed here.
Similarly, one can use MACE4 to find models of the premises used in the proof of each theorem. This provides a finite verification of the consistency of the axioms and definitions. The standard command-line syntax for running MACE4 is (unless otherwise noted):
mace4 -c -N 8 -p 1 < model.in
or, if you want to append MACE4’s output to a file,
mace4 -c -N 8 -p 1 < model.in > model.out
For your convenience, we’ve also included links to the PROVER9 and MACE4 output files for each theorem, for the runs we have executed. You can compare your runs to ours.
We shall assume familiarity with the formalization of Anselm’s Ontological Argument as presented in the paper Oppenheimer & Zalta 1991. That representation uses the following premises, where:
φ1 = Cx & ¬∃y(Gyx & Cy)
and where φ[τ/x] indicates the formula which is just like φ except that occurrences of the variable x are replaced by occurrences of the term τ:
The argument also uses the following background logical axioms, theorems, and lemmas:
Finally, we use the following Lemma and Definition, where φ1 is Cx & ¬∃y(Gyx & Cy)
Then Anselm’s Ontological Argument, as represented in Oppenheimer & Zalta 1991, proceeds as follows:
1. ∃xφ1 Premise 1 2. ∃!xφ1 from (1), Lemma 2 3. ∃y(y = ιxφ1) from (2), Description Theorem 1 4. Cιxφ1 & ¬∃y(Gyιxφ1 & Cy) from (3), by Description Theorem 2. 5. ¬E!ιxφ1 assumption for reductio 6. ∃y(Gyιxφ1 & Cy) from (5), Premise 2 7. ¬∃y(Gyιxφ1 & Cy) from (4), by &E 8. E!ιxφ1 from (5), (6), (7), by Reductio 9. E!g from (8), by the definition of ‘g’
It turns out that all we need by way of reasoning in a language without descriptions is to:
Specifically, we first introduce the predication Is_the(x,F) and axiomatize it in PROVER9 by asserting the Unique Exemplification Axiom, namely, that if x is the F, then x is F and anything that is F is identical to x. We formalize this in PROVER9 syntax as:
Unique Exemplification Axiom:
all x all F ((Object(x) & Relation1(F)) -> (Is_the(x,F) <-> (Ex1(F,x) & (all z ((Object(z) & Ex1(F,z)) -> Ex2(id,x,z)))))).
Next, we introduce the 2-place relation of identity, id, and axiomatize it by asserting both that id is a relation and that it holds between any two items in the domain of discourse if and only if system identity holds between those objects. We call this the Bridge Principle:
The Bridge Principle:
all x all y (Ex2(id,x,y) <-> x=y).
Connectedness of Greater Than: ∀x∀y(Gxy ∨ Gyx ∨ x=y).
This asserts that for every distinct pair of objects, either the first is greater than the second or the second is greater than the first. We represent this in PROVER9 as follows:
all x all y ((Object(x) & Object(y)) -> (Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | Ex2(id,x,y))).
To represent Premise 1, we need to introduce a new predicate and make sure that it behaves correctly, from a logical point of view. The new predicate is none_greater and it requires both a definition and a ‘sorting’ principle:
Definition of none_greater:
all x (Object(x) -> (Ex1(none_greater,x) <-> (Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))).Sorting Principle for none_greater
Relation1(none_greater).
The definition says: an object x exemplifies being none_greater if and only if no object greater than x is conceivable. The sorting principle says that none_greater is a 1-place relation.
Given this predicate, we can represent Premise 1 in PROVER9 syntax. Recall that Premise 1 asserts:
∃xφ1.
If we unpack the definition of φ1, this becomes:
Premise 1: ∃x(Cx & ¬∃y(Gyx & Cy))
In this premise, the expression “Cx” asserts that x is conceivable, and so Premise 1 asserts that there is something which is conceivable and such that there is nothing y which is greater than x and conceivable. So we can represent Premise 1 in PROVER9 very simply as follows:
exists x (Object(x) & Ex1(none_greater,x)).
Note here how our definition of the property none_greater is the counterpart in PROVER9 to the abbrevation φ1 that we used in object theory.
The final premise needed for the argument is:
Premise 2: ¬E!ιxφ1 → ∃y(Gyιxφ1 & Cy)
This asserts that if the conceivable thing such that nothing greater is conceivable doesn’t exist, then there is something greater than it which is conceivable. If we use our property none_greater, then we can represent Premise 2 as the following general claim, using ‘e’ as the property of existence:
-(exists x(Object(x) & Is_the(x,none_greater) & Ex1(e,x))) ->
(all z ((Object(z) & Is_the(z, none_greater)) ->
exists y (Object(y) & Ex2(greater_than,y,z) & Ex1(conceivable,y)))).
This says: if it is not the case that there is an object x such that (a) x is the unique conceivable thing than which none greater can be conceived and (b) x exists, then for any object z, if z is the unique conceivable thing than which none greater can be conceived, then there exists an object y such that nothing greater can be conceived and is conceivable.
Lemma 2: ∃xφ1 → ∃!xφ1
The importance of this lemma cannot be overstated, for it validates the introduction of the definite description into Anselm’s language. It justifies his use of the expression “the (conceivable) x such that nothing greater is conceivable”.
We can represent this claim in PROVER9’s syntax as follows:
exists x (Object(x) & Ex1(none_greater,x)) ->
exists x (Object(x) & Ex1(none_greater,x) &
(all y (Object(y) -> (Ex1(none_greater,y) -> y=x)))).
This tells us that if some Object x exemplifies the none_greater property, then a unique Object x does. Here are the input and output files for both the theorem and the model of the premises:
Conclusion of Ontological Argument:
exists x (Object(x) & Is_the(x, none_greater) & Ex1(e,x)).
This asserts: there is an object x that is_the none_greater and that exemplifies existence. Clearly, this conclusion suffices, for given that conclusion, Anselm can conclude that God exists, by defining ‘God’ as the x such that x is the none_greater.
The above representations are combined into the following input files, which enable PROVER9 to find a “proof” of God's existence from the three non-logical premises:
We then checked that all the premises from all the theorems and lemmas, as well as the premises needed to rule out unintended models, are jointly consistent:
Though the above representation of the ontological argument in PROVER9 validates that the conclusion follows from the three premises (the connectedness of greater than, Premise 1, and Premise 2), our original representation of the argument in PROVER9 didn’t optimally eliminate the descriptions. The representations we used, together with PROVER9’s operations on them, led us to discover a simplified version of Anselm’s Proslogion 2 ontological argument, on the basis of the output from PROVER9’s operation on those less faithful representations. Here is a simplified version of the argument, which uses Description Theorem 3, namely, ψ[ιxφ/x] → ∃y(y = ιxφ), where ψ is any atomic or identity formula with x free:
1. ¬E!ιxφ1 Assumption for reductio 2. ∃y(Gyιxφ1 & Cy) from (1), by Premise 2 and MP 3. Ghιxφ1 & Ch from (2), by EE, ‘h’ arbitrary and new 4. Ghιxφ1 from (3), by &E 5. ∃y(y = ιxφ1) from (4), by Description Theorem 3 6. Cιxφ1 & ¬∃y(Gyιxφ1 & Cy) from (5), by Description Theorem 2 7. ¬∃y(Gyιxφ1 & Cy) from (6), by &E 8. E!ιxφ1 Reductio (1); (2) vs. (7) 9. E!g from (8), by definition ‘g’
The above argument is a perfectly valid and interesting representation of the ontological argument despite having emerged as a result of the following mistakes in representation:
Some of these points were noticed by P. Garbacz, in his 2012 paper “PROVER9’s Simplification Explained Away” (Australasian Journal of Philosophy, 90(3): 585–592.
As a result of these issues affecting Argument B, PROVER9 did find a "simple proof" of the conclusion that didn't make use of all of the premises we fed it. This led us to formulate Argument D. PROVER9's output for Argument B made a connection we hadn’t seen ourselves, namely Description Theorem 3 (below). When we studied PROVER9’s proof of God’s existence using Argument B, we discovered it didn’t use Description Theorem 1, the connectedness of greater than, Premise 1, or Lemma 2. Instead it found a proof from Premise 2, the definition of God, and Description Theorem 2. Inspired by the this result, we constructed Argument D using standard logical notation and using only premise that PROVER9 used, together with this additional logical theorem schema concerning definite descriptions:
Description Theorem 3: ψιxφx → ∃y(y = ιxφ), where ψ is any atomic or identity formula with x free.
Description Theorem 3 is derivable from the Description Axiom. The derivation is given in the 2011 paper on page 15 in note 13.
Argument D is correct and interesting, but it is not the proof that PROVER9 found when given Argument B as input. The proof found by PROVER9 from Argument B suffers from the weaknesses of that representation.