Normal modal logic

In logic, normal modal logic is a set L of modal formulas such that L contains

• all propositional tautologies,
• Kripke's schema: $\Box (A\to B)\to (\Box A\to \Box B)$,

and L is closed under

• substitution,
• detachment rule: from A and A→B infer B,
• necessitation rule: from A infer $\Box A$.

The minimal normal modal logic is known as K.