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.
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.
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(Gu → u=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 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: τ = ι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: ∃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:
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) | x=y)).
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: ∃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: ¬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:
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.
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.
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:
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.