Axioms for modal epistemic logic

A modal epistemic logic for $N$ agents is obtained by joining together $N$ modal logics, one for each agent. For simplicity's sake it is usually assumed that the agents are homogeneous, i.e., they can be described by the same logic. So an epistemic logic for $N$ agents consists of $N$ copies of a certain modal logic. Such a system is denoted by the same name as the modal system, but with the subscript $N$, e.g., K$_N$ is the logic consisting of $N$ copies of the logic K.

Stronger logics can be obtained by adding additional principles, which express the desirable properties of the concept of knowledge, to the basic system K$_N$. The following properties are often considered:

(T)

$K_i\alpha \to \alpha$

(D)

$K_i\alpha \to \lnot K_i \lnot\alpha$

(4)

$K_i\alpha \to K_iK_i\alpha$

(5)

$\lnot K_i\alpha \to K_i\lnot K_i\alpha$

The formula (T) states that knowledge must be true. One normally takes this property to be the major one distinguishing knowledge from belief: you can have false beliefs, but you cannot know something that is not true. For that reason (T) is sometimes called the Knowledge Axiom or the Truth Axiom (for knowledge). Systems containing the schema (T) (such as S4$_N$ and S5$_N$) are then called logics of knowledge, and logics without the schema (T) are called logics of belief.^2.2

The property (D), occasionally called the Consistency Axiom, requires that agents be consistent in their knowledge: they do not know both a formula and its negation. Often the formula $\lnot K_i(\alpha \land \lnot\alpha)$ is used instead of (D). These two formulae are equivalent in all logics containing $K_i\alpha \land K_i\beta \leftrightarrow K_i(\alpha \land \beta)$, in particular in all normal modal systems. Generally, (D) is a weaker condition than (T).

The properties (4) and (5) are called positive and negative introspection axioms, respectively. They say that an agent is aware of what he knows and what he does not know. Their converses, i.e., the formulae $K_iK_i\alpha \to K_i\alpha$ and $K_i\lnot K_i\alpha \to \lnot K_i\alpha$, are instances of the schema (T). Taking (4) and (5) together with their converses we have $K_iK_i\alpha \leftrightarrow K_i\alpha$ and $K_i\lnot K_i\alpha \leftrightarrow \lnot K_i\alpha$, which allow to reduce multiple knowledge operators to a single (positive or negative) knowledge operator.

The commonly used epistemic logics are specified as follows:

• T$_N$ is K$_N$ plus (T)
• S4$_N$ is T$_N$ plus (4)
• S5$_N$ is S4$_N$ plus (5)
• KD$_N$ is K$_N$ plus (D)
• KD4$_N$ is KD$_N$ plus (4)
• KD45$_N$ is KD4$_N$ plus (5)

That is, the logics KD$_N$, KD4$_N$ and KD45$_N$ are obtained by substituting the axiom schema (D) for (T) in the axiomatization of T$_N$, S4$_N$ and S5$_N$ respectively.

It is easily verified that the following inference rules are valid for K$_N$ and its normal extensions:

(NEC)

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

(MON)

From $\alpha \to \beta$ to infer $K_i\alpha \to K_i\beta$ (Monotony)

(CGR)

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

(RK$_n$)

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