


\documentstyle[10pt]{article}
%\input{cprim}
\hsize=13.5cm
\vsize=18.5cm
\begin{document}
%\begin{verse}
%{\scriptsize Lietuvos matematik\c{u} draugijos mokslo darbai, III tomas, 1999\\
%\copyright MII}
%\end{verse}
%\vspace{5mm}
%\begin{center}
%{\large\bf Some decidable classes of modal logic S5}\\
%\vspace{5mm}
\title{Some decidable classes of modal logic S5}
\author{S.Norg\.{e}la (VU)\\
e-mail: Stasys.Norgela@maf.vu.lt}
%\end{center}
\date{}
\maketitle
\begin{abstract}
We prove the decidability by deducibility of some monadic classes of 
modal logic S5 using the inverse method of S.Yu.Maslov.\\
{\bf Key words}: modal logic S5, decidable classes.
\end{abstract}
\vspace{5mm}
{\bf 1. Introduction}\\
It is know (see, for example [1]) that monadic quantifier 
modal logic S5 is undecidable. We describe
some decidable by deducibility classes of  quantifier modal logic S5 containing
only monadic predicate variables.
In this paper we consider only closed formulas i.e. the formulas without free variables.
Also every atomic formula occurs in the scope of modal connective $\Box$ (or $\Diamond$).
We assume that there are no two bound variables in a formula with
the same name. The formulas $F$ contain only logical connectives $\vee, \wedge, \neg$
and no logical or modal symbol in $F$ lies in the scope of a negation.\\

{\bf Definition 1.} {\it We say the occurence of modal connective $\Box$
 (or $\Diamond$) is the nearest modal
connective for the occurence of atomic formula P if the following conditions holds:}\\
\begin{itemize}
\item {\em the occurence of P belongs to the scope of considerable $\Box$ ($\Diamond$),} 
\item {\em if in the scope of any other occurence of $\Box$ ($\Diamond$)is a considerable
occurence of P, then the nearest modal connective belong also to the same scope of $\Box$ 
($\Diamond$)}\\
\end{itemize}

{\bf Definition 2.} {\it  A sequence $Q_{i}$, $Q_{j}$ ($Q_{i}, Q_{j} \in {\forall, \exists,
 \Box, \Diamond}$) is
called $F$-prefix of the occurence of a atomic formula $G(x)$ in F if $Q_{j}x$
($Q_{j} \in {\forall, \exists}$) belongs to the scope of the nearest modal connective
$Q_{i}$ ($Q_{i} \in {\Box, \Diamond}$) of considerable G(x). Contrary F-prefix
is $Q_{j}, Q_{i}$.}\\

{\bf Definition 3.} {\it A sequence $Q_{i}, Q_{j}$ ($Q_{i}, Q_{j} \in {\forall, \exists,
\Box, \Diamond}$), which is the F-prefix of same atomic formula in F, is called F-prefix
of the formula F}\\

We will consider three decidable classes.\\
The formulas of the first class the following conditions hold:
\begin{enumerate}
\item all occurences of literal containing $x$ (for all variables $x$) belong to
the scope of the same nearest modal connective; the occurences of different variables
belong to different scopes of nearest modal connectives as well, 
\item every $F$-prefix of the formula F ends either with ${\forall, \Box}$ or 
$F$-prefix does not contain $\forall, \Box$.\\  
\end{enumerate}
For example, the following formula belongs to a considerable class:\\

\[ \forall y \Diamond \forall x (P(x) \vee \Box ((P(y) \wedge Q(y)) \vee 
\exists z \Diamond Q(z))\]\\
The next formula does not belong to the first class:\\
\[\forall x \exists y \Diamond (P(x) \wedge Q(y))\]
We will describe two more classes. The second class consists of all formulas which every
$F$-prefix ends either with $\forall$ or $\Box$.\\
For example, the formulas of following forms belong to the second class:
\[ Q_{1}x_{1} \ldots Q_{m}x_{m} \forall y_{1} \ldots \forall y_{s} G \hspace{6mm}
Q \in \{ \Box, \Diamond \}, i=1,...,m\]\\
\[ Q_{1}x_{1} \ldots Q_{m}x_{m} \Box y_{1} \ldots \Box y_{s} G \hspace{6mm}  
Q \in \{ \forall, \exists \}, i=1,...,m\]\\
where $G$ is a formula which does not contain $\Box, \Diamond, \forall, \exists$.\\
Third class. Every formula contains only two occurences of {$\Diamond, \exists$}, or
more precisely, any formula holds one of following conditions:
\begin{enumerate}
\item there are only two occurences of $\Diamond$,
\item there are only two occurences of $\exists$, 
\item there is only one occurence of $\Diamond$ and one occurence of $\exists$.\\
\end{enumerate}
Besides the considerable occurences do not occur in a scope of $\forall$ or $\Box$.\\
\newpage

{\bf 2. Indexing modal logic S5}\\

In this section, we will consider modal logic formulas containing predicate variables
with arity $n$ ($n \geq 1$). In next section we will consider formulas containing
only monadic predicate variables which become two-place predicate variables after 
the transformation into a formula of S5i.\\
We define the formulas of modal logic $S5i$ in the following way:\\
\begin{enumerate}
\item If $P(x_{1},...,x_{n})$ is $n$-place predicate variable, then $P(0, x_{1},...,x_{n})$
is a formula.
\item If {\em F} is a formula, then $\neg F$  is also a formula.
\item If $F, G$ are formulas, then $(F \wedge G)$, $(F \vee G)$, $(F \rightarrow G)$ are
also formulas.
\item If {\em F} is a formula, $x$ is an individual variable, then $\forall x F$ and
$\exists x F$ are also formulas.
\item If $P_{1}(0, x^{1}_{1},..., x^{1}_{n_{1}}), P_{2}(0, x^{2}_{1},..., x^{2}_{n_{2}}),
\ldots, P_{m}(0, x^{m}_{1},..., x^{m}_{n_{m}})$
are any occu\-rences of atomic formulas (we do not require all of the possible occurences
of such formulas) in $F$, then $\Box z F'$ and $\Diamond z F'$ are also formulas.
$F'$ is obtained from $F$ by replacing $P_{k}(0, x^{k}_{1},..., x^{k}_{n_{k}})$ by
$P_{k}(z, x^{k}_{1},..., x^{k}_{n_{k}})$ $(k=1,...,m)$, and $z$ is a new individual
 variable not occuring in $F$.\\
\end {enumerate}
We present modal sequent system $S5i$. We will describe a part of inference rules.
 The following rules $(\vdash \wedge), (\wedge \vdash), (\vdash \rightarrow),
(\rightarrow \vdash), (\vdash \exists), (\exists \vdash), (\vdash \Diamond),
(\Diamond \vdash)$
are described similarly. \\

Axiom scheme \hspace{8mm} $\Gamma_{1}, F, \Gamma_{2} \vdash \Delta_{1}, F, \Delta_{2}$\\

Inference rules:\\

\[(\vdash \neg) \hspace{5mm} \frac{\Gamma_{1}, F, \Gamma_{2} \vdash \Delta_{1}, \Delta_{2}}
{\Gamma_{1}, \Gamma_{2} \vdash \Delta_{1}, \neg F, \Delta_{2}} \hspace{5mm} 
(\neg \vdash) \hspace{5mm} \frac {\Gamma_{1}, \Gamma_{2} \vdash \Delta_{1}, F, \Delta_{2}}
 {\Gamma_{1}, \neg F,  \Gamma_{2} \vdash \Delta_{1}, \Delta_{2}}\]\\

  
\[(\vdash \vee) \hspace{5mm} \frac{\Gamma, \vdash \Delta_{1}, F, G, \Delta_{2}}
{\Gamma  \vdash \Delta_{1}, F \vee G, \Delta_{2}} \hspace{5mm}
 (\vee \vdash) \hspace{5mm} \frac {\Gamma_{1}, F, \Gamma_{2} \vdash \Delta \hspace {3mm}
\Gamma_{1}, G, \Gamma_{2} \vdash \Delta}
 {\Gamma_{1}, F \vee G,  \Gamma_{2} \vdash \Delta}\]\\

 \[(\vdash \forall) \hspace{5mm} \frac{\Gamma \vdash \Delta_{1}, F(y), \Delta_{2}}
{\Gamma \vdash \Delta_{1}, \forall x F(x), \Delta_{2}} \hspace{5mm} 
 (\forall \vdash) \hspace{5mm} \frac {\Gamma_{1}, F(t), \forall x F(x), \Gamma_{2} \vdash \Delta}
 {\Gamma_{1}, \forall x F(x),  \Gamma_{2} \vdash \Delta}\]\\

 \[(\vdash \Box) \hspace{5mm} \frac{\Gamma \vdash \Delta_{1}, F(i), \Delta_{2}}
{\Gamma \vdash \Delta_{1}, \Box x F(x), \Delta_{2}} \hspace{5mm}
(\Box \vdash) \hspace{5mm} \frac {\Gamma_{1}, F(k), \Box x F(x), \Gamma_{2} \vdash \Delta}
 {\Gamma_{1}, \Box x F(x),  \Gamma_{2} \vdash \Delta}\]\\

 $\Gamma, \Gamma_{1}, \Gamma_{2}, \Delta, \Delta_{1}, \Delta_{2}$ are finite sets of formulas.
$F, G$ are formulas. In the rule $(\vdash \forall)$ the variable $y$ has no free
occurences in conclusion of the rule. Term $t$ is free for $x$ in $F(x)$. $i$ is a natural
number not occuring in the conclusion of $(\vdash \Box)$. $k$ is any natural number
(including zero).\\

{\bf Theorem 1.} {\it For any formula F of modal logic one can construct F' of S5i such
that $\vdash F$ is derivable in indexing system S5 iff $\vdash F'$ is derivable in S5i.}\\

For any formula $F$, we construct $F'$ in following way. Any occurence of a atomic
formula $P(x_{1},...,x_{n})$ not occuring in a scope of modal connective $\Box (\Diamond)$
is replaced by $P(0,x_{1},...,x_{n})$. Suppose that $P_{1}(x^{1}_{1},...,x^{1}_{n_{1}}),...,
P_{m}(x^{m}_{1},...,x^{m}_{n_{m}})$ is a complete sequence of atomic formulas which
 nearest modal connective is occurence of $\Box (\Diamond)$. We replace $P_{i}(x^{i}_{1},...,
x^{i}_{n_{i}})$ $(i=1,...,m)$ by $P_{i}(0,x^{i}_{1},...,x^{i}_{n})$ and considerable
occurence of $\Box (\Diamond)$ is replaced by $\Box z (\Diamond z)$ (where $z$ is a new
variable). If all such sequences are replaced, then we delete all occurences of
$\Box (\Diamond)$ without variables.\\

For example.\\
\[F: \hspace{5mm} \forall x \Box \Box (P(x) \wedge \Diamond \exists y Q(y))\]\\
\[F': \hspace{5mm} \forall x \Box z (P(z,x) \wedge \Diamond u \exists y Q(u,y))\]\\

One shows that for any formula $F$ of modal logic one can construct the
deductive equivalent sequent which
is derivable in $K_{1}S5$ ([2]) iff $\vdash F'$ is derivable in $S5i$.\\

{\bf Definition 4.} {\it A equivalent formula for F of the form $Q_{1}x_{1}Q_{2}x_{2}...Q_{n}x_{n}G$
(where $Q_{j} \in \{ \exists, \forall, \Box, \Diamond \}$ and G is quantifier-free formula
not occuring $\Box, \Diamond$) is called generalized prenex normal form of F.}\\

{\bf Theorem 2} {\it For any formula of S5i there exists deductive equivalent generalized
prenex normal form}\\

\vspace{5mm}
{\bf 3. Decidable classes}\\

{\bf Theorem 3.} {\it For any formula F of the first class there exists deductive equivalent
formula F' of the generalized prenex normal form\\ $F'=Q_{1}x_{1}...Q_{m}x_{m}G$ which
belongs to first class as well and the following condition holds:\\
for any literal in G there exists such j $(j=1,2,...,m-1)$ that $x_{j}=y$ and
$x_{j+1}=z$ (or $x_{j}=z, x_{j+1}=y$).}\\

{\bf Theorem 4.} {\it Assume we have a derivation of sequent $\vdash F$ (F belongs to the
first class) and in deduction tree the literal $P([i/x], [a/y])$ is meeted. Then we
can construct deduction tree in which does be not the literals of the form
$Q(i,b)$ (i.e. the literals with $b \neq a$) or $R(j,a)$ (i.e. the literals with
$j \neq i$)}.\\

{\bf Theorem 5} {\it The first class is decidable by deducibility.}\\

{\em The second class.} Class is decidable because the class of the formulas of the
classical predicate logic without function symbols and equality containing only the 
formulas which all $F$- prefixes end with $\forall$ belongs to class {\bf K} [3].
{\bf K} is decidable [3].\\

{\em The third class.} For any formula of the third class one can construct a equivalent
formula $F'$ occuring in $S5i$ of the following generalized prenex normal form\\
\[Q_{1}x Q_{2}yQ_{3}z_{1}Q_{4}z_{2}...Q_{n+2}z_{n}G\\
Q_{1}, Q_{2} \in \{ \exists, \Diamond \}, \hspace{5mm} Q_{i} \in \{ \forall, \Box \}
\hspace{3mm} (i=3,4,...,n+2)\]\\

where $G$ is a formula does not contain occurences of $\forall, \exists, \Box,
\Diamond$.\\
Class is decidable because any $F$-prefix the following conditions holds:\\
\begin{itemize}
\item it ends with $\Box$ or $\forall$.
\item it is one of the following forms $\exists \exists, \exists \Diamond, 
\Diamond \exists, \Diamond \Diamond$; also the considerable occurences of $\exists,
\Diamond$ not occur in the scope of a occurence of $\forall$ or $\Box$.\\
\end{itemize} 
Such formulas (after the replacing $\Box$ by $\forall$ and $\Diamond$ by $\exists$)
occur in decidable class {\bf K} as well.\\
\newpage 
\begin{center}
{\bf REFERENCES}
\end{center}
\vspace{5mm}
1.S.A.Kripke, The undecidability of monadic quantification theory, {\em Zeitschrift
f\"{u}r mathematische Logik und Grundlagen der Mathematik}, 8, 113-116 (1962).\\
2.R.Pliu\v{s}kevi\v{c}ius, On the conservative exsitension of quantifier modal
logic S5.- {\em Mathematical logic and its applications}, Vilnius, 4, 25-38 (1985).\\
3.S.Yu.Maslov, The inverse method of establiching deducibility for logical calculi,
{\em Proceedings of the Steklov Institute of Mathematics}, 98, 25-96 (1971).\\

{\bf Kai kurios i\v{s}sprend\v{z}iamos modalin\.{e}s logikos S5 klas\.{e}s}\\
\begin{center}
{\em S.Norg\.{e}la}\\
\end{center}

Naudojantis Maslovo atvirk\v{s}tiniu metodu \c{i}rodomas kai kuri\c{u} modalin\.{e}s\\
logikos S5 klasi\c{u} su vienvie\v{c}iais predikatiniais kintamaisiais i\v{s}sprend\v{z}iamumas
pagal i\v{s}vedim\c{a}. 
\end{document}

