formulas(assumptions). %------------------------------ % Premises used in the theorems %------------------------------ % Connectedness of Greater Than all x all y ((Object(x) & Object(y)) -> (Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | Ex2(id,x,y))). % Definition of None_greater % 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)))))). % Sorting on none_greater Relation1(none_greater). % Premise 1 exists x (Object(x) & Ex1(none_greater,x)). % Premise 2 (- (exists x(Object(x) & Is_the(x,none_greater) & Ex1(e,x)))) -> (all x ((Object(x) & Is_the(x, none_greater)) -> exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))). % 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) -> Ex2(id,y,x))))). % Unique Exemplification Axiom all x all F ((Object(x) & Relation1(F)) -> (Is_the(x,F) <-> (Ex1(F,x) & (all z ((Object(z) & Ex1(F,z)) -> Ex2(id,x,z)))))). % Bridge Principle all x all y ((Object(x) & Object(y)) -> (Ex2(id,x,y) <-> x=y)). % Sorting on Ex2 all R all x all y (Ex2(R,x,y) -> (Relation2(R) & Object(x) & Object(y))). % ---------------------------------- % Premises Needed for a Sane Model % ---------------------------------- % Sorting on Is_the all x all F (Is_the(x,F) -> (Relation1(F) & Object(x))). % Sorting on greater_than Relation2(greater_than). % Sorting on conceivable Relation1(conceivable). % id is a relation Relation2(id). % e is a property Relation1(e). % greater_than is a relation Relation2(greater_than). % Non-identity of existence and none_greater e != none_greater. % Non-identity of id and greater_than id != greater_than. % Non-identity of conceivable and none_greater. conceivable != none_greater. % Non-identity of conceivable and e. conceivable != e. % Sorting Principles: all x (Object(x) -> -Relation1(x)). all x (Object(x) -> -Relation2(x)). all x (Relation1(x) -> -Relation2(x)). all F all x (Ex1(F,x) -> (Relation1(F) & Object(x))). end_of_list.