The Clausifications of the Premises

In this document, we list the first-order formulas, in PROVER9 syntax, that we used to represent the logic of the ontological argument in Oppenheimer and Zalta 1991. After each formula, we show clauses into which they are transformed when PROVER9 preprocesses them for its proof search.

The Logical Axioms and Theorems

Description Axiom

 -Relation1(x) | -Relation1(y) | -Object(z) |
    -Is_the(z,x) | -Ex1(y,z) | Object(f1(x,y,z)). 
 -Relation1(x) | -Relation1(y) | -Object(z) |
    -Is_the(z,x) | -Ex1(y,z) | Ex1(x,f1(x,y,z)).
 -Relation1(x) | -Relation1(y) | -Object(z) |
    -Is_the(z,x) | -Ex1(y,z) | -Object(u) | -Ex1(x,u) | f1(x,y,z) = u. 
 -Relation1(x) | -Relation1(y) | -Object(z) |
    -Is_the(z,x) | -Ex1(y,z) | Ex1(y,f1(x,y,z)).
 -Relation1(x) | -Relation1(y) | -Object(z) |
    Is_the(z,x) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). 
 -Relation1(x) | -Relation1(y) | -Object(z) |
    Is_the(z,x) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). 
 -Relation1(x) | -Relation1(y) | -Object(z) | 
    Is_the(z,x) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). 
 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) |
    -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u).
 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) |
    -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). 
 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) |
    -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u).

Description Theorem 1

-Relation1(x) | -Object(y) | -Ex1(x,y) |
    Object(f1(x,y)) | Object(f2(x)).
-Relation1(x) | -Object(y) | -Ex1(x,y) |
    Object(f1(x,y)) | Is_the(f2(x),x).
-Relation1(x) | -Object(y) | -Ex1(x,y) |
    Ex1(x,f1(x,y)) | Object(f2(x)).
-Relation1(x) | -Object(y) | -Ex1(x,y) |
    Ex1(x,f1(x,y)) | Is_the(f2(x),x).
-Relation1(x) | -Object(y) | -Ex1(x,y) |
    f1(x,y) != y | Object(f2(x)).
-Relation1(x) | -Object(y) | -Ex1(x,y) |
    f1(x,y) != y | Is_the(f2(x),x).

Lemma 1

-Object(x) | -Relation1(y) | -Object(z) | 
   -Is_the(x,y) | z != x | Ex1(y,z).

Description Theorem 2

-Relation1(x) | -Object(y) | 
   -Is_the(y,x) | -Object(z) | -Is_the(z,x) | Ex1(x,z).

The Non-Logical Premises, Theorems, and Definitions

Connectedness of Greater Than

-Object(x) | -Object(y) | 
  Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | y = x.

Definition of Nongreater

-Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x).
-Object(x) | -Ex1(none_greater,x) | -Object(y) |
    -Ex2(greater_than,y,x) | -Ex1(conceivable,y).
-Object(x) | Ex1(none_greater,x) |
    -Ex1(conceivable,x) | Object(f1(x)).
-Object(x) | Ex1(none_greater,x) |
    -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x).
-Object(x) | Ex1(none_greater,x) |
    -Ex1(conceivable,x) | Ex1(conceivable,f1(x)).

Premise 1

 
 Object(c1).
 Ex1(none_greater,c1).

Lemma 2

-Object(x) | -Ex1(none_greater,x) | Object(c1).
-Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c1).
-Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | y = c1.

Premise 2

  
-Object(x) | -Is_the(x,none_greater) | Ex1(e,x) |
   Object(f1(x)).
-Object(x) | -Is_the(x,none_greater) | Ex1(e,x) |
   Ex2(greater_than,f1(x),x).
-Object(x) | -Is_the(x,none_greater) | Ex1(e,x) |
   Ex1(conceivable,f1(x)).

Definition of God

Is_the(g,none_greater).