formulas(assumptions). % 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))))). % 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)))))). % Sorting on Is_the all x all F (Is_the(x,F) -> (Relation1(F) & Object(x))). % 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)))))). % Premise 1 exists x (Object(x) & Ex1(none_greater,x)). % 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)))). % 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)))). % Definition of God Is_the(g,none_greater). end_of_list.