op(300,prefix,~). formulas(sos). % axioms for theorem 20 Point(W). all p (Proposition(p)->Proposition(~p)). all d all p (Point(d)&Proposition(p)-> (True(~p,d)<-> -True(p,d))). all x (Object(x)-> (Actual(x)<->Situation(x)& (all p (Proposition(p)-> (TrueIn(p,x)->True(p,W)))))). 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)). World(ALPHA)&Actual(ALPHA)& (all x (Actual(x)&World(x)->x=ALPHA)). end_of_list.