op(300,prefix,~).

formulas(sos).
% axioms for theorem 17b
all p (Proposition(p)->Proposition(~p)).

all d all p (Point(d)&Proposition(p)-> (True(~p,d)<-> -True(p,d))).

all x (Object(x)-> (World(x)<->Situation(x)& (exists y (Point(y)& (all p (Proposition(p)-> (TrueIn(p,x)<->True(p,y)))))))).

all x (World(x)->Object(x)).

all x (Object(x)-> (Consistent(x)<->Situation(x)& -(exists p (Proposition(p)&TrueIn(p,x)&TrueIn(~p,x))))).
end_of_list.

