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)$.

Moreover, L is closed under:

• Substitution;
• Detachment rule: from A and A→B infer B;
• Necessitation rule: from A infer $\Box A$.

The modal logic with just the above features is called K. Normal modal logic, a proper extension of the propositional calculus, includes most modal logics commonly used nowadays, including C. I. Lewis's S4 and S5.