



\documentclass{article}
\usepackage{amssymb,amsmath,latexsym}
%\usepackage{amssymb,amsmath,latex}

\date{}

\author{Vladimir V.~Rybakov\\
\it
 Institute of Mathematics and Computer Science, \\
Siberian Federal University, Krasnoyarsk; \\
and Institute of Informatics Systems Ac. Sci., Novosibirsk\\
Vladimir\_Rybakov@mail.ru  }



{\medskip}
\newcommand{\ii}[0]
{\rightarrow}

\newcommand{\ri}[0]
{\mbox{$\Rightarrow$}}

\newcommand{\lri}[0]
{\mbox{$\Leftrightarrow$}}

\newcommand{\lr}[0]
{\mbox{$\Longleftrightarrow$}}

\newcommand{\ppp}{\varphi}


\newcommand{\vv}[0]{
\unitlength=1mm \linethickness{0.5pt} \protect{
\begin{picture}(4.40,4.00)
\put(1.2,-0.4){\line(0,1){3.1}} \put(2.1,-0.4){\line(0,1){3.1}}
\put(2.1,1.1){\line(1,0){2.0}}
\end{picture}\hspace*{0.3mm}}}


\newcommand{\nv}[0]{
\unitlength=1mm \linethickness{0.5pt} \protect{
\begin{picture}(4.40,4.00) \put(1.2,-0.4){\line(0,1){3.1}}
\put(2.1,-0.4){\line(0,1){3.1}} \put(2.1,1.1){\line(1,0){2.0}}
\protect{ \put(0.3,-0.7){\line(1,1){3.6}}}
\end{picture}\hspace*{0.3mm}
} }



\begin{document}



\title{ Multi-agent Logics  with  Frozen States, Admissibility via Projectivity
}



\maketitle


Subject Classification:  510.64,510.65,510.66

\bigskip

{\Large \bf  Abstract}.  \ \
 \footnote{This work was supported by the Russian Science Foundation and Krasnoyarsk Regional Fund of Science (Project No 25-21-20011,  https://rscf.ru/en/project/25-21-20011/).
  }

\medskip

In this paper we study
 multi-agent temporal logics whose models allow frozen states if information nodes (information states).
Models for these logics are similar to standard ones for
multi-modal temporal logics, but  the current time clusters may posses
states with broken connections of information channels. Such look at models (as we feel)
  stays close to real world situation with networks of agents' information.  In order to solve open problems of decidability in such logics and recognizing admissible rules we
 use some elements of unification and projective formulas techniques and find positive solution of these problems.









\bigskip

 {\large Key words: } {\sl temporal logics,
 multi-agent logics, information, knowledge,
 deciding algorithms
}





\section{\bf Introduction}


Multi-agent  logics and their combination with modal logics made active research area in AI  and social sciences.
E.g. the book [1] suggests approach used multi-dimensional Kripke models
\(M = \langle W, R_1, \dots, R_n , V \rangle,\) where $W$ models some amount of states and   $R_j$ represents
  agents' accessibility relations between states. Then the
modal-like formula ${K_i}A$ is interpreted as -- the agent $i$ knows the information ((or the knowledge) described by formula $A$. That approach may be extended by usage instead the formula $K_i A$ a more informative ones, which means that the agent is simply informed (a formula
 $A_i(x)$ illustrates that {\it the agent
 $i$ knows (may know) information  $x$}.
That ideas were developed  in
 Rybakov [2], in particular, there we find algorithm for decidability such logics, several
   applications been suggested. To nowadays many works in application non-standard logic to AI and
   computation logical information appeared in press (cf.
   for instance [3, 4, 5, 6, 7, 8]).



In this our  paper we develop some new logical techniques in order to solve open problems for the case
of multi-agent logics whose models allow frozen states if information nodes (information states).
The models look as standard multi-modal temporal logics, but  the current time clusters may posses
states with broken connection of information channels.
 All accessibility relations of agents' - relations $R_j$ --  in each time cluster $C(i)$ defined separately
 and independently. This approach corresponds close to real world situation with networks of agents' information.  In order to solve open problems of decidability in such logics and recognizing admissible rules we
 use some elements of unification and projective formulas techniques. That not only allows to essentially short proofs but also helps to solve affirmatively the problems.




\section{\bf Short recall on projective formulas}

We start by short recall known technique which we will use longer. Basic knowledge in non-classical logic is assumed. We need to report basics of unification.
For a set of propositional letters  $P$ a substitution
 is a mapping $\varepsilon$  of $P$ into set of all formulas
$For$; any such substitution may be  extended to set of all formulas
by
 $\varepsilon
(\ppp(x_1, \dots , x_n)) := \ppp(\varepsilon(x_1), \dots ,
\varepsilon(x_n))$.
 A formula is said to be unifiable in a logic $L$ if there is a substitution
$\varepsilon$ (which is said to be an unifier for $\ppp$) such that $
\varepsilon(\ppp) \in L$.

%Now we recall the basic definition of our paper:

\medskip

{\bf Definition 2.1.} {\it
A unifier  $\varepsilon$ for a formula  $\ppp$ in a logic $L$ is said to be more general then a unifier
  $\varepsilon_1$  if there is a substitution
$\delta$ such that for any letter $x$, $[\varepsilon_1(x) \equiv
\delta(\varepsilon(x))] \in L$. }

\medskip



%\begin{definition} \label{lu1} {\em
%A substitution $ \varepsilon$ is a unifier for a formula $\ppp$ in $\llll$ if
%$\varepsilon(\ppp) \in \llll$.  A formula $\ppp$ is unifiable in
%$\llll$ if it has a unifier. A unifier $\varepsilon$ is more general
%than a unifier $\varepsilon_1$ iff there is a substitution $\delta$
%such that for any letter $x$, $\varepsilon_1(x) = \delta(\varepsilon
%(x))$.}
%\end{definition}


%Since the logic $\llll$ is decidable, to check unifiability a formula
%in $\llll$, is the reasonably easy task: it is sufficient to use only
%ground substitutions: mappings of variables in the set $\{\bot,
%\top\}$.

In usual, if a logic $L$ is decidable, to verify unifiability of a formula is an easy task
(in theoretical means, since  complexity of computation may be very high)
: actually it is sufficient to verify only substitution of letters from the set $\{\bot, \top\}$ instead propositional letters - variables.
At the same time, the question of finding all unifiers is not simple.



\medskip

{\bf Definition 2.2.} {\it A set of unifiers
 $CU$ for a formula $\ppp$ in a logic $L$ is complete set of unifiers
  if the following holds.
 For any unifier
$\sigma$ of $\ppp$ in $L$, there is a unifier $\sigma_1$ from $CU$, such that  $\sigma_1$ is more general then
$\sigma$.}

\medskip



For modal logics, for example  extending modal logic
$S4$,  the definition of  projective formulas  is as follows:


\medskip

{\bf Definition 2.3.} {\it
 A formula $\ppp$ is projective in a logic
 $L$ if the following holds. There exists a substitution
 $\sigma$ (which is called projective substitution for
 formula $\ppp$) such that $\sigma$  is a unifier for $\ppp$  in  $L$    and
  $\Box \ppp \ii [ x_i \equiv \sigma (x_i)] \in L$ for any propositional letter  $x_i$ from $\ppp$.}



\medskip

{\bf Lemma 2.4.} {\it If
 a substitution $\sigma_p$ is projective for
   $\ppp$  in  $L$, then $\{\sigma_p\}$ is a complete set of unifiers for  $\ppp$ (that is $\sigma_p $ is more
   general unifier).}

\medskip

Proof. Assume that   $\sigma$ is some unifier for $\ppp$ in  $L$.
Since  $\sigma_p$ is projective for  $\ppp$ in $L$, we get
$\Box \ppp \ii [x_i \equiv \sigma_p(x_i)] \in L$ for any letter $x_i$ from $\ppp$. Applying $\sigma$ to formulas above
we get
$\sigma(\Box \ppp) \ii [\sigma(x_i) \equiv \sigma (\sigma_p (x_i))] \in L $,
that is $\sigma(x_i) \equiv \sigma (\sigma_p (x_i)) \in L $. Q.E.D.


\medskip



It is easy to see that, if for a decidable modal logic
$L$, we can verify if a formula $\ppp$ is projective and can compute its projective unifier,
then {\bf  admissibility problem in logic $L$ is decidable}.
 Indeed, recall {\it the definition.} An inference rule
 $\ppp_1, \dots \ppp_n /  \psi$ is admissible in  $L$  iff for any  unifier $\epsilon$ for
 $\ppp_1 \wedge  \dots \wedge \ppp_n$ this  $\epsilon$ is also a unifier for
   $\psi $.

  To show decidability of the admissibility problem then, admit that an inference rule
 $\ppp_1, \dots \ppp_n /  \psi$ is admissible in  $L$, Admit that there is a unifier for
 $\ppp_1, \dots \ppp_n$.  Then by our assumption above we may compute
its projective unifier and it is enough just to verify if this  projective unifier (which is then most general unifier) is a unifier for
$ \psi$, and the problem is solved.
     This fruitful idea was found by Silvio Ghilardi [9,10].
 In this our paper we will apply elements of this technique below.




\section{Decidability by Projectivity}

All definitions an facts recalled above are true (and applicable) to our logic introduced below.
 As we noted above, applications of projective technique was found  by Silvio Ghilardi [9,10] and later on it was applied to the linear modal logics in
works of  Wojciech Dzik and  Piotr Wojtylak for modal logics extending S.4.3 cf. [11].
Recently we used similar technique  for multi-modal logics
  studying transfer information and its' reliability (cf. [12]).
 We start now by definition of semantics for our logic  - Kripke-like frames of our logic.

\
\medskip

  {\bf Definition 3.1. }  {\it Frames
  \(   F := \langle \bigcup_{i \in N}  C(i), \leq, Prev, R_j, j \in J \rangle \) are structures where
 $C(i), i \in N$ are infinite sequence of not-intersecting sets $\ C(i)$ of states, which may be thought as  clusters of time.}

\medskip

The definitions of operations used in the one above are explained below.
Here, each $R_j$ is a binary reflexive and transitive accessibility relation on each $C(i)$, -- the agents' accessibility relations (if $ a R_j b$ there is $C(i)$ where $a,b \in C(i)$). The binary relation
$\leq$ is the linear-like order of time: For all $a,b \in  \bigcup_{i \in N}  C(i)$, $ a\leq b$ iff $a\in C(i)$  for some  $C(i)$ and
$b \in C(i_1)$, where $ i \leq i_1$. $Prev $ is the binary relation introduced to distinguish the previous time cluster, its definition is as follows:
$\forall a,b \in \in  \bigcup_{i \in N}  C(i)$, $a Prev  b \ \lri \  b \in C(i+1), a \in C(i)$ or $a = b$ (the latter one is very important to our research technique would work).

A model $M$ for our logic to be obtained from a frame $F$ by choice a valuation $V$  a set of propositional letters in states of the frame.  A valuation $V$ of a set of propositional letters (variables) $P$ in $F$ is a mapping $V$ of $P$ in the set of all subsets of $\bigcup_{i \in N}  C(i)$, so
$\forall p \in P,  V(p) \subseteq \bigcup_{i \in N}  C(i)$.   We  write for $ a  \in F$ that   $a \vv_V p$  \ iff \  $  a \in V(P)$, and we say then that $p$ is true at $a$ w.r.t. $V$.

The language of our temporal multi-agent logic consists of propositional letters, usual Boolean logical operations,
 temporal-modal operations $\Box$ and $\Diamond$, and agents' operations $\Box_i,\Diamond_j, j \in J$ and  the previous-time unary operation $\Diamond_{Prev}$. Rules for constructions of formulas by these operations are standard.


For any Kripke model
 $M$,
 the truth values can
be extended from propositions letters $P$ to arbitrary formulas
constructed from these propositions as follows:

\smallskip

$ \forall p\in Prop \ (M,a)\vv_V p \ \lri  a\in \bigcup_{i \in N}  C(i) \wedge \ a\in V(p);$

\smallskip

$ (M,a)\vv_V (\ppp\wedge \psi) \ \lri
(M,a)\vv_V \ppp \ \wedge \
(M,a)\vv_V \psi;$

\smallskip


$ (M,a)\vv_V (\ppp\vee \psi) \ \lri
(M,a)\vv_V \ppp \ \vee \
(M,a)\vv_V \psi;$


\smallskip

$ (M,a)\vv_V \neg \ppp \ \lri not [(M,a)\vv_V \ppp]  ;$

$ (M,a)\vv_V \Diamond \ppp \ \lri \exists b
[(a \leq b) \& (M,b)\vv_V \ppp]  ;$

\smallskip


$ (M,a)\vv_V \Box \ppp \ \lri \forall b
[(a \leq b) \ri (M,b)\vv_V \ppp]  ;$

\smallskip


$ (M,a)\vv_V \Diamond_j \ppp \ \lri \exists b
[(a R_j b) \& (M,b)\vv_V \ppp]  ;$

\smallskip


$ (M,a)\vv_V \Box_j \ppp \ \lri \forall b
[(a R_j b) \ri (M,b)\vv_V \ppp]  ;$

\medskip


%$ (M,a)\vv_V \Box_{Prev} \ppp \ \lri \forall b
%[(b Prev a) \ri (M,b)\vv_V \ppp]  ;$


$ (M,a)\vv_V \Diamond_{Prev} \ppp \ \lri \exists b
[(b Prev a) \& (M,b)\vv_V \ppp]  ;$

\smallskip


\medskip
\medskip


 { For a Kripke model $M:= \langle F, V \rangle$ and a formula $\ppp$ with letters from the domain of $V$,
 $\ppp$ is true in $M$ (denotation -- $M\vv \ppp$) if, \ for any
state $b$ from $F$,
 the formula $\ppp$ is true at $b$ (that is: $(M,b)\vv_V
\ppp)$. For a frame $F:=\langle W, R \rangle$, we say that a formula $\ppp$ is true at $F$,
(and we will write $F \vv \ppp$) if $\ppp$ is true at any model based at $F$. }


\medskip

Let $P_n :=\{ p_1, \dots, p_n\} $  be a fixed set of propositional letters.
Let  $Pos_n$ be a non-empty set of some subsets  $Y_n$  of $P_n$. Let
\( \psi(Y_n):= [\bigwedge_{p_j \in Y_n} p_j \wedge \bigwedge_{p_j \not\in Y_n} \neg p_j ]\).
We   now    impose some additional requirement on the structure of all models $M$ of our logic in order to express all possible situations for agents accessibility relations.

  \medskip


 {\bf Definition 3.2. } {\it  We   say that a model $M$ has frozen states w.r.t. $P_n$ if for any $C(i)$ there is some
 unique set $P_n[C(i)]$ of some sets $Pos_n $ each of which consists of letters from $P_n$ with following properties. For any
   $Y_n\in Pos_n$   there are some states $ a_{Y_n} \in C(i)$ such that
   $(a_{Y_n} \Vdash_V [\psi(Y_n) \wedge \bigwedge_j \Box_j \psi(Y_m)])$.
        Besides, for all subsets $Y_m$ of
 $P_n :=\{ p_1, \dots, p_n\} $
 not occurring in the set $P_n[C(i)]$,
  $\forall b \in C(i) (b \nVdash_V [\psi(Y_m) \wedge \bigwedge_j \Box_j \psi(Y_m)])$.}







     \medskip

     So, states $a_{Y_n}$ have frozen agents' accessibility relations $R_J$, so to say broken  information channels.
      All accessibility relations of agents' - relations $R_j$ --  in each time cluster $C(i)$ defined separately
 and independently. This approach corresponds close to real world situation with networks of agents' information.

\medskip



Our logic $L$ is {\it the set of all formulas $\ppp(p_1, \dots, p_n)$ which are true at
any state of any model $M$  with frozen sets w.r.t. $P_n$  and any given valuation}.

\medskip

Recall that a formula $\ppp(p_1, \dots, p_n)$ is said to be unifiable in a logic $L$ if there is a substitution $ \varepsilon(x_i) := \beta_i$ arbitrary formulas $\beta_i$ instead of propositional letters $x_i$   such that $\ppp(\beta_1, \dots,  \beta_n) \in L$.


\bigskip

Possible case for choice of our models for the logic $L$ is the model $M_0$  when  for all $i$ $C(i) = \{a_{0,i}\}$ and when the valuation is $V_0(p_k) = \{a_{0,i} \mid 0,i\}$ for all $p_k$.  That is for all $a_{0,i}$, $a_{0,i} \vv_{V_0} p_k$ for all $k$.


 \medskip

{\bf Lemma 3.3.} {\it There is an algorithm, which for any formula $\ppp(p_1, \dots, p_n)$, constructed out of letters $p_1, \dots, p_n$,  verifies if this formula is
unifiable in $L$ and if yes constructs  a substitution for letters $p_1, \dots, p_n$ which replaces $ p_j$ on  $ y_j$ which is a unifier for $\ppp(p_1, \dots p_n)$ in $L$ and any $y_j$ is either $\top$ or $\bot$. We will denote in the sequel  $\epsilon(p_j):= y_j$.}

\medskip


Proof. If a formula $\ppp(p_1, \dots, p_n)$ is unifiable in $L$ then there is a substitution $p_j  \ri \psi_j$, such that the formula
$\ppp(\psi_1, \dots, \psi_n)$ is true by any valuation $V$ at any state of any model for $L$ with some frozen
sets w.r.t all propositional letters from $\ppp(\psi_1, \dots, \psi_n)$.
In particular this holds at the model $M_o$ w.r.t. $Pos_n = \{P_n\}$ and $P_n$ to be the set of
 all propositional letters from $\ppp(\psi_1, \dots, \psi_n)$, $M_o\Vdash \ppp(\psi_1, \dots, \psi_n)$.

  Then the formula $\ppp(\epsilon(p_1), \dots, \epsilon(p_n))$ is true in the one element model w.r.t. any  valuation
  $V_1$ when w.r.t. $V_1$  truth value of any letter $p_j$ is $\epsilon(p_j)$ where $ \epsilon(p_j) = \top $ or  $\epsilon(p_j) = \bot$ w.r.t. how $\psi_j$ was true in $M_o$ at any state.

   For some substitutions $\epsilon_1(p_j) \in \{\top, \bot\}$, if the formula
  $\ppp(\epsilon_1(p_1), \dots, \epsilon_1(p_n)$ is true in the one element model it is easy to calculate.
  If we found a such substitution, then
  the formula $\ppp(\epsilon_1(p_1), \dots,\epsilon_1(p_n)$ is true in any model with frozen sets, so  $\ppp$ is unifiable. Q.E.D.


\medskip



 {\bf Theorem 3.4.} { \it  Any unifiable formula $\ppp$ is projective in  $L$. There is an algorithm verifying unifiability in $L$ and constructing a projective unifier for $\ppp$ if $\ppp$ is unifiable (so, then
 the admissibility of inference rules in $L$ is decidable).
 }

\bigskip

Proof. Given a formula $\ppp(p_1, \dots, p_n)$ constructed out of propositional letters $p_i$.
By {\bf Lemma 3.3.} we verify if this formula is unifiable in $L$ and if yes construct a shown in this Lemma unifier
$\epsilon(p_j):= y_j$.
 We now will try to prove that this formula  is projective.



    Let  $Var(\Box \varphi)$ be the set $\{p_1, \dots, p_n\}$ of all propositional letters from  $\Box \varphi$
    (so in other notation, $Var(\Box \varphi) = P_n$.
  To fix notation, let now
 $SV$ be the set of all subsets of the set $Var(\Box \varphi)$.

  Let for any $SV_p\subseteq SV $,  $ASV_p$ be a fixed set from $SV_p$. Else let
   for $p_k \in Var(\Box \varphi)$,  $tv(SV_p,p_k) = \top$ if
 $p_k \in ASV_p$ and $tv(SV_p,p_k) = \bot$ otherwise.


 We introduce now our substitution.
 The structure of this substitution (as well as understanding of its value and actions) is crucial for the rest of the proof below; the expressed by this substitution properties are important via joining all of them together and cannot be commented separately. For any
 letter $p_i$ from $P_n$, let

\[\sigma(p_i) := [(\Box \varphi)\wedge p_i ] \vee
[\neg \Diamond \Box  \varphi  \wedge \epsilon(p_i)]  \vee
 [\neg \Box \varphi \wedge \Diamond \Box  \varphi \wedge \]
 \[
\big( \bigvee _{SV_P  \subseteq  SV} \ [\bigwedge_{A \in SV_P } \big(
[   \bigwedge_{Y_n \in A} [\Diamond [  \Box \ppp \wedge \Diamond_{Prev} \neg \Box \ppp \wedge
\psi(Y_n) ]  \wedge  \]
\[ \Box [\Box
\ppp \wedge \Diamond_{Prev} \neg \Box \ppp \wedge [\psi(Y_n) \ii \bigwedge_{j \in J} \Box_j \psi(Y_n) ]]\big) \wedge tv(SV_p,p_i) \big) \wedge \]


\[ \bigwedge_{Y_r \subseteq P_n, Y_r \not\in SV_p} \neg \Diamond [  \Box \ppp \wedge \Diamond_{Prev} \neg \Box \ppp \wedge
\psi(Y_r) \wedge
  \bigwedge_j \Box_j \psi(Y_r)]] \big), \]



Now we will prove that this substitution is  a projective unifier for
 $\varphi$ in logic  $L$. Choose any model $M = \langle F, V \rangle$ of our logic
with a frame
$F$ and given valuation of the set  of all letters $P_n$ from $\varphi$, which is frozen w.r.t. $P_n$.
 Take any state  $a \in F$.

Consider first the case when
  $(F,a) \Vdash_V \neg \Diamond \Box \varphi $.
By our definition of the unifier $\sigma(p_i)$ and Lemma 3.3. we have $ \sigma(p_i)$ is equivalent to $ \epsilon(p_i)$,
where $ \epsilon(p_i) =  y_i$, and then $\sigma$
it is a unifier for formula
 $\varphi$ in our logic. So,

\[ \ \forall b \in F, \ (F,b) \Vdash_V \sigma(\varphi)).\]


Let now  $(F,a) \Vdash_V  \Box \varphi $. Then the substitution  $\sigma$ does not change  truth values of letters $p_i$ in $a$ and all $b$, where $a \leq b$,
comparing with their original truth values w.r.t. $V$. Therefore




\[ (F,a) \Vdash_V  p_i \  \lri \ (F,a) \Vdash_V  \sigma(p_i), \ \forall b \geq a  \
(F,b) \Vdash_V  p_i \  \lri \ (F,b) \Vdash_V  \sigma(p_i). \]


This implies

\[ (F,a)  \Vdash_V  \sigma(\Box \varphi).\]

It remains only to consider the case when


\[ (F,a)  \Vdash_V \neg \Box \varphi \wedge \Diamond \Box  \varphi .\]

Then let we look close to our model.
The model $M$ is based at $F$ is a model with frozen states w.r.t. $P_n$,
then  by definition of frozen, for any $C(i)$ there is a
 unique set $P_n[C(i)]$ of some sets $Pos_n $ of letters from  $Var(\Box \varphi)$ with all required properties.

Let  $C(i)$ be the lowest cluster where the formula  $\Box  \varphi$  is true w.r.t. the original valuation $V$.
Then for $SV_p = P_n[C(i)]$ the disjunct member of the definition of $\sigma(p_i)$ above is true at
all states $ b $ situated strictly below $C(i)$. And for $SV_p$ distinct from $P_n[C(i)]$ this is not the case for any
such $b$.


 Then the truth value of all $\sigma(p_i)$ at all such $b$ is exactly the same as the truth value of $p_i$ w.r.t. the original frame valuation $V$ in a state
 $a_{Y_k} $ from $C(i)$  where $(a_{Y_k} \Vdash_V \psi(Y_k))$ where $Y_k \in ASV_p$ (and, recall, $ASV_p \in SV_p =
 P_n[C(i)]$.



\bigskip


{\bf Lemma 3.5.} {\it Truth value of any formula $\sigma(\alpha)$,
 where $\alpha$ is  a formula constructed out of letters $p_1, \dots , p_n$, by Boolean operations and operations $\Diamond_j$,  at the states $b$ situated strictly below $C(i)$ w.r.t. $V$ is the same as the truth of this formula at $a_{Y_k}$ w.r.t.  $V$}.


\medskip

Proof. Here it is sufficient to use standard  induction by the length of formula, for Boolean logical operation it is evident. For modal operations it is again trivial because we consider in this lemma truth of  formulas strictly below $C(i)$.

\medskip


\bigskip


{\bf Lemma  3.6. } {\it Truth value of any formula $\sigma(\alpha)$, where $\alpha$ is  a formula constructed out of letters $p_1, \dots , p_n$, by Boolean operations and operations $\Diamond_j$,
  $\Diamond$ and $\Diamond_{Prev}$
at the states $b$ situated strictly below $C(i) $ w.r.t. $V$
 is the same as truth value of $\sigma(\alpha)$ at $a_{Y_k}$ w.r.t.  $V$.}

\smallskip

 Proof. Again, as in the lemma above we use standard induction by the length of formula, and for more used modal operation it is again directly follows from the case that by condition of this current lemma states $b$ situated strictly below $C(i) $ w.r.t. $V$.

\medskip

So, $\sigma$ is a unifier for $\ppp$ and it is evident that $\sigma$  is projective for $\ppp$
(that is $\Box \ppp \ii [ x_i \equiv \sigma (x_i)] \in L$ ).
 Theorem is proved.



\bigskip



%Literature

\begin{thebibliography}{9}

%\begin{thebibliography}{90}

\bibitem{faa2} {\it Ronald Fagin, Joseph Y. Halpern, Yoram Moses and Moshe Vardi}
(Reasoning About Knowledge, MIT, 1995).



\bibitem{rraa2z} {\it  V. V. Rybakov. } {\it Refined common knowledge logics or logics of common information.-
 Archive for mathematical Logic, 42 (2), 2003, 179 -- 200.}




\bibitem{ar2}
  {\it S. Artemov} {Explicit Generic-Common Knowledge}, Lect.  Notes in CS,  LFCS 2013: Logical Foundations of Computer Science 2013, pp 16–28.

\bibitem{ar3}  {\it S. Artemov}
{ Justification awareness. --
} Journal of Logic and Computation 30 (8), 2020, 1431 -- 1446.

\bibitem{ry2}
{\it  V Rybakov Temporal Multi-Agent’s Logic, Knowledge, Uncertainty, and Plausibility}. --
Agents and Multi-Agent Systems: Technologies and Applications, LNCS, 2021,  2005 -  2014.




\bibitem{ba2}
Baader F., Kusters R. {\em Unification in a description logic with transitive closure of roles.} In: Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2001. Vol. 2250. LNCS, Springer (2001),  217 -- 232.





\bibitem{vr11y}
Rybakov V.V.,
{\em Multiagent temporal logics with multivaluations},
Siberian. Math. J.,
59,
no 4, (2018),
710 -– 720.


\bibitem{08ñ}
 Rybakov V. V. {\em Projective formulas and unification in linear temporal logic LTLU},
Logic Journal of the IGPL, Oxford Press. --  22 (4), (2014), 665 -- 672.

\bibitem{r10}
Ghilardi S. {\em Unification Through Projectivity,} -- J. of Logic and Computation, Oxford Press, 7(6) (1997),
733 -- 752.


\bibitem{g1}
Ghilardi S. {\em  Unification, finite duality and projectivity in
varieties of Heyting algebras,}  -- Annals of Pure and Applied Logic, 127(1-3),
(2004),  99 -- 115.



\bibitem{dz} Dzik W., Wojtylak P. {\em Projective unification in modal logic.} -- Logic Journal of IGPL, --  20, (1), (2012), 121 -- 153.


\bibitem{rb43a} Rybakov V. V., {\em Multi-agent logics with interaction, unifiability and projectivity}, --  Siberian Electronic Mathematical Reports, --  21, (2), (2024), 1370-1384.


\end{thebibliography}

\end{document}
