A Computational Implementation of the Ontological Argument (Corrected)

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:

  1. Argument A: The representation of the argument in first-order logic with identity and definite descriptions, as presented in the paper Oppenheimer & Zalta 1991 (“On the Logic of the Ontological Argument”). In this paper, we argued Anselm needed three non-logical premises to prove God's existence.
  2. Argument B: The representation of Argument A in PROVER9, as developed in the paper Oppenheimer & Zalta 2011 (“A Computationally-Discovered Simplification of the Ontological Argument”). We now think this representation isn't as faithful to Argument A as it could have been. Consequently, Argument B no longer appears on this page; it is available on the previous version of this webpage
  3. Argument C: A more faithful representation of Argument A in PROVER9, as presented below.
  4. Argument D: A simplified version of Anselm's argument represented in first-order logic with identity and definite descriptions, as presented in the paper Oppenheimer & Zalta 2011 (“A Computationally-Discovered Simplification of the Ontological Argument”). This argument shows how Anselm could derive God's existence from a single non-logical premise. Argument D was discovered as a result of our work in formulating Argument B.

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.

  1. The Tools You Will Need
  2. A Computational Implementation of the Ontological Argument
  3. A Simplification of the Ontological Argument

1. The Tools You Will Need

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.

2. A Computational Implementation of the Ontological Argument

2.1 Argument A: The Logic of the Ontological Argument (1991)

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. ¬Exφ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. Exφ1 from (5), (6), (7), by Reductio
9. E!g from (8), by the definition of ‘g

2.2 Representing Descriptions in PROVER9

To represent the above in PROVER9, we need to translate the notation of the first-order predicate calculus with identity and definite descriptions into the PROVER9 syntax. Since there are no definite descriptions in PROVER9 syntax, we shall have to find a way to represent the Description Axiom and its consequences, Description Theorem 1, 2, and Lemma 1, without using definite descriptions explicitly. Once we do this, the Description Axiom and the description theorems will be transformed into other logical axioms and theorems that capture the reasoning.

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).

2.3 Representing The Non-Logical Premises, Theorems, and Definitions

The Connectedness of the Greater Than Relation

Our 1991 formulation revealed that only a very weak condition on the greater than relation is required for the ontological argument, namely, its connectedness:
Connectedness of Greater Than: ∀xy(GxyGyxx=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))).

Premise 1

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.

Premise 2

The final premise needed for the argument is:

Premise 2: ¬Exφ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

Given that we are replacing the axioms and theorems for definite descriptions with the Unique Exemplification Axiom and the Bridge Principle, we can move directly to the representation of Lemma 2. Lemma 2 states an interesting result that follows from the connectedness of the greater than relation, namely, if there is something than which none greater can be conceived, then there is a unique thing than which none greater can be conceived:
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:

Definition of “God”

We omit the definition of God when representing the argument in PROVER9 because as soon as we introduce a new constant, say g, into the representation, PROVER9 will introduce a domain element to model it. Consequently, in the following representation, the conclusion of the argument simply is the claim:
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.

2.4 Argument C: The Ontological Argument in PROVER9

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:

3. Argument D: A Simplification of the Ontological Argument

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:

  1. In Argument B, we inadvertently contaminated the representation of the predication RaιxGx (the left condition of Russell’s axiom) with the representation of the logical claim ∃y(y = ιxφ) (the consequent of Description Theorem 1) by using the same formula in PROVER9, namely, Is_the(x,F). See the old representation here, where RaιxGx is represented as Is_the(x,F) & Ex1(G,x) and ∃y(y = ιxφ) is represented as exists u (Object(u) & Is_the(u,F)). This made it too easy for PROVER9 to prove Description Theorem 1 (it invokes the right-to-left direction of the Russell axiom). We repaired this in our work above by more carefully distinguishing the PROVER9 formulas used to represent RaιxGx and ∃y(y = ιxφ).
  2. Moreover, we used PROVER9 system identity to represent the claim ∃y(y = ιxφ), as we just saw. But PROVER9 system identities don’t have the right form to be used with Russell’s axiom. More precisely, the left-side of Russell’s axiom is RaιxGx, but a PROVER9 system identity x=y doesn’t have the form of a predication. A formula of the form a = ιxφ (in first-order logic with identity, where = is a distinguished relation term) is really of the form Raιxφ. This resolves identities with descriptions to a formula that subject to Russell’s axiom. So, we corrected this above by introducing a new relation, id, into the PROVER9 representations.
  3. In addition, in Argument A, the natural deduction framework permitted the definition of “God” to be introduced only after the definite description “the conceivable thing than which no greater can be conceived” had been proved to have a denotation. In Argument B, however, we did not take account of the fact that the refutation framework did not provide a way of delaying the introduction of the abbreviation. Moreover, Argument B PROVER9 forced the automated engine to introduce a domain element for the constant g, for we introduced the constant using the axiom Is_the(g,none_greater). The representation we are now offering doesn’t use the constant g at all; we now take the conclusion of the argument to be exists x (Object(x) & Is_the(x, none_greater) & Ex1(e,x)) and let the conclusion “God exists” follow from this by definition of “God” (g) as Is_the(g, none_greater).

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.