PROVER9's Clausification of the Premises and Conclusion of the Ontological Argument

NOTE: This file contains the clauses of the improved representations discussed at <https://mally.stanford.edu/cm/ontological-argument/>. For the clauses of the representations discussed in Oppenheimer & Zalta 2011, see <https://mally.stanford.edu/cm/ontological-argument/old/clauses.html>.

Definition of none_greater

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

Sorting on none_greater

Relation1(none_greater).

Premise 1

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

Premise 2

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

Lemma 2

-Object(x) | -Ex1(none_greater,x) | Object(c3).
-Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c3).
-Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | Ex2(id,y,c3).

Unique Exemplification Axiom

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

Bridge Principle

-Object(x) | -Object(y) | -Ex2(id,x,y) | y = x.
-Object(x) | -Object(y) | Ex2(id,x,y) | y != x.

Negation of the Conclusion

-Object(x) | -Is_the(x,none_greater) | -Ex1(e,x).