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: