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))))))))).

end_of_list.

