set(auto2).
clear(fof_reduction).

formulas(sos).

% Sorting on WorldAt
all x all d (WorldAt(x,d) -> Object(x) & Point(d)).

% L1
all x (Object(x) -> ((exists d (Point(d) & WorldAt(x,d))) -> (all d (Point(d) -> WorldAt(x,d))))).

% Corollary to L2
all x all p ((Object(x) & Proposition(p)) -> ((exists d (Point(d) & TrueInAt(p,x,d))) -> (all d (Point(d) -> TrueInAt(p,x,d))))).

% L3
all x all d ((Object(x) & Point(d)) -> ((WorldAt(x,d) & ActualAt(x,d)) -> (all p (Proposition(p) -> (TrueInAt(p,x,d) <-> True(p,d)))))).

% L4 
all d (Point(d) -> (exists x (WorldAt(x,d) & ActualAt(x,d)))).

% Distinguished Point.
Point(W).

% Definition of PossiblyTrue
all p (PossiblyTrue(p) <-> (exists d (Point(d) & True(p,d)))).

% Definition of World(x).
all x (World(x) <-> WorldAt(x,W)).

% Definition of TrueIn
all x all p (TrueIn(p,x) <-> TrueInAt(p,x,W)).


% denial of 25a
-(all p (Proposition(p) -> (PossiblyTrue(p) -> (exists x (World(x) & TrueIn(p,x)))))).
end_of_list.


