set(auto2).
clear(fof_reduction).

formulas(sos).
% axioms for theorem 23
Point(W).

all p (Proposition(p)<->Property(VAC(p))).

all F all x (Property(F)&Object(x)<->Proposition(PLUG(F,x))).

all p all d all x (Object(x)&Proposition(p)&Point(d)-> (Ex1At(VAC(p),x,d)<->True(p,d))).

all x all F all d (Object(x)&Property(F)&Point(d)-> (True(PLUG(F,x),d)<->Ex1At(F,x,d))).

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

World(ALPHA)&Actual(ALPHA)& (all x (Actual(x)&World(x)->x=ALPHA)).

all p (Proposition(p)-> (TrueIn(p,ALPHA)<->Ex1At(VAC(p),ALPHA,W))).

% denial of theorem 23
-(all p (Proposition(p)-> (True(p,W)<->TrueIn(PLUG(VAC(p),ALPHA),ALPHA)))).
end_of_list.

