% NOTE: This file doesn't quite match the discussion in Section 3.2 of % Oppenheimer & Zalta 2011. We have improved our representations of % first-order logic formulas and so improved our representation of the % argument. The new representations avoid the problem noted on our % webpage https://mally.stanford.edu/cm/ontological-argument/ . formulas(assumptions). % Definition of Nonegreater all x (Object(x) -> (Ex1(none_greater,x) <-> (Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). % Connectedness of Greater Than all x all y ((Object(x) & Object(y)) -> (Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | Ex2(id,y,x))). end_of_list. formulas(goals). exists x (Object(x) & Ex1(none_greater,x)) -> exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> Ex2(id,y,x))))). end_of_list.