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:

**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.**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**Argument C**: A more faithful representation of**Argument A**in PROVER9, as presented below.**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**.

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

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 τ:

**Connectedness of**: ∀*Greater Than**x*∀*y*(*Gxy*∨*Gyx*∨*x=y*)**Premise 1**: ∃*x*φ_{1}**Premise 2**: ¬*E*!ι*x*φ_{1}→ ∃*y*(*Gy*ι*x*φ_{1}&*Cy*)

The argument also uses the following background logical axioms, theorems, and lemmas:

**Description Axiom**: ψ[ι*x*φ/*z*] ≡ ∃*y*(φ[*y*/*x*] & ∀*u*(φ[*u*/*x*] →*u*=*y*) & ψ[*y*/*z*] ),

where ψ is any atomic formula in which*z*occurs free, and φ is any formula in which*x*is free**Description Theorem 1**: ∃!*x*φ → ∃*y*(*y*= ι*x*φ)**Lemma 1**: τ = ι*x*φ → φ[τ/*x*]**Description Theorem 2**: ∃*y*(*y*= ι*x*φ) → φ[ι*x*φ/*x*]

Finally, we use the following Lemma and Definition, where φ_{1} is *Cx* &
¬∃*y*(*Gyx* & *Cy*)

**Lemma 2**: ∃*x*φ_{1}→ ∃!*x*φ_{1}**Definition**:*g*=_{df}ι*x*φ_{1}

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 Reductio9. E!gfrom (8), by the definition of ‘ g’

It turns out that all we need by way of reasoning in a language without descriptions is to:

- introduce the predication
`Is_the(x,F)`to represent the fact that*x*uniquely exemplifies*F*. - introduce a completely unsorted relation of identity,
`id`, that can be used in exemplfication formulas such as`Ex2(id,x,y)`. - add axioms to govern both the
`Is_the(x,F)`predication and the`id`relation.

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 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) | 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 fornone_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:

- Input file trimmed by using theorems: ontological.in
- PROVER9 proof the theorem: ontological.out
- Mace model of the
premises: ontological-mace.out
- Note that the Mace model is trivial: it collapses model
elements when it is possible to do so. For a
*sane*model, we need to add premises that assert, e.g., that the property of existence is distinct from the property of being conceivable, etc.

- Note that the Mace model is trivial: it collapses model
elements when it is possible to do so. For a
- Input file trimmed by using theorems: ontological.p (in TPTP syntax)

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:

- Master premises input file: master-premises.in
- Master premises input file, in TPTP syntax: master-premises.p
- A model of master-premises.p using PARADOX: master-paradox-model.out.

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

- 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*φ). - 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. - 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 withxfree.

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.