A modal epistemic logic for agents is obtained by joining together 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 agents consists of copies of a certain modal logic. Such a system is denoted by the same name as the modal system, but with the subscript , e.g., K is the logic consisting of 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. The following properties are often considered:
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 and S5) 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 is used instead of (D). These two formulae are equivalent in all logics containing , 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 and , are instances of the schema (T). Taking (4) and (5) together with their converses we have and , which allow to reduce multiple knowledge operators to a single (positive or negative) knowledge operator.
The commonly used epistemic logics are specified as follows:
That is, the logics KD, KD4 and KD45 are obtained by substituting the axiom schema (D) for (T) in the axiomatization of T, S4 and S5 respectively.
It is easily verified that the following inference rules are valid for K and its normal extensions: