Definitions for Propositional Modal Logics

Formulae in propositional modal logics are built from primitive propositions, classical connectives, the unary modal connectives $\Box$ and $\Diamond$, and parentheses, in a usual way.

DefinitionKripke frame is a triple $\langle W, \tau, R\rangle$, where W is a nonempty set (of possible worlds), $\tau \in W$ is the actual world, and R is a binary relation on W, called the accessibility relation. A (propositional) Kripke model is a tuple $\langle W, \tau, R, h\rangle$, where $\langle W, \tau, R\rangle$ is a Kripke frame, and h is a mapping from worlds to sets of primitive propositions; that is, h(w) is the set of primitive propositions which are ``true'' at the world w.

The satisfiability relation is defined in a usual way (see Definition 2.1.4).

The simplest normal (propositional) modal logic (called K) is axiomatized by the standard axioms for the classical propositional logic and the modus ponens inference rule together with the axiom schema $\Box(\phi \to \psi) \to (\Box \phi \to \Box \psi)$, which is usually called the K-axiom, plus the additional necessitation rule

$$\frac{\vdash \phi}{\vdash \Box \phi}$$

It can be shown that a modal logic formula is provable in this axiomatization iff it is satisfied in every Kripke model (i.e. without any special R-properties) [9]. It is known that certain axiom schemata added to this axiomatization correspond to certain properties of the accessibility relation.

Many of such correspondences are definable as formulae of first-order logic where the binary predicate R(x,y) represents the accessibility relation, as shown in Table . Different modal logics are distinguished by their respective additional axiom schemata. Some of the most popular modal logics together with their axiom schemata are listed in Table . We refer to properties of the accessibility relation of a modal logic L as L-frame axioms or L-frame restrictions. A Kripke frame is called L-frame if its accessibility relation satisfies all L-frame restrictions.

We call a Kripke model M a L-model if the accessibility relation of M satisfies all L-frame restrictions. We say that $\phi$ is L-satisfiable if there exists a L-model of $\phi$.

We call modal logics which are characterized by classes of Kripke models normal modal logics. Given two normal modal logics L and ${{\textit{L}\textrm{}}'}$, we say that ${{\textit{L}\textrm{}}'}$ is a normal extension of L if all L-frame restrictions are also ${{\textit{L}\textrm{}}'}$-frame restrictions.

We say that two sets X and Y of formulae are equisatisfiable in a logic L if (X is L-satisfiable iff Y is L-satisfiable).

 

Table: Axioms and corresponding first-order conditions on R

Axiom	Schemata	First-Order Formula
D	$\Box \Phi \to \Diamond\Phi$	$\forall w\ \exists{{w}'}\ R(w,{{w}'})$
T	$\Box \Phi \to \Phi$	$\forall w\ R(w,w)$
B	$\Phi \to \Box\Diamond\Phi$	$\forall w,{{w}'}\ R(w,{{w}'}) \to R({{w}'},w)$
4	$\Box \Phi \to \Box\Box \Phi$	$\forall w,u,v\ R(w,u) \land R(u,v) \to R(w,v)$
5	$\Diamond\Phi \to \Box\Diamond\Phi$	$\forall w,u,v\ R(w,u) \land R(w,v) \to R(u,v)$

 

 

Table: Modal logics and frame restriction

Logic	Axioms	Frame Restriction
K	K	no restriction
KD	KD	serial
T	KT	reflexive
KB	KB	symmetric
KDB	KDB	serial and symmetric
B	KTB	reflexive and symmetric
K4	K4	transitive
KD4	KD4	serial and transitive
S4	KT4	reflexive and transitive
K5	K5	euclidean
KD5	KD5	serial and euclidean
K45	K45	transitive and euclidean
KD45	KD45	serial, transitive and euclidean
KB5	KB5	symmetric and euclidean
S5	KT5	reflexive and euclidean