op(300,prefix,~). set(auto2). clear(fof_reduction). formulas(sos). % axioms for theorem 21 Point(W). all x (Object(x) -> (Situation(x) <-> (Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) -> (exists p (Proposition(p) & F=VAC(p))))))))). all x (Object(x) -> (Actual(x) <-> (Situation(x) & (all p (Proposition(p) -> (TrueIn(p,x) -> True(p,W))))))). all p all x ((Object(x) & Proposition(p)) -> (TrueIn(p,x) <-> Encp(x,p))). all x all p ((Object(x) & Proposition(p)) -> (Encp(x,p) <-> (exists F (Property(F) & F=VAC(p) & Enc(x,F))))). all p all d all x ((Object(x) & Proposition(p) & Point(d)) -> (Ex1At(VAC(p),x,d) <-> True(p,d))). % denial of theorem 21 -(all x (Object(x) -> ((Situation(x) & Actual(x)) -> (all F (Property(F) -> (Enc(x,F) -> Ex1At(F,x,W))))))). end_of_list.