%------------------------------------------------------------------------------
% File     : LCL007+0 : TPTP v7.2.0. Released v3.3.0.
% Domain   : Logic Calculi (Propositional modal)
% Axioms   : Propositional modal logic rules and axioms
% Version  : [She06] axioms.
% English  :

% Refs     : [Hal]   Halleck (URL), John Halleck's Logic Systems
%          : [She06] Shen (2006), Automated Proofs of Equivalence of Modal
% Source   : [She06]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :   23 (   0 unit)
%            Number of atoms       :   52 (   1 equality)
%            Maximal formula depth :    6 (   4 average)
%            Number of connectives :   29 (   0 ~  ;   0  |;   2  &)
%                                         (  23 <=>;   4 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :   25 (  23 propositional; 0-2 arity)
%            Number of functors    :    7 (   0 constant; 1-2 arity)
%            Number of variables   :   39 (   0 singleton;  39 !;   0 ?)
%            Maximal term depth    :    5 (   3 average)
% SPC      : 

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

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(adjunction,axiom,
    ( adjunction
  <=> ! [X,Y] :
        ( ( is_a_theorem(X)
          & is_a_theorem(Y) )
       => is_a_theorem(and(X,Y)) ) )).

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

%----"Standard" modal axioms
fof(axiom_K,axiom,
    ( axiom_K
  <=> ! [X,Y] : is_a_theorem(implies(necessarily(implies(X,Y)),implies(necessarily(X),necessarily(Y))))  )).

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

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

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

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

%----Axioms for Lewis systems
fof(axiom_s1,axiom,
    ( axiom_s1
  <=> ! [X,Y,Z] : is_a_theorem(implies(and(necessarily(implies(X,Y)),necessarily(implies(Y,Z))),necessarily(implies(X,Z)))) )).

fof(axiom_s2,axiom,
    ( axiom_s2
  <=> ! [P,Q] : is_a_theorem(strict_implies(possibly(and(P,Q)),and(possibly(P),possibly(Q))))  )).

fof(axiom_s3,axiom,
    ( axiom_s3
  <=> ! [X,Y] : is_a_theorem(strict_implies(strict_implies(X,Y),strict_implies(not(possibly(Y)),not(possibly(X)))))  )).

fof(axiom_s4,axiom,
    ( axiom_s4
  <=> ! [X] : is_a_theorem(strict_implies(necessarily(X),necessarily(necessarily(X))))   )).

%----Axioms for S1-0
fof(axiom_m1,axiom,
    ( axiom_m1
  <=> ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),and(Y,X))) )).

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

fof(axiom_m3,axiom,
    ( axiom_m3
  <=> ! [X,Y,Z] : is_a_theorem(strict_implies(and(and(X,Y),Z),and(X,and(Y,Z)))) )).

fof(axiom_m4,axiom,
    ( axiom_m4
  <=> ! [X] : is_a_theorem(strict_implies(X,and(X,X))) )).

fof(axiom_m5,axiom,
    ( axiom_m5
  <=> ! [X,Y,Z] : is_a_theorem(strict_implies(and(strict_implies(X,Y),strict_implies(Y,Z)),strict_implies(X,Z))) )).

%----Axioms for building from S1-0
fof(axiom_m6,axiom,
    ( axiom_m6
  <=> ! [X] : is_a_theorem(strict_implies(X,possibly(X)))  )).

fof(axiom_m7,axiom,
    ( axiom_m7
  <=> ! [P,Q] : is_a_theorem(strict_implies(possibly(and(P,Q)),P))  )).

fof(axiom_m8,axiom,
    ( axiom_m8
  <=> ! [P,Q] : is_a_theorem(strict_implies(strict_implies(P,Q),strict_implies(possibly(P),possibly(Q)))) )).

fof(axiom_m9,axiom,
    ( axiom_m9
  <=> ! [X] : is_a_theorem(strict_implies(possibly(possibly(X)),possibly(X)))  )).

fof(axiom_m10,axiom,
    ( axiom_m10
  <=> ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X)))) )).

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