Modal logic

The domain of logic in which along with the usual statements modal statements are considered, that is, statements of the type "it is necessary that …" , "it is possible that …" , etc. In mathematical logic various formal systems of modal logic have been considered, interrelations between these systems have been revealed, and their interpretations have been studied.

Elements of modal logic were in essence already known to Aristotle (4th century B.C.) and became part of classical philosophy. Modal logic was formalized for the first time by C.I. Lewis [1], who constructed five propositional systems of modal logic, given in the literature the notations S1–S5 (their formulations are given below). Other systems of modal logic were then constructed and investigated. The great variety of systems of modal logic is explained by the fact that the ideas of "possible" and "necessary" can be made precise in various ways; in addition, there are various ways to treat complex modalities (cf. Modality) of the type "necessarily possible" , and "interrelations" of modality with the logical connectives. The majority of systems of modal logic which have been studied are based on classical logic; however, systems based on intuitionistic logic have also been discussed (see, for example, [6]).

Below, several of the most widely-studied propositional systems of modal logic are described. The language of each of these systems is obtained from the language of classical propositional calculus $ P $ by the addition of the new one-place connectives (modal operators) $ \square $( necessary) and $ \dia $( possible). Since in almost all these systems the relation

$$ \tag{* } \dia A \equiv \neg \square \neg A $$

holds, initially one modal operator is chosen, for example $ \square $, and the other is defined by (*).

The system S1. Axiom schemes:

1) all formulas of the form $ \square A $, where $ A $ is a formula derivable in $ P $;

2) $ \square ( \square A \supset A ) $;

3) $ \square ( \square ( A \supset B ) \& \square ( B \supset C ) \supset \square ( A \supset C ) ) $.

Derivation rules:

I) $ \frac{A A \supset B }{B} $([[ Modus ponens|modus ponens]]);

II) $ \frac{\square A }{A} $;

III) $ \frac{\square ( A \supset B ) \square ( B \supset A ) }{\square ( \square A \supset \square B ) } $.

The system S2: S1 + $ \{ \square ( \square A \supset \square ( A \lor B ) ) \} $.

The system S3: S2 + $ \{ \square ( \square ( A \supset B ) \supset \square ( \square A \supset \square B ) ) \} $.

The system K. Axiom schemes:

1) the axiom schemes of the propositional calculus $ P $;

2) $ \square ( A \supset B ) \supset ( \square A \supset \square B ) $.

Derivation rules: modus ponens and

$$ \frac{A}{\square A } \ \ ( \square \textrm{ - prefix } ) . $$

The system T: K + $ \{ \square A \supset A \} $ $ = $ S2 + $ \{ \textrm{ rule of } \square \textrm{ \AAh prefix } \} $.

The system B: T + $ \{ A \supset \square \dia A \} $.

The system S4: S3 + $ \{ \square ( \square A \supset \square \square A) \} $ $ = $ T + $ \{ \square A \supset \square \square A \} $.

The system S5: S4 + $ \{ \square ( A \supset \square \dia A ) \} $.

Among the above systems, S4 has important significance since the intuitionistic propositional calculus $ I $ can be interpreted in it, that is, with respect to every propositional (non-modal) formula $ A $ it is possible to construct a formula $ A ^ {*} $ of modal logic such that

$$ I \vdash A \iff \textrm{ S4 } \vdash A ^ {*} . $$

In this connection the system of Grzegorczyk is of particular interest (see [5]):

$$ G = \textrm{ S4 } + \{ \square ( \square ( \square ( A \supset \square A ) \ \supset A ) \supset A ) \} ; $$

for it the transference theorem is true: For any set of axiom schemes $ \Gamma $ and any formula $ A $,

$$ I + \Gamma \vdash A \iff \ \textrm{ S4 } + \Gamma ^ {*} \vdash A ^ {*} \iff \textrm{ G } + \Gamma ^ {*} \vdash A ^ {*} , $$

where $ \Gamma ^ {*} = \{ {B ^ {*} } : {B \in \Gamma } \} $; moreover, G is the strongest system with this property. This theorem makes it possible to transfer a property (for example, completeness or decidability) from an extension of the system S4 (or G) to an intermediate logic.

For each propositional system of modal logic S it is possible to consider the corresponding predicate system, which is obtained by the addition of object variables, predicate symbols and the quantifiers $ \forall $, $ \exists $( or one of these) to the language of S. The usual axiom schemes and derivation rules for quantifiers are added. In addition one sometimes also adds axioms which describe the actions of modal operators on quantifiers such as, for example, the Barcan formula:

$$ \forall x \square A ( x) \supset \square \forall x A ( x) . $$

The algebraic interpretation of a system of modal logic is given by some algebra (also called a matrix)

$$ \mathfrak M = < M , D ; \& ^ {*} , \lor ^ {*} ,\ \supset ^ {*} , \neg ^ {*} , \square ^ {*} > , $$

where $ M $ is the set of truth values (cf. Truth value), $ D $ is a set of distinguished truth values, $ D \subset M $, and $ \& ^ {*} $, $ \lor ^ {*} $, $ \supset ^ {*} $, $ \neg ^ {*} $, $ \square ^ {*} $ are the operations in $ M $ corresponding to the connectives $ \& $, $ \lor $, $ \supset $, $ \neg $, $ \square $. A formula is called generally valid in $ M $ if for every valuation of its propositional variables by elements of $ M $ it takes a distinguished value. A system of modal logic S is called complete relative to a class of algebras $ {\mathcal K} $ if a formula is derivable in S if and only if it is generally valid in every algebra in the class $ {\mathcal K} $. For example, the system S4 is complete relative to the class of so-called finite topological Boolean algebras (see [3]). In general, a system S is called finitely approximable if it is complete relative to finite algebras. If a system is finitely axiomatizable and finitely approximable, then it is decidable, that is, the problem of recognition of derivability is algorithmically decidable. A matrix $ \mathfrak M $ is called characteristic or adequate for a system S if S is complete relative to $ \{ \mathfrak M \} $. None of the above-mentioned propositional systems of modal logic has a finite adequate matrix, but each of them is finitely approximable and therefore decidable. On the other hand, every extension of S5 has a finite adequate matrix with one distinguished value. The property of finite approximability also holds for all extensions of the system

$$ \textrm{ S4 }.3 = \textrm{ S4 } + \ \{ \square ( \square A \supset \square B ) \lor \square ( \square B \supset \square A ) \} . $$

An important tool in the study of modal logics are Kripke models, having the form $ ( W , R , \theta ) $, where $ W $ is a set (called the set of "worlds" , "situations" ), $ R $ is a relation on $ W $ and $ \theta $ is a valuation of the propositional variables by subsets of $ W $. For $ s, t \in W $ the relation $ s R t $ can be treated as "the world t is possible in the world s" . The pair $ ( W , R ) $ is called a Kripke structure, or frame (the term scale is also used). A formula $ A $ is generally valid in the frame $ ( W, R) $ if for each valuation $ \theta $ formula $ A $ is true in the Kripke model $ ( W , R , \theta ) $. A system S is called Kripke complete relative to a class of Kripke structures if the S-derivable formulas are exactly the formulas which are generally valid in all Kripke structures in the class $ {\mathcal K} $. For example, the system T is Kripke complete relative to the class of structures $ ( W , R ) $, where $ R $ is a reflexive relation; S4 is Kripke complete relative to a structure with a reflexive and transitive relation. Among the finitely-axiomatizable extensions of S4 there are extensions which are not Kripke complete (see [7]).

For predicate systems of modal logic the Kripke models have the form $ ( W , R , D , \psi , \theta ) $, where $ D = \{ D _ {s} \} _ {s \in W } $, $ D _ {s} $ is a universe for the world $ s $, $ \psi $ is an interpretation of the predicate symbols in $ D $, and $ \theta $ is a valuation associating to object variables some elements of the set $ \cup _ {s \in W } D _ {s} $. For systems containing the Barcan formula, it is also necessary to require

$$ s R t \iff D _ {t} \subseteq D _ {s} . $$

Kripke models, as a rule, have a more easily visualized structure than algebraic models; therefore they are often more convenient for the study of different systems of modal logic.

References

[1]	C.I. Lewis, C.H. Langford, "Symbolic logic" , Dover, reprint (1930)
[2]	R. Feys, "Modal logics" , Gauthier-Villars (1965)
[3]	E. Rasiowa, R. Sikorski, "The mathematics of metamathematics" , Polska Akad. Nauk (1963)
[4]	G.A. Mints, "On some calculi of model logic" Proc. Steklov Inst. Math. , 98 (1968) pp. 97–124 Trudy Mat. Inst. Steklov. , 98 (1968) pp. 88–111
[5]	A. Grzegorczyk, "Some relational systems and the corresponding topological spaces" Fund. Math. , 60 : 2 (1967) pp. 223–231
[6]	R.A. Bull, "A model extension of intuitionist logic" Notre Dame J. Formal Logic , 6 (1965) pp. 142–146
[7]	K. Fine, "An incomplete logic containing S4" Theoria , 40 : 1 (1974) pp. 23–29
[8]	D.M. Gabbay, "Deducability results in non-classical logics I" Ann. Math. Logic , 8 : 3 (1975) pp. 237–295

Comments

A formula $ A $ holds at a world $ s \in W $ if and only if (inductively) either: 1) more precisely, "being true" of a formula in a Kripke model is defined as follows: $ A $ is a propositional variable and $ s \in \theta ( A) $; 2) $ A $ is $ \neg B $ and $ B $ does not hold at $ s $; 3) $ A $ is $ B \lor C $ and at least one of $ B , C $ holds at $ s $; or (and this the distinctive clause) 4) $ A $ is $ \square B $ and $ B $ holds at each $ t $ for which $ s R t $.

General validity of a modal formula $ A $ on a frame $ ( W , R ) $ expresses a monadic universal second-order condition on $ ( W , R ) $. (For, propositional variables are related to subsets of $ W $, hence monadic; and in the condition "for each q and s, A holds at s" the part "A holds at s" is first-order expressible — as can be seen immediately from the above definition.) Therefore, modal logic, through its Kripke semantics, can be considered as part of second-order logic.

Questions like: which modal formulas have a first-order equivalent (on a given class of frames)?, and: which (monadic universal) second-order formulas can be modally expressed?, belong to the correspondence theory of modal logic. Cf., e.g., [a1], [a2].

In provability logic the modal expression $ \square A $ is interpreted as "A is provable" . A basic result here is Solovay's completeness theorem, which states that the theorems of Löb's modal logic (the extension of S4 with the scheme $ \square ( \square A \rightarrow A ) \rightarrow \square A $, expressing the generalization of Gödel's second incompleteness theorem known as Löb's theorem) are exactly those modal formulas with the following property: Every arithmetical instance of it (where $ \square $ is replaced by the formalized provability predicate of formal (Peano) arithmetic) is a theorem of formal arithmetic; cf. [a4].

References

[a1]	J. van Benthem, "Modal logic and classical logic" , Bibliopolis (1983)
[a2]	J. van Benthem, "Correspondence theory" D. Gabbay (ed.) F. Guenther (ed.) , Handbook of philosophical logic , II , Reidel (1984) pp. 167–242
[a3]	R.A. Bull, K. Segerberg, "Basic modal logic" D. Gabbay (ed.) F. Guenther (ed.) , Handbook of philosophical logic , II , Reidel (1984) pp. 1–88
[a4]	C. Smorynski, "Self-reference and modal logic" , Springer (1985)
[a5]	G.E. Hughes, M.J. Cresswell, "An introduction to modal logic" , Methuen (1968)