set(auto2). clear(fof_reduction). formulas(sos). % Logical Axiom: If being-such-that-p = being-such-that-q, then p=q all p all q (Proposition(p)&Proposition(q)-> (VAC(p)=VAC(q)->p=q)). % Logical Axiom: p is a proposition iff VAC(p) is a property. all p (Proposition(p)<->Property(VAC(p))). % Definition: SituationAt(x,d) all x all d (Object(x)&Point(d)-> (SituationAt(x,d)<->Ex1At(A,x,d)& (all F (Property(F)-> (EncAt(x,F,d)-> (exists p (Proposition(p)&F=VAC(p)))))))). % 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)))))). % 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)))))))). % Definition: EncpAt(x,p,d) all x all p all d (Object(x)&Proposition(p)&Point(d)-> (EncpAt(x,p,d)<-> (exists F (Property(F)&F=VAC(p)&EncAt(x,F,d))))). % Definition: TrueInAt(p,x,d) all p all x all d (Object(x)&Proposition(p)&Point(d)-> (TrueInAt(p,x,d)<->EncpAt(x,p,d))). % Proper Axiom: Necessary Existence of an Object that Encodes all and only the Truths all d (Point(d)-> (exists x (Object(x)&Ex1At(A,x,d)& (all F (Property(F)-> (EncAt(x,F,d)<-> (exists p (Proposition(p)&True(p,d)&F=VAC(p))))))))). % denial of L4 -(all d (Point(d)-> (exists x (WorldAt(x,d)&ActualAt(x,d))))). end_of_list.