Clausification of the Premises for the Ontological Argument (1991): % Description Theorem 1 % 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))))). -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Object(f2(x)). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Is_the(f2(x),x). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Object(f2(x)). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Is_the(f2(x),x). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Object(f2(x)). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Is_the(f2(x),x). [clausify(1)]. % Description Theorem 2: % all F (Relation1(F) -> ((exists y (Object(y) & Is_the(y,F))) -> (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z)))))). -Relation1(x) | -Object(y) | -Is_the(y,x) | -Object(z) | -Is_the(z,x) | Ex1(x,z). [clausify(2)]. % Sorting on Is_the % all x all F (Is_the(x,F) -> (Relation1(F) & Object(x))). -Is_the(x,y) | Relation1(y). [clausify(3)]. -Is_the(x,y) | Object(x). [clausify(3)]. % Def: 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)))))). -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(4)]. -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(4)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f3(x)). [clausify(4)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f3(x),x). [clausify(4)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f3(x)). [clausify(4)]. % Premise 1 % exists x (Object(x) & Ex1(none_greater,x)). Object(c1). [clausify(5)]. Ex1(none_greater,c1). [clausify(5)]. % Lemma 2 % 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)))). -Object(x) | -Ex1(none_greater,x) | Object(c2). [clausify(6)]. -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c2). [clausify(6)]. -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | c2 = y. [clausify(6)]. % Premise 2 % all x (Object(x) -> ((Is_the(x,none_greater) & -Ex1(e,x)) -> exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))). -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f4(x)). [clausify(7)]. -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f4(x),x). [clausify(7)]. -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f4(x)). [clausify(7)]. % Definition of God % Is_the(g,none_greater). Is_the(g,none_greater). [assumption]. % Conclusion: God exists. % Ex1(e,g). -Ex1(e,g). [deny(8)].