Namespaces
Variants
Actions

Difference between revisions of "Modal logic"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
Line 1: Line 1:
 +
<!--
 +
m0643201.png
 +
$#A+1 = 110 n = 0
 +
$#C+1 = 110 : ~/encyclopedia/old_files/data/M064/M.0604320 Modal logic
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
 +
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
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.
 
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 [[#References|[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|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, [[#References|[6]]]).
 
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 [[#References|[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|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, [[#References|[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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643201.png" /> by the addition of the new one-place connectives (modal operators) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643202.png" /> (necessary) and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643203.png" /> (possible). Since in almost all these systems the relation
+
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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643204.png" /></td> <td valign="top" style="width:5%;text-align:right;">(*)</td></tr></table>
+
$$ \tag{* }
 +
\dia A  \equiv  \neg \square  \neg A
 +
$$
  
holds, initially one modal operator is chosen, for example <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643205.png" />, and the other is defined by (*).
+
holds, initially one modal operator is chosen, for example $  \square $,  
 +
and the other is defined by (*).
  
 
The system S1. Axiom schemes:
 
The system S1. Axiom schemes:
  
1) all formulas of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643206.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643207.png" /> is a formula derivable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643208.png" />;
+
1) all formulas of the form $  \square A $,  
 +
where $  A $
 +
is a formula derivable in $  P $;
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m0643209.png" />;
+
2) $  \square  ( \square A \supset A ) $;
  
3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432010.png" />.
+
3) $  \square  ( \square ( A \supset B )  \&  \square ( B \supset C )  \supset  \square ( A \supset C ) ) $.
  
 
Derivation rules:
 
Derivation rules:
  
I) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432011.png" /> ([[Modus ponens|modus ponens]]);
+
I)
 +
\frac{A  A \supset B }{B}
 +
$([[
 +
Modus ponens|modus ponens]]);
  
II) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432012.png" />;
+
II)
 +
\frac{\square A }{A}
 +
$;
  
III) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432013.png" />.
+
III)
 +
\frac{\square ( A \supset B )  \square ( B \supset A ) }{\square  ( \square A \supset \square B ) }
 +
$.
  
The system S2: S1 + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432014.png" />.
+
The system S2: S1 + $  \{ \square  ( \square A  \supset  \square ( A \lor B ) ) \} $.
  
The system S3: S2 + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432015.png" />.
+
The system S3: S2 + $  \{ \square  ( \square ( A \supset B )  \supset  \square  ( \square A \supset \square B ) ) \} $.
  
 
The system K. Axiom schemes:
 
The system K. Axiom schemes:
  
1) the axiom schemes of the propositional calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432016.png" />;
+
1) the axiom schemes of the propositional calculus $  P $;
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432017.png" />.
+
2) $  \square ( A \supset B )  \supset  ( \square A \supset \square B ) $.
  
 
Derivation rules: modus ponens and
 
Derivation rules: modus ponens and
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432018.png" /></td> </tr></table>
+
$$
  
The system T: K + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432019.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432020.png" /> S2 + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432021.png" />.
+
\frac{A}{\square A }
 +
\ \
 +
( \square \textrm{ - prefix  } ) .
 +
$$
  
The system B: T + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432022.png" />.
+
The system T: K + $  \{ \square A  \supset  A \} $
 +
= $
 +
S2 +  $  \{ \textrm{ rule  of  }  \square \textrm{ \AAh prefix  } \} $.
  
The system S4: S3 + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432023.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432024.png" /> T + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432025.png" />.
+
The system B: T + $  \{ A  \supset  \square \dia A \} $.
  
The system S5: S4 + <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432026.png" />.
+
The system S4: S3 + $  \{ \square  ( \square A  \supset  \square \square A) \} $
 +
= $
 +
T +  $  \{ \square A  \supset  \square \square A \} $.
  
Among the above systems, S4 has important significance since the intuitionistic propositional calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432027.png" /> can be interpreted in it, that is, with respect to every propositional (non-modal) formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432028.png" /> it is possible to construct a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432029.png" /> of modal logic such that
+
The system S5: S4 +  $  \{ \square  ( A  \supset  \square \dia A ) \} $.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432030.png" /></td> </tr></table>
+
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 [[#References|[5]]]):
 
In this connection the system of Grzegorczyk is of particular interest (see [[#References|[5]]]):
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432031.png" /></td> </tr></table>
+
$$
 +
= \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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432032.png" /> and any formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432033.png" />,
+
for it the transference theorem is true: For any set of axiom schemes $  \Gamma $
 +
and any formula $  A $,
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432034.png" /></td> </tr></table>
+
$$
 +
I + \Gamma \vdash A  \iff \
 +
\textrm{ S4 }  +  \Gamma  ^ {*} \vdash A  ^ {*}
 +
\iff  \textrm{ G }  +  \Gamma  ^ {*} \vdash A  ^ {*} ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432035.png" />; 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|intermediate logic]].
+
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|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432036.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432037.png" /> (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:
+
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:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432038.png" /></td> </tr></table>
+
$$
 +
\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)
 
The algebraic interpretation of a system of modal logic is given by some algebra (also called a matrix)
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432039.png" /></td> </tr></table>
+
$$
 +
\mathfrak M  = < M , D ; \&  ^ {*} , \lor  ^ {*} ,\
 +
\supset  ^ {*} , \neg  ^ {*} , \square  ^ {*} > ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432040.png" /> is the set of truth values (cf. [[Truth value|Truth value]]), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432041.png" /> is a set of distinguished truth values, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432042.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432043.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432044.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432045.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432046.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432047.png" /> are the operations in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432048.png" /> corresponding to the connectives <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432049.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432050.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432051.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432052.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432053.png" />. A formula is called generally valid in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432054.png" /> if for every valuation of its propositional variables by elements of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432055.png" /> it takes a distinguished value. A system of modal logic S is called complete relative to a class of algebras <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432056.png" /> if a formula is derivable in S if and only if it is generally valid in every algebra in the class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432057.png" />. For example, the system S4 is complete relative to the class of so-called finite topological Boolean algebras (see [[#References|[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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432058.png" /> is called characteristic or adequate for a system S if S is complete relative to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432059.png" />. 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
+
where $  M $
 +
is the set of truth values (cf. [[Truth value|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 [[#References|[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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432060.png" /></td> </tr></table>
+
$$
 +
\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|Kripke models]], having the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432061.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432062.png" /> is a set (called the set of  "worlds" ,  "situations" ), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432063.png" /> is a relation on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432064.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432065.png" /> is a valuation of the propositional variables by subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432066.png" />. For <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432067.png" /> the relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432068.png" /> can be treated as  "the world t is possible in the world s" . The pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432069.png" /> is called a Kripke structure, or frame (the term scale is also used). A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432070.png" /> is generally valid in the frame <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432071.png" /> if for each valuation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432072.png" /> formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432073.png" /> is true in the Kripke model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432074.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432075.png" />. For example, the system T is Kripke complete relative to the class of structures <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432076.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432077.png" /> 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 [[#References|[7]]]).
+
An important tool in the study of modal logics are [[Kripke models|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 [[#References|[7]]]).
  
For predicate systems of modal logic the Kripke models have the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432078.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432079.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432080.png" /> is a universe for the world <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432081.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432082.png" /> is an interpretation of the predicate symbols in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432083.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432084.png" /> is a valuation associating to object variables some elements of the set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432085.png" />. For systems containing the Barcan formula, it is also necessary to require
+
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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432086.png" /></td> </tr></table>
+
$$
 +
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.
 
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.
Line 83: Line 191:
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  C.I. Lewis,  C.H. Langford,  "Symbolic logic" , Dover, reprint  (1930)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  R. Feys,  "Modal logics" , Gauthier-Villars  (1965)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  E. Rasiowa,  R. Sikorski,  "The mathematics of metamathematics" , Polska Akad. Nauk  (1963)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  A. Grzegorczyk,  "Some relational systems and the corresponding topological spaces"  ''Fund. Math.'' , '''60''' :  2  (1967)  pp. 223–231</TD></TR><TR><TD valign="top">[6]</TD> <TD valign="top">  R.A. Bull,  "A model extension of intuitionist logic"  ''Notre Dame J. Formal Logic'' , '''6'''  (1965)  pp. 142–146</TD></TR><TR><TD valign="top">[7]</TD> <TD valign="top">  K. Fine,  "An incomplete logic containing S4"  ''Theoria'' , '''40''' :  1  (1974)  pp. 23–29</TD></TR><TR><TD valign="top">[8]</TD> <TD valign="top">  D.M. Gabbay,  "Deducability results in non-classical logics I"  ''Ann. Math. Logic'' , '''8''' :  3  (1975)  pp. 237–295</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  C.I. Lewis,  C.H. Langford,  "Symbolic logic" , Dover, reprint  (1930)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  R. Feys,  "Modal logics" , Gauthier-Villars  (1965)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  E. Rasiowa,  R. Sikorski,  "The mathematics of metamathematics" , Polska Akad. Nauk  (1963)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  A. Grzegorczyk,  "Some relational systems and the corresponding topological spaces"  ''Fund. Math.'' , '''60''' :  2  (1967)  pp. 223–231</TD></TR><TR><TD valign="top">[6]</TD> <TD valign="top">  R.A. Bull,  "A model extension of intuitionist logic"  ''Notre Dame J. Formal Logic'' , '''6'''  (1965)  pp. 142–146</TD></TR><TR><TD valign="top">[7]</TD> <TD valign="top">  K. Fine,  "An incomplete logic containing S4"  ''Theoria'' , '''40''' :  1  (1974)  pp. 23–29</TD></TR><TR><TD valign="top">[8]</TD> <TD valign="top">  D.M. Gabbay,  "Deducability results in non-classical logics I"  ''Ann. Math. Logic'' , '''8''' :  3  (1975)  pp. 237–295</TD></TR></table>
 
 
  
 
====Comments====
 
====Comments====
A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432087.png" /> holds at a world <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432088.png" /> if and only if (inductively) either: 1) more precisely,  "being true"  of a formula in a Kripke model is defined as follows: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432089.png" /> is a propositional variable and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432090.png" />; 2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432091.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432092.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432093.png" /> does not hold at <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432094.png" />; 3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432095.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432096.png" /> and at least one of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432097.png" /> holds at <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432098.png" />; or (and this the distinctive clause) 4) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m06432099.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320100.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320101.png" /> holds at each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320102.png" /> for which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320103.png" />.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320104.png" /> on a frame <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320105.png" /> expresses a monadic universal second-order condition on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320106.png" />. (For, propositional variables are related to subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320107.png" />, 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.
+
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., [[#References|[a1]]], [[#References|[a2]]].
 
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., [[#References|[a1]]], [[#References|[a2]]].
  
In provability logic the modal expression <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320108.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320109.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064320/m064320110.png" /> is replaced by the formalized provability predicate of formal (Peano) arithmetic) is a theorem of formal arithmetic; cf. [[#References|[a4]]].
+
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. [[#References|[a4]]].
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  J. van Benthem,  "Modal logic and classical logic" , Bibliopolis  (1983)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  J. van Benthem,  "Correspondence theory"  D. Gabbay (ed.)  F. Guenther (ed.) , ''Handbook of philosophical logic'' , '''II''' , Reidel  (1984)  pp. 167–242</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  R.A. Bull,  K. Segerberg,  "Basic modal logic"  D. Gabbay (ed.)  F. Guenther (ed.) , ''Handbook of philosophical logic'' , '''II''' , Reidel  (1984)  pp. 1–88</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  C. Smorynski,  "Self-reference and modal logic" , Springer  (1985)</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  G.E. Hughes,  M.J. Cresswell,  "An introduction to modal logic" , Methuen  (1968)</TD></TR></table>
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  J. van Benthem,  "Modal logic and classical logic" , Bibliopolis  (1983)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  J. van Benthem,  "Correspondence theory"  D. Gabbay (ed.)  F. Guenther (ed.) , ''Handbook of philosophical logic'' , '''II''' , Reidel  (1984)  pp. 167–242</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  R.A. Bull,  K. Segerberg,  "Basic modal logic"  D. Gabbay (ed.)  F. Guenther (ed.) , ''Handbook of philosophical logic'' , '''II''' , Reidel  (1984)  pp. 1–88</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  C. Smorynski,  "Self-reference and modal logic" , Springer  (1985)</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  G.E. Hughes,  M.J. Cresswell,  "An introduction to modal logic" , Methuen  (1968)</TD></TR></table>

Revision as of 08:01, 6 June 2020


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)
How to Cite This Entry:
Modal logic. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Modal_logic&oldid=12997
This article was adapted from an original article by S.K. Sobolev (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article