In this project, we used PROVER9 to implement the
reading of Anselm's ontological argument that 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.

- The Tools You Will Need
- A Computational Implementation of the Ontological Argument
- A Simplification of the Ontological Argument

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:

- June 2007 and later Versions (Unix, Mac, Windows)
- Graphical Version of Prover9 for Mac, Windows and Linux

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 whichzoccurs free, and φ is any formula in whichxis 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 ofGreater 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}abbreviatesCx& ¬∃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 withxfree.

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 reductio2. ∃ y(Gyιxφ_{1}&Cy)from (1), by Premise 2 and MP 3. Ghιxφ_{1}&Chfrom (2), by EE, ‘ h’ arbitrary4. 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!gfrom (8), by definition ‘ g’

The input/output files for this version of the argument is here:

- ontological-simplified.in
- ontological-simplified.out
- ontological-simplified-model.in
- ontological-simplified-model.out

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.