set(auto2). clear(fof_reduction). 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)). % denial of theorem 24b -(all p (Proposition(p) -> ((all x (World(x) -> TrueIn(p,x))) -> NecessarilyTrue(p)))). end_of_list.