%------------------------------------------------------------------------------
fof(necessitation,axiom,
    ( necessitation
  <=> ! [X] : 
        ( is_a_theorem(X)
       => is_a_theorem(necessarily(X)) ) )).

fof(adjunction,axiom,
    ( adjunction
  <=> ! [X,Y] : 
        ( ( is_a_theorem(X)
          & is_a_theorem(Y) )
       => is_a_theorem(and(X,Y)) ) )).

fof(modus_ponens_strict_implies,axiom,
    ( modus_ponens_strict_implies
  <=> ! [X,Y] : 
        ( ( is_a_theorem(X)
          & is_a_theorem(strict_implies(X,Y)) )
       => is_a_theorem(Y) ) )).

fof(substitution_strict_equiv,axiom,
    ( substitution_strict_equiv
  <=> ! [X,Y] : 
        ( is_a_theorem(strict_equiv(X,Y))
       => X = Y ) )).

%------------------------------------------------------------------------------