formulas(sos).

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

% Logical Theorem  (Lemma 1): 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 (Corollary to Lemma 2): TrueInAt(p,x,d) is rigid.
all x all p ((Object(x) & Proposition(p)) -> ((exists d (Point(d) & TrueInAt(p,x,d))) -> (all d (Point(d) -> TrueInAt(p,x,d))))).

% Logical Theorem (Lemma 3): If x is an ActualWorld At d, then p is TrueIn x At d iff p is True wrt d
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)))))).

% Proper Theorem (Lemma 4): An Actual World Exists at Every Point.
all d (Point(d) -> (exists x (WorldAt(x,d) & ActualAt(x,d)))).

% Logical Axiom: W is a Distinguished Point.
Point(W).

% Definition: NecessarilyTrue(p)
all p (NecessarilyTrue(p) <-> (all d (Point(d) -> True(p,d)))).

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

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

end_of_list.



