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

%----John says this can be inferred from not_is_idempotent and modus_ponens
%----Is it a rule or an axiom? The neccesarily_hilbert assumes it's an axiom.
fof(modus_tollens,axiom,
    ( modus_tollens
  <=> ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )).

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

fof(implies_2,axiom,
    ( implies_2
  <=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,implies(Y,Z)),implies(implies(X,Y),implies(X,Z)))) )).

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

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

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

fof(or_1,axiom,
    ( or_1
  <=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )).

fof(or_2,axiom,
    ( or_2
  <=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )).

fof(or_3,axiom,
    ( or_3
  <=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )).

fof(equivalence_1,axiom,
    ( equivalence_1
  <=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )).

fof(equivalence_2,axiom,
    ( equivalence_2
  <=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )).

fof(equivalence_3,axiom,
    ( equivalence_3
  <=> ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )).

fof(not_is_idempotent,axiom,
    ( not_is_idempotent
  <=> ! [X] : not(not(X)) = X )).

fof(all_hilbert,axiom,
    ( all_hilbert
   => ( modus_ponens
      & modus_tollens
      & implies_1
      & implies_2
      & and_1
      & and_2
      & and_3
      & or_1
      & or_2
      & or_3
      & equivalence_1
      & equivalence_2
      & equivalence_3
      & not_is_idempotent ) )).

fof(necessarily_modus_tollens,axiom,
    ( necessarily_modus_tollens
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(implies(not(Y),not(X)),implies(X,Y)))) )).

fof(necessarily_implies_1,axiom,
    ( necessarily_implies_1
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(X,implies(Y,X)))) )).

fof(necessarily_implies_2,axiom,
    ( necessarily_implies_2
  <=> ! [X,Y,Z] : is_a_theorem(necessarily(implies(implies(X,implies(Y,Z)),implies(implies(X,Y),implies(X,Z))))) )).

fof(necessarily_and_1,axiom,
    ( necessarily_and_1
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(and(X,Y),X))) )).

fof(necessarily_and_2,axiom,
    ( necessarily_and_2
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(and(X,Y),Y))) )).

fof(necessarily_and_3,axiom,
    ( necessarily_and_3
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(X,implies(Y,and(X,Y))))) )).

fof(necessarily_or_1,axiom,
    ( necessarily_or_1
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(X,or(X,Y)))) )).

fof(necessarily_or_2,axiom,
    ( necessarily_or_2
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(Y,or(X,Y)))) )).

fof(necessarily_or_3,axiom,
    ( necessarily_or_3
  <=> ! [X,Y,Z] : is_a_theorem(necessarily(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))) )).

fof(necessarily_equivalence_1,axiom,
    ( necessarily_equivalence_1
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(equiv(X,Y),implies(X,Y)))) )).

fof(necessarily_equivalence_2,axiom,
    ( necessarily_equivalence_2
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(equiv(X,Y),implies(Y,X)))) )).

fof(necessarily_equivalence_3,axiom,
    ( necessarily_equivalence_3
  <=> ! [X,Y] : is_a_theorem(necessarily(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y))))) )).

fof(neccesarily_hilbert,axiom,
    ( necessarily_hilbert
   => ( necessarily_modus_tollens
      & necessarily_implies_1
      & necessarily_implies_2
      & necessarily_and_1
      & necessarily_and_2
      & necessarily_and_3
      & necessarily_or_1
      & necessarily_or_2
      & necessarily_or_3
      & necessarily_equivalence_1
      & necessarily_equivalence_2
      & necessarily_equivalence_3 ) )).