A Computational Implementation of the Ontological Argument

In this project, we used PROVER9 to implement the reading of Anselm's ontological argument developed in the 1991 paper by Oppenheimer and Zalta (‘On the Logic of the Ontological Argument’). Our paper offered a reading of the argument in Anselm's Proslogion II, and it developed the underlying logic of descriptions, the three non-logical premises, and the one definition (of "God"). (Here is the Jonathan Barnes Translation of Anselm's Proslogion II.)

However, to our surprise, PROVER9 found a simplification of the argument. It found an argument for God's existence that required only one non-logical premise instead of three. In what follows, we rehearse the argument from our 1991 paper and then show how to turn PROVER9's simplified argument into an argument, in familiar first-order syntax, that uses a single non-logical premise!

A more complete discussion of the material below can be found in the paper ‘A Computationally-Discovered Simplification of the Ontological Argument’, by Paul E. Oppenheimer and Edward N. Zalta.

  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

In the following formulas, we use φ[y/x] to indicate the formula which is just like φ except that occurences x are replaced by occurences of y.

2.1 The Logical Axioms and Theorems

The Description Axiom

The Description Axiom derives from Russell's theory of description. It can be formulated as follows:
Description Axiom: Where ψ is any atomic formula or identity formula in which z occurs free, and φ is any formula in which x is free, the following is an axiom:
ψ[ιxφ/z] ≡ ∃y(φ[y/x] & ∀u(φ[u/x] → u=y) & ψ[y/z] )

This is an axiom schema that encapsulates Russell's theory of definite descriptions. It says: the object x such that φ satisfies the (atomic or identity) formula ψ if and only if there is something y which: (a) is such that φ, (b) is such that anything u such that φ is identical to it, and (c) is such that ψ. As an example, let "Raz" be our formula ψ and let "Gx" be φ, where R and G are variables. Then the following is an instance of the Description Axiom:

RaιxGx ≡ ∃y(Gy & ∀u(Guu=y) & Ray)

In PROVER9 we cannot formulate schemata, but we can formulate universal generalizations of their instances. So, for example, the following generalization would capture a certain class of instances of the axiom:

all x all G all R(Object(x) & Relation1(G) & Relation2(R) -> 
  ((Is_the(x,G) & Ex2(R,a,x)) <-> 
    exists y (Object(y) & Ex1(G,y) &
      all u (Ex1(G,u) -> u=y) & Ex2(R,a,y))))

Description Theorem 1

Description Theorem 1 is a logical theorem schema and is a consequence of the Description Axiom. In classical notation with metavariables ranging over formulas, we may state the theorem as follows:

Description Theorem 1: ∃!xφ → ∃y(y = ιxφ)

This is a theorem schema, which we might read as follows: if there is a unique object x which is such that φ then the x such that φ is something. In semantic terms, if something uniquely satisfies φ then the definite description "the x such that φ" has a denotation. Since we cannot represent a theorem schema in PROVER9, the best we can do is use generality (i.e., quantifiers) and our typed variables to claim: if there is a unique oject x which exemplifies property F, then the some object x is the F. Thus, we are using a property variable F instead of the metavariable φ:

 all F (Relation1(F) ->
   ((exists y (Object(y) & Ex1(F,y) &
     (all z (Object(z) ->(Ex1(F,z) -> z=y))))) ->
        (exists u (Object(u) & Is_the(u,F))))).
 

This tells us that for every property F, if there is an object y that (a) exemplifies F and (b) is such that anything z that exemplifies F is identical to it, then there is an object u which is the F. Here are the input and output files for both the theorem and the model of the premises:

For interested readers, the document Clausifying Description Theorem 1 explains the steps that are needed to turn the above representation of this theorem in PROVER9 syntax into clausal normal form.

Lemma 1

Lemma 1 is used to prove Description Theorem 2. It states:
Lemma 1: τ = ιxφ → φ[τ/x]

Though this theorem schema cannot be represented in the syntax of PROVER9, we can approximate it with the following claim:

all x all F all y ((Object(x) & Relation1(F) & Object(y)) -> 
	((Is_the(x,F)  & x=y) -> Ex1(F,y))).

This tells us, for any object x, property F and object y, that if x is the F and x=y, then y exemplifies F. Here are the input and output files for both the theorem and the model of the premises:

Description Theorem 2

Description Theorem 2 plays a role in the ontological argument. It may be formulated as follows:
Description Theorem 2: ∃y(y = ιxφ) → φ[ιxφ/x]

Again, this is a theorem schema, and in the syntax of PROVER9, we represent it in terms of the following general claim:

all F (Relation1(F) ->
  ((exists y (Object(y) & Is_the(y,F))) ->
    (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z)))))).

This asserts, for any property F, that if something y is the F, then anything z that is the F exemplifies F. Here are the input and output files for both the theorem and the model of the premises:

2.2 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) | x=y)).

Premise 1

The first premise needed for the argument is:
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. In Oppenheimer and Zalta 1991, we abbreviated Premise 1 using the following abbreviation:

φ1 abbreviates Cx & ¬∃y(Gyx & Cy).

Thus, we often formulate Premise 1 as:

xφ1.

To represent Premise 1 in PROVER9, we introduced the property none_greater to represent the open formula "x is conceivable and such that nothing greater than x is conceivable", as follows:

all x (Object(x) -> (Ex1(none_greater,x) <->
  (Ex1(conceivable,x) &
    -(exists y (Object(y) & Ex2(greater_than,y,x) &
      Ex1(conceivable,y)))))).

With this definition, we may represent Premise 1 in PROVER9 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.

Lemma 2

The following was an interesting result described in Oppenheimer and Zalta 1991, namely, that if greater than is connected, then if there is something than which none greater can be conceived, then there is a unique thing than which none greater can be conceived. This is capture by Lemma 2:
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".

Though this theorem schema cannot be represented in the syntax of PROVER9, we formulate a very general first-order claim that captures its intent:

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:

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:

all x (Object(x) ->
  ((Is_the(x,none_greater) & -Ex1(e,x)) ->
    exists y (Object(y) & Ex2(greater_than,y,x) &
      Ex1(conceivable,y)))).

This says: for any object x, if x is that than which none greater can be conceived and fails to exemplify existence, then some object y is such that nothing greater can be conceived and is conceivable.

Definition of "God"

We defined "God" ("g") in our original paper as follows:
g   =df   ιxφ1

Since PROVER9 doesn't have primitive descriptions, we defined God as follows in PROVER9 syntax:

 Is_the(g,none_greater)

Interested readers may examine the document The Clausification of the Premises to see how each of the above premises, logical and non-logical, gets clausified into clausal normal form.

2.3 The Ontological Argument

The conclusion of the ontological argument, as formulated in 1991, is claim "E!g", where g is defined as above. But the conclusion in PROVER9 syntax is: Ex1(e,g).

Given the Premise 1, Premise 2, the definition of none_greater, and the definition of God, we use the theorems Lemma 2 and Description Theorems 1 and 2 to produce the following input (and output) files for the ontological argument:

3. A Simplification of the Ontological Argument

PROVER9 indeed discovered a proof of God's existence from the above input file, but a close examination of the proof shows that 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. We can therefore extract a human-readable proof in standard logical notation that uses only the premises that PROVER9 used. It will be helpful to have the following logical theorem schema in mind:
Description Theorem 3: ψιxφx → ∃y(y = ιxφ), where ψ is any atomic or identity formula with x free.

Here is an instance of Description Theorem 3, where ψ is the formula Rax and the description ιxGx has been substituted for x in ψ:

RaιxGx → ∃y(y = ιxGx)

Description Theorem 3 is derivable from the Description Axiom.

We can construct a proof using only the premises that PROVER9 used as follows:

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
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 input/output files for this version of the argument is here:

A more complete discussion of the above material can be found in the paper ‘A Computationally-Discovered Simplification of the Ontological Argument’, by Paul E. Oppenheimer and Edward N. Zalta.