Sytax of modal logic

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

The formula $\Box\alpha$ is read: it is necessarily true that $\alpha$. The possibility operator is introduced as an abbreviation: $\diamond\alpha =_{def} \lnot \Box \lnot \alpha$. If $\Gamma\subseteq \mathcal{L}^M$ is a set of formulae then $\Box(\Gamma)$ denotes the set $\{\Box\alpha : \alpha \in \Gamma \}$. We stipulate that the modal operators bind more strongly than the Boolean connectives. Furthermore, we introduce the following abbreviations:

$$\Box^0\alpha =_{def} \alpha$$

$$\Box^{m+1}\alpha =_{def} \Box(\Box^{m}\alpha)$$

for all $m\geq 0$ and $\alpha \in \mathcal{L}^M$.

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 $\alpha$ and $\alpha \to \beta$ to infer $\beta$

(K)

$\Box\alpha \land \Box(\alpha \to \beta) \to \Box\beta$

(T)

$\Box\alpha \to \alpha$

(D)

$\Box\alpha \to \lnot \Box\lnot\alpha$

(4)

$\Box\alpha \to \Box\Box\alpha$

(5)

$\lnot \Box\alpha \to \Box\lnot \Box\alpha$

(N)

$\Box (\alpha \lor \lnot \alpha)$

(C)

$\Box\alpha \land \Box\beta \to \Box(\alpha \land \beta)$

(G)

$\diamond\Box\alpha \to \Box\diamond\alpha$

(NEC)

From $\alpha$ to infer $\Box\alpha$ (Necessitation)

(MON)

From $\alpha \to \beta$ to infer $\Box\alpha \to \Box{\rm }\beta$ (Monotony)

(CGR)

From $\alpha \leftrightarrow \beta$ to infer $\Box\alpha \leftrightarrow \Box\beta$ (Congruence)

(RK$_n$)

From $\avec{\alpha}{\land}{n}\to \beta$ to infer $\avec{\Box\alpha}{\land}{n}\to \Box\beta$, for all $n\in \omega$

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)

$\alpha \to (\beta \to \alpha)$

(PC2)

$(\alpha \to (\beta \to \gamma))\to ((\alpha\to \beta)\to (\alpha\to \gamma))$

(PC3)

$(\lnot \beta \to \lnot \alpha)\to (\alpha\to \beta)$

Let (A) be one of the axiom schemata listed above and $\alpha$ the formula named (A). Then $\Box^{\omega}$(A) denotes the set $\{ \Box^{i}\alpha : i \in \omega \}$. For example, $\Box^{\omega}$(K) is the set $\{ \Box^{i}(\Box\alpha \land \Box(\alpha \to \beta) \to \Box\beta) : i \in \omega \}$.

A modal logic (over the language $\mathcal{L}^M$) 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., $\mathbf{E}\subset \mathbf{M} \subset \mathbf{K}$.

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.