formulas(sos). % Sorting: WorldAt(x,d) all x all d (WorldAt(x,d) -> Object(x) & Point(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 (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 Axiom: W is a Distinguished Point. Point(W). % Definition: PossiblyTrue(p) all p (PossiblyTrue(p) <-> (exists 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. formulas(goals). % Logical Theorem: If there is a world p is true in, p is possibly true. all p (Proposition(p) -> ((exists x (World(x) & TrueIn(p,x))) -> PossiblyTrue(p))). end_of_list.