%------------------------------------------------------------------------------
%----These define the operators
fof(op_possibly,axiom,
    ( op_possibly
   => ! [X] : possibly(X) = not(necessarily(not(X))) )).

fof(op_necessarily,axiom,
    ( op_necessarily
   => ! [X] : necessarily(X) = not(possibly(not(X))) )).

fof(op_implies,axiom,
    ( op_implies
   => ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) )).

fof(op_or,axiom,
    ( op_or
   => ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) )).

fof(op_strict_implies,axiom,
    ( op_strict_implies
   => ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) )).

%fof(op_strict_implies,axiom,
%    ( op_strict_implies
%   => ! [X,Y] : strict_implies(X,Y) = not(possibly(and(X,not(Y)))) )).

fof(op_strict_equiv,axiom,
    ( op_strict_equiv
   => ! [X,Y] : strict_equiv(X,Y) = and(strict_implies(X,Y),strict_implies(Y,X)) )).

fof(all_operators,axiom,
    ( all_operators
   => ( op_possibly
      & op_necessarily
      & op_implies
      & op_or
      & op_strict_implies
      & op_strict_equiv ) )   ).
%------------------------------------------------------------------------------