op(300,prefix,~). set(auto2). clear(fof_reduction). formulas(sos). % axioms for theorem 18 (thanks to Geoff Sutcliffe for isolating % what was necessary, using EP/Vampire to prove this quickly all p all q (Proposition(p)&Proposition(q)-> (VAC(p)=VAC(q)->p=q)). all p (Proposition(p)<->Property(VAC(p))). all y all G all d (Ex1At(G,y,d)->Property(G)&Object(y)&Point(d)). all x all p (Object(x)&Proposition(p)-> (Encp(x,p)<-> (exists F (Property(F)&F=VAC(p)&Enc(x,F))))). all x (Object(x)-> (Situation(x)<->Ex1At(A,x,W)& (all F (Property(F)-> (Enc(x,F)-> (exists p (Proposition(p)&F=VAC(p)))))))). all p all x (Object(x)&Proposition(p)-> (TrueIn(p,x)<->Encp(x,p))). 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)))))))). exists x (Object(x)&Ex1At(A,x,W)& (all F (Property(F)-> (Enc(x,F)<-> (exists p (Proposition(p)&True(p,W)&F=VAC(p))))))). % denial of the theorem 18a -(exists x (World(x)&Actual(x))). end_of_list.