In this project, we used PROVER9 to implement the reading of Anselm's ontological argument that we developed in our paper of 1991 (Oppenheimer and Zalta 1991). Our paper offered a reading of the argument in Anselm's Proslogion II. Here is the Jonathan Barnes Translation of Anselm's Proslogion II.
NOTE: The files below all work correctly with the June 2007 version of PROVER9. They may also work with later versions, but they were all checked with the June 2007 version. You can download a compressed archive of this version by following one of these links:
You will need to expand the Unix/Mac archive and compile the program yourself; the Windows version comes only as a binary, without sources.
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.
• The 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 (object(x) & relation1(G) & relation2(R) ->
((is_the(x,G) & exemplifies2(R,a,x)) <->
exists y (object(y) & exemplifies1(G,y) &
all u (ex1(G,u) -> u=y) & exemplifies2(R,a,y))))
• The Connectedness of the GreaterThan Relation: ∀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)) -> (exemplifies2(greaterthan,x,y) | exemplifies2(greaterthan,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 nonegreater to represent the open formula "x is conceivable and such that nothing greater than x is conceivable", as follows:
all x (object(x) -> (exemplifies1(nonegreater,x) <->
(exemplifies1(conceivable,x) &
-(exists y (object(y) & exemplifies2(greaterthan,y,x) &
exemplifies1(conceivable,y)))))).
With this definition, we may represent Premise 1 in PROVER9 as follows:
Note here how our definition of the property nonegreater is the counterpart in PROVER9 to the abbrevation φ1 that we used in object theory.exists x (object(x) & exemplifies1(nonegreater,x)).
• 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 nonegreater, 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,nonegreater) & -exemplifies1(e,x)) ->
exists y (object(y) & exemplifies2(greaterthan,y,x) &
exemplifies1(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.
Here is a list of the theorems we have proved, leading to the ontological argument itself, along with the input and output files for both the theorem and the model of the premises.
• 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 object 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 x (object(x) & exemplifies1(F,x) &
(all y (object(y) ->(exemplifies1(F,y) -> y=x))))) ->
(exists x (object(x) & is_the(x,F))))).
This tells us that for every property F, if there is an object x that (a) exemplifies F and (b) is such that anything y that exemplifies F is identical to it, then there is an object x which is the F. Here are the input and output files for both the theorem and the model of the premises:
• 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) -> exemplifies1(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 x (object(x) & is_the(x,F))) ->
(all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y)))))).
This asserts, for any property F, that if something x is the F, then anything y that is the F exemplifies F. Here are the input and output files for both the theorem and the model of the premises:
• Lemma 2: ∃xφ1 → ∃!xφ1
This lemma tells us that if there is something such that nothing greater can be conceived, then there is a unique thing such that nothing greater can be conceived. 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) & exemplifies1(nonegreater,x)) ->
exists x (object(x) & exemplifies1(nonegreater,x) &
(all y (object(y) -> (exemplifies1(nonegreater,y) -> y=x)))).
This tells us that if some object x exemplifies the nonegreater property, then a unique object x does. Here are the input and output files for both the theorem and the model of the premises:
In object theory, the conclusion of the ontological argument is the claim "E!g", where g is defined as:
g = ιxφ1
To introduce the constant "g" ("God") into our PROVER9 representations we use the following:
is_the(g,nonegreater).
Given the Premise 1, Premise 2, the definition of nonegreater, 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: