op(300,prefix,~).
set(auto2).
clear(fof_reduction).

formulas(sos).

% Definition: ActualAt(x,d)
all x all d (Object(x) & Point(d) -> (ActualAt(x,d) <-> SituationAt(x,d) & (all p (Proposition(p) -> (TrueInAt(p,x,d) ->True(p,d)))))).

% Logical Axiom: ~p is a proposition if p is.
all p (Proposition(p) -> Proposition(~p)).

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

% Definition: WorldAt(x,d)
all x all d (Object(x) & Point(d) -> (WorldAt(x,d) <-> SituationAt(x,d) & (exists d2 (Point(d2) & (all p (Proposition(p) -> (TrueInAt(p,x,d2) <-> True(p,d2)))))))).

% Logical Theorem (L1): WorldAt(x,d) is rigid.
all x (Object(x) -> ((exists d (Point(d) & WorldAt(x,d))) -> (all d (Point(d) -> WorldAt(x,d))))).

% Logical Theorem (L2): EncpAt(x,p,d) is rigid.
all x all p ((Object(x) & Proposition(p)) -> ((exists d (Point(d) & EncpAt(x,p,d))) -> (all d (Point(d) -> EncpAt(x,p,d))))).

all p all x all d ((Object(x) & Proposition(p) & Point(d)) -> (TrueInAt(p,x,d) <-> EncpAt(x,p,d))).

% denial of 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))))))).
end_of_list.

