The language of propositional modal logic is formed by extending that of the propositional calculus by an one-place modal operator . Formally:

The formula is read: it is necessarily true that . The possibility operator is introduced as an abbreviation: . If is a set of formulae then denotes the set . We stipulate that the modal operators bind more strongly than the Boolean connectives. Furthermore, we introduce the following abbreviations:

for all and .

All the modal systems we consider are formed by adding to a complete axiomatization of the propositional calculus some specific modal axiom schemata and rules of inference. We shall consider some modal logics determined by axioms and rules from the following lists:

**(PC)**- All propositional tautologies
**(MP)**- Modus ponens: from and to infer
**(K)****(T)****(D)****(4)****(5)****(N)****(C)****(G)****(NEC)**- From to infer (Necessitation)
**(MON)**- From to infer (Monotony)
**(CGR)**- From to infer (Congruence)
**(RK)**- From to infer , for all

Instead of using **(PC)** for defining a logic to include all
tautologies, it would suffice to include a set of schemata from which
all tautologies can be derived by appropriate rules of inference,
e.g., modus ponens. An example of such a set of schemata is:

**(PC1)**-
**(PC2)**-
**(PC3)**-

Let **(A)** be one of the axiom schemata listed above and
the formula named **(A)**. Then
**(A)** denotes the set
. For example, **(K)** is the set
.

A modal logic (over the language ) is called classical
if it is closed under the rule of congruence **(CGR)**. The
minimal classical logic, which is axiomatized by **(PC)**,
**(MP)**, and **(CGR)**, is denoted **E**. A modal
system is called monotonic if it is closed under the monotony rule
**(MON)**. The minimal monotonic logic, which is axiomatized by
**(PC)**, **(MP)**, and **(MON)**, is called
**M**. A modal logic is called normal if it contains the schema
**(K)** and is closed under the rule of necessitation
**(NEC)**. Some equivalent axiomatizations of the
minimal normal modal logic **K** are given in the following.

The last of the above axiomatizations is less common than the
other. It is however of interest for epistemic logic because none of
the inference rules **(NEC)**, **(MON)**, and **(CGR)**
is required.

It is easy to see that every monotonic logic is also classical, and
every normal logic is also monotonic logic and classical. In
particular, one can show that **E** is a proper subsystem of
**M**, and **M** is in turn a proper subsystem of
**K**, i.e.,
.

Additional normal (monotonic, classical) systems of modal logic can be
formed by adding axioms to the basic systems **K** (**M**,
**E**). The new systems are often named by appending the names of
the additional modal axioms used to the name of the basic system,
e.g., **EK** is the logic **E** together with the axiom
**K**; the logic **EK** together with the axiom **4**
is called **EK4**; and **KD45** is the logic **K**
together with the axioms **(D)**, **(4)**, and
**(5)**. Some modal logics are better known under their
historical names, in particular, **KT4** is known as **S4**,
**KT4G** as **S4.2**, and **KT45** as **S5**.