\documentclass[11pt,reqno]{amsart}
\usepackage[cp1251]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage[colorlinks]{hyperref}


\usepackage{titlesec}
\titlespacing{\section}{0pt}{2.5ex}{1.5ex}
\titlespacing{\subsection}{0pt}{1.5ex}{1ex}
\titlespacing{\subsubsection}{0pt}{1.5ex}{1ex}
\titleformat{\section}{\large\bfseries\centering}{\thesection}{1em}{}
\titleformat{\subsection}[runin]{\bfseries}{\thesubsection.}{0.5em}{}[.\mbox{\ }]
\titleformat{\subsubsection}[runin]{\bfseries}{\thesubsubsection.}{0.4em}{}[.\mbox{\ }]



%%%%%---------- ORCiD
\newcommand\orcidicon[1]{\href{https://orcid.org/#1}{\includegraphics[scale=0.02]{orcid.pdf}}}

\def\udcs{510.64} %Здесь автор определяет УДК своей работы
\def\mscs{03B44, 03B42, 03A05, 03B45, 03B70,03H05} %Здесь автор определяет классификаторы AMS своей работы
\setcounter{page}{144}

\newtheorem{lemma}{Лемма}
\newtheorem{theorem}{Теорема}
\newtheorem{definition}{Определение}
\newtheorem{corollary}{Следствие}
\newtheorem{proposition}{Предложение}


\definecolor{myblue}{rgb}{0.03, 0.27, 0.79}

\hypersetup{linkcolor=blue,filecolor=black,urlcolor=blue, citecolor=blue}

\def\logo{\textcolor{blue}{{\bf\Huge S\raisebox{0.2ex}{\hspace{0.55ex}\raisebox{0.05ex}e\hspace{-1.65ex}$\bigcirc$}MR}}}

\def\semrtop
     {
  \vbox{
     \noindent\logo \hspace{-3mm}  \parbox{12cm}{     \begin{center}
     {\LARGE \textsf{СИБИРСКИЕ ЭЛЕКТРОННЫЕ}} \\[2mm]
     {\LARGE \textsf{МАТЕМАТИЧЕСКИЕ ИЗВЕСТИЯ}} \\[2mm]
     {\Large \textsf{Siberian Electronic Mathematical Reports}} \\[1mm]
     {\Large\tt{\textcolor{blue}{http://semr.math.nsc.ru}}}\\[1mm]
     \raisebox{1ex}{ISSN 1813-3304 }
     \vspace*{-3mm}
%     {\small Институт математики им. С.Л.Соболева СО РАН}\\[-1mm]
%     {\small Sobolev Institute of Mathematics SB RAS}
     \end{center}
}
     \vspace{-1mm}
     \noindent
      \begin{tabular}{c}
     \hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa!} \\
     \hline\hline
     \end{tabular}

     \vspace{3mm}
     {\flushleft\it Том 20, № 2, стр. 144--145 (2023) \hspace{\fill}{\rm\small УДК \udcs \hspace{-4mm}}}
     \newline
     	{\rm\small \textcolor{blue}{https://doi.org/10.33048/semi.2023.20.???}}\hphantom{aaaaaaaaaaaaaaaaaaaaaaaa\;}{\rm\small MSC\ \ \mscs }
  }%\vbox
}



\begin{document}
\renewcommand{\refname}{References}


\thispagestyle{empty}

\title[\sc Линейная ступенчатая логика знания $\mathcal{LTK}.{sl}$]{\large Линейная ступенчатая логика знания $\mathcal{LTK}.{sl}$}
\author[С.И. БАШМАКОВ, Т.Ю. ЗВЕРЕВА]{{\bf \large \textsc{С.И. Башмаков, Т.Ю. Зверева}}\protect\orcidicon{0000-0002-3354-0383}\protect\orcidicon{0000-0002-9222-1331} \\
\textit{Представлено} \textsc{П.П. Петровым}
%\textit{(заполняется редакт ором)}
}%
\address{Stepan Igorevich Bashmakov % Контактные данные всех авторов и место работы указываются только на английском языкеse
\newline\hphantom{iii} Siberian Federal University,
\newline\hphantom{iii} pr. Svobodny, 79,
\newline\hphantom{iii} 600041, Krasnoyarsk, Russia}%
\email{\textcolor{blue}{krauder@mail.ru}}%

\address{Tatyana Yurievna Zvereva % Контактные данные всех авторов и место работы указываются только на английском языкеse
\newline\hphantom{iii} Siberian Federal University,
\newline\hphantom{iii} pr. Svobodny, 79,
\newline\hphantom{iii} 600041, Krasnoyarsk, Russia}%
\email{\textcolor{blue}{3336259@gmail.com}}%

\thanks{\sc Bashmakov, S.I., Zvereva T.Yu.,
Linear Step-like logic of knowledge $\mathcal{LTK}.{sl}$}
\thanks{\copyright \ 2023 Башмаков С.И.}
\thanks{\rm Первый автор поддержан Российским научным фондом, Правительством Красноярского края и Красноярским краевым фондом науки (грант 22-21-20028).}
\thanks{\it Поступила 1 января 2023 г., опубликована 31 декабря 2023 г.}%


\semrtop \vspace{1cm}
\maketitle {\small
\begin{quote}
\noindent{\bf Abstract:} This paper proposes a description of linear multi-agent logic of knowledge $\mathcal{LTK}.{sl}$ that models a linear non-reflexive non-transitive (step-like) temporal process of transition between information clusters --- time points.

Using modified techniques, we proved the finite approximability of logic. We proposed an approach for solving the main unification problem in logics of a step-like temporal relation. The projectivity and, as a consequence, unitary type of unification in logic are proved.
\medskip

\noindent{\bf Keywords:} modal logics, temporal logics, finite model property, linear time, Kripke relational semantics, multi-agent logic, unification.
 \end{quote}
}

\bigskip

\section{Введение}

Модальные и временные логики с середины прошлого века держат планку интенсивно развивающейся области знания, что обусловлено их фундаментальным значением и широкой применимостью в информационных системах \cite{Prior, ShapShech, VanDerMeyden}. Наиболее ярким примером, пожалуй, являются линейная временная логика $\mathcal{LTL}$ и логика деревьев вычислений (ветвящегося времени) $\mathcal{CTL}$, используемые в теории верификации программ и, фактически, составляющие её фундамент, \cite{Karpov}. 

В последние годы возрастает необходимость поиска эффективных инструментов для реализации новых запросов к моделированию процесса передачи информации --- в частности, обусловленных <<плохими>> условиями реализации информационного процесса, невыразимыми стандартными операторами. Одним из актуальных направлений в этой области является рассмотрение отношений и систем с операторами, нарушающими по своей природе принципы транзитивности временного (модального \cite{KudShap}) процесса: в ограниченных диапазонах достижимости или всюду в процессе рассуждений, \cite{Ryb2015, R_InTrz}.

В терминологии  интенсивно развивающейся области модальных и временных логик, актуально воспринимать временной процесс как вычислительную процедуру, позволяющую апеллировать понятием знания в условиях дискретно изменяющегося направленного времени. Здесь введение условия на нетранзитивность приводит к необходимости поиска, зачастую, принципиально новых подходов к анализу свойств логики в сравнении с транзитивными вариантами, поскольку стандартные понятия и техники разрабатывались и применялись, в основном, для логических систем <<хороших>> характеристик.

В качестве такой системы ранее нами была предложена линейная временная логика знания с <<универсальной модальностью>> $\mathcal{LTK}.{sl}_U$ \cite{BashZver}. Для обозначения временного процесса, обладающего свойством достижимости только следующего момента времени, был введён термин <<ступенчатого>> перехода временных состояний (с англ. \textit{step-like}), а универсальная модальность позволила определить всеобщую достижимость на моделях логики, избегая проблем конечной модальной достижимости каждой формулы, \cite{GorPassy}. Задачей данной работы стало исследование версии логики $\mathcal{LTK}.{sl}_U$, сохраняющей ступенчатую природу временного процесса, но лишённой оператора универсальной модальности, доказательство финитной аппроксимируемости, а также унитарности унификации, используя нестандартный взгляд на понятие проективной формулы в условиях нетранзитивного характера единственного отношения достижимости.

Для задач семантической характеризации неклассических логик широко применяется развитая \textit{реляционная семантика Крипке} --- подход, основанный на структурно-графической интерпретации логических систем при помощи модельного представления. Логику $\mathcal{LTK}.{sl}_U$ определяли и исследовали именно на языке реляционной семантики, \cite{BashZver}, логику обеднённого языка $\mathcal{LTK}.{sl}$ мы рассматриваем используя тот же подход, для удобства обобщая базовую технику сразу на мультимодальный случай.



\section{Семантика логики $\mathcal{LTK}.{sl}$}

Алфавит языка $L^{\mathcal{LTK}.{sl}}$ включает счётное множество пропозициональных переменных $Prop=\{p_{1},\dots,p_{n},\dots\}$, константы $\top , \bot$ скобки $(,)$, стандартные булевы операции и набор унарных модальных операторов \{$N$, $\Box_1,\dots,\Box_n$, $\Box_e$\}.

(Многомодальным) $\mathcal{LTK}.{sl}$-фреймом назовём упорядоченный набор $F:=\langle W_{\mathbb{N}}, \mathbf{Next}, R_e, R_1,\dots,R_n\rangle$, где
\begin{itemize}
    \item $W_{\mathbb{N}} = \bigcup_{t\in\mathbb{N}} C_t$ -- совокупность сгустков $C_t$, пронумерованных натуральными числами:  $C_{t_1} \cap C_{t_2}=\emptyset$, если $t_1\neq t_2$;
	\item $\mathbf{Next}$ -- отношение <<следующее натуральное число>>: 
$$\forall a,b \in W: a \mathbf{Next} b \Leftrightarrow \exists t\in \mathbb {N} (a\in C_t \,\&\, b\in C_{t+1});$$
	\item $R_e$ -- отношение эквивалентности на каждом сгустке:
 $$ \forall t\in \mathbb {N}, \forall a,b \in C_t: a R_e b,$$
$$R_e \subseteq \bigcup_{t\in\mathbb{N}} (C_t)^2;$$
	\item $R_1, \dots ,R_n$ -- отношения знаний агентов, каждое из которых задаёт отношение эквивалентности на некотором подмножестве элементов каждого момента времени (сгустка):
	$$\forall i\in [1,n] \, R_i \subseteq R_e.$$

 
\end{itemize}

Моделью на  $\mathcal{LTK}.{sl}$-фрейме $F$ назовём пару $M:=\langle F,V \rangle$, где $F$ -- $\mathcal{LTK}.{sl}$-фрейм, $V$ -- означивание: $Prop \mapsto 2^{W_{\mathbb{N}}}$. Тогда выводимость формул, содержащих модальные операторы, задаётся следующим образом: $\forall a\in C_t\subseteq W_{\mathbb{N}}, \forall t\in \mathbb{N}$:

a. $\langle F, a\rangle \models_{V} \varphi \wedge \psi \Leftrightarrow \langle F, a\rangle \models_{V} \varphi$ и $\langle F, a\rangle \models_{V} \psi $;

b. $\langle F, a\rangle \models_{V} \varphi \vee \psi \Leftrightarrow \langle F, a\rangle \models_{V} \varphi$ или $\langle F, a\rangle \models_{V} \psi$;

c. $\langle F, a\rangle \models_{V} \bar \varphi \Leftrightarrow \langle F, a\rangle \not\models_{V} \varphi$;

d. $\langle F, a\rangle \models_{V} N\varphi \Leftrightarrow \forall b \in C_{t+1} : \langle F, b\rangle \models_{V} \varphi$;

e. $\langle F, a\rangle \models_{V} \Box_e \varphi \Leftrightarrow \forall b \in C_t : \langle F, b\rangle \models_{V} \varphi$;

f. $\langle F, a\rangle \models_{V} \Box_i \varphi \Leftrightarrow \forall b \in C_t : a \, R_i \, b \Rightarrow \langle F, b\rangle \models_{V} \varphi$.

Определяемая как множество формул истинных на всех таких моделях, логика $\mathcal{LTK}.{sl}$ моделирует линейный направленный временной процесс, в котором из текущего временного состояния (сгустка $t$) достижим только следующий момент времени --- тем самым, временной процесс представляет собой направленный в будущее луч, разделённый на дискретные такты вычислений или рассуждений.

Отношение всеобщей достижимости внутри каждого сгустка $R_e$ задаёт саму совокупность непересекающихся сгустков, а линейную связь между ними --- временное отношение  $\mathbf{Next}$. Взаимодействие внутри временного процесса обеспечивают агенты, а доступную для них информацию (\textit{знания}) конечное (заранее определенное, но произвольное) агентные отношения $R_1, \dots ,R_n$, каждое из которых является некоторым подмножеством отношения $R_e$. Агенты могут интерпретироваться и как субъекты социального взаимодействия, и как элементы систем администрирования, обладающие собственной совокупностью доступной информации или прав в каждый момент времени. \textit{Общее знание} (англ. \textit{Common Knowledge}) определяется отношением $R_e$.

Стоит отметить, что ограничения, накладываемые на доступные некоторому агенту знания могут задаваться как отдельным отношением $R_i$, так и некоторым их объединением. Однако, концептуально важна возможность недостижимости некоторой части информации ни одному агенту, а значит объединение всех $n$ заданных на $\mathcal{LTK}.{sl}$-фрейме отношений не обязательно всюду совпадает с отношением Общего знания.

\section{Финитная аппроксимируемость в $\mathcal{LTK}.{sl}$}

\textit{Финитная аппроксимируемость} является важным свойством логических систем, поскольку позволяет нам оперировать в описании логики конечными моделями, а не их бесконечными вариантами. Логика $\mathcal{L}$ \textit{финитно аппроксимируема} (обладает \textit{свойством конечной модели}), если она полна относительно класса конечных фреймов, \cite{Chagr}.

Отметим, что нерефлексивный нетранзитивный характер временного отношения, в совокупности с необходимостью сохранить эффективную модель реализации временного процесса, не позволяют нам в явном виде ограничиться эффективными техниками р-морфизма или фильтрации --- в обоих случаях классическое применение методов привело бы к смещению последовательности моментов времени: их отождествлению или возникновению временных коллизий. Для сохранения временной достижимости сгустков и связи агентов внутри них, нами предложен комбинированный метод доказательства финитной аппроксимируемости рассматриваемой логики $\mathcal{LTK}.{sl}$.

Переопределим в языке $\mathcal{LTK}.sl$ необходимые теоретико-модельные понятия и методы.

Под \textit{модальной степенью} $d(\alpha)$ формулы $\alpha$ в логике $\mathcal{LTK}.{sl}$ будем понимать число вложенных в $\alpha$ нетранзитивных нерефлексивных операторов $N$: $d(p) = d(\circ p) = 0$, где $\circ \in \{\neg ,\Box_e, \Box_i\};$
$\forall p\in Prop$ $d(\alpha \odot \beta) = max(d(\alpha); d(\beta))$, где $\odot\in\{\vee,\wedge \}; d(N \alpha)=d(\alpha)+1$. Иначе говоря, ни один из модальных операторов логики, кроме $N$, не увеличивает модальную степень, так как не требует рассмотрения иных, кроме текущего, временных состояний.

Длину $l(\alpha)$ формулы $\alpha$ логики $\mathcal{LTK}.{sl}$ определим по числу операторов формулы следующим образом:
$l(p)=0$; $l(\alpha \circ \beta\alpha) = l(\alpha) + l(\beta) + 1 $, где $\circ \in \{\wedge, \vee \}$;
$l(\bullet \alpha) = l(\alpha) + 1$, где $\bullet \in \{N, \neg ,\Box_e, \Box_i\}$.

%Для доказательства финитной аппроксимируемости логики $\mathcal{LTK}.sl$, определим p-морфное отображение конечной $\mathcal{LTK}.sl$-модели $M$ на конечную по времени и, используя технику фильтрации сгустков, построим модель со сгустками конечной мощности на p-морфном варианте.

\subsection{p-морфизм в $\mathcal{LTK}.sl$}


Отображение $f$ многомодального фрейма $F := \left\langle W, \mathbf{Next}, R_e, R_1, \dots, R_n\right\rangle$ на фрейм $F' := \left\langle W', R'_e, R'_1, \dots, R'_n\right\rangle$ называется \textit{$p$-морфизмом}, если $\forall a,b \in W \, \forall R \in \{\mathbf{Next}, R_e, R_1, \dots, R_n\}$:
\begin{enumerate}
	\item $a \,R \,b \Rightarrow f(a) R ' f(b)$;
	\item $f(a) R ' f(b) \Rightarrow \exists c \in W [a\, R\, c \wedge f(c) = f (b)]$.
\end{enumerate}


Для произвольной $\mathcal{LTK}.sl$-модели $M = \left\langle W, \mathbf{Next}, R_e, R_1, \dots, R_n, V\right\rangle$ определим конечную по числу временных сгустков модель $N$ следующим образом:
$$N := \left\langle \bigcup_{j\in[1,k+1]} C_{j}, \mathbf{Next}', R'_{e}, R'_{1}, \dots, R'_{n}, V'\right\rangle,$$
где:
\begin{itemize}
	\item $\bigcup_{j\in[1,k]} C_{j} \subset W$ -- конечное число сгустков, сгусток $C_{k+1}$ состоит из одного вырожденного элемента;
	\item $R'_{e}, R'_{1}, \dots, R'_{n}$ задаются как ограничения соответствующих отношений $R_e, R_{1}, \dots, R_{n}$ на сгустки $\bigcup_{j\in[1,k]} C_{j}$, дополненные следующими условиями: $\forall R\in \{R_e, R_{1}, \dots, R_{n}\}$
	\begin{center}
	   $\forall a,b \in W \setminus\{C_{1}, \dots, C_{k}\}$ если $a R b$, то $\,a=b\in C_{k+1} \, \& \, a \, R' \, b;$
	\end{center}

	\item $\mathbf{Next}'$ определяется следующим образом:
 \\ $\forall a \in \{C_{1}, \dots, C_{{k}}\}$ если $a \, \mathbf{Next} \, b$, тогда $b \in \{C_{2}, \dots, C_{k+1}\}$;
\\$\forall a \in W \setminus\{C_{1}, \dots, C_{k}\}$, $\forall b\in W$ если $a\, \mathbf{Next}\, b$, тогда $a,b \in C_{k+1}$ $\& \,a \,\mathbf{Next}' \, b$;
%	\item $ V' = V \cap\{C_{1}, \dots, C_{k}\}$.
  \item $V'(p) = V(p)\cap \bigcup_{j\in [1,k]} C_j$ для $p\in Prop$.
\end{itemize}

В целях согласования обозначений, будем далее называть определённый ранее бесконечный $\mathcal{LTK}.{sl}$-фрейм, как $F_{inf}$, а ограниченный по времени --- $F_{fin} := \left\langle \bigcup_{j\in[1,k+1]} C_{j}, \mathbf{Next}', R'_{e}, R'_{1}, \dots, R'_{n}\right\rangle$.

\vspace{2mm}
\begin{figure}[h]
\center{\includegraphics[width=13cm]{inf-fin_frame.jpg}}
\caption{Бесконечный фрейм $F_{inf}$ и конечный фрейм $F_{fin}$}
\end{figure}
\vspace{2mm}

\begin{theorem}
Любой $F_{fin}$ является $p$-морфным образом $F_{inf}$.
\end{theorem}

\begin{proof}

Зададим отображение $f$ фрейма 
$F_{inf}= \left\langle W, \mathbf{Next}, R_{e}, R_{1}, \dots, R_{n} \right\rangle$
на конечный по времени фрейм $F_{fin}=\left\langle \bigcup_{j\in[1,k+1]} C_{j}, \mathbf{Next}', R'_{e}, R'_{1}, \dots, R'_{n} \right\rangle$ следующим образом:
\begin{enumerate}
	\item $\forall x \in \bigcup_{j\in[1,k]} C_{j} \, f(x) = x$;
	\item $\forall x \in W \setminus \bigcup_{j\in[1,k]} C_{j}$ $f(x) = y$, где $y \in C_{k+1}$.
\end{enumerate}

Докажем, что для $f$ сохраняются условия (1.) и (2.) определения $p$-морфизма: $\forall a, b \in W$

(1.) Если $a \, \mathbf{Next} \,b$, то, по определению $\mathbf{Next}$, $a \in C_{i}$ и $b \in C_{{i+1}}$.
Если $b \in \{C_{2}, \dots, C_{k}\}$, тогда $f(a)=a$, $f(b)=b$ и $f(a)\, \mathbf{Next}' \,f(b)$. Если $b\in W \setminus \{C_{1}, \dots, C_{k}\}$, тогда $f(a) \in C_{k} \cup C_{k+1}$, а $f(b) \in C_{k+1}$ и $f(a) \,\mathbf{Next}'\, f(b)$.\\
Если $a \,R_{e} \,b$ и $ a, b \in C_{i} \in \{C_{1}, \dots, C_{k}\}$ тогда $f(a)\, R'_{e} \,f(b)$. Если $C_{i} \in W \setminus \{C_{1}, \dots, C_{k}\}$, тогда $f(a)=f(b)=y \in C_{k+1}$.

В силу $R_{i}\subseteq R_{e}, \, \forall i\in [1, \dots, n]$, для отношений $R'_{1}, \dots, R'_{n}$ доказательство аналогично $R_{e}$.

(2.) Если $f(a) \mathbf{Next}' f(b)$, то возможны следующие случаи:
\begin{itemize}
	\item В случае если $f(a) \mathbf{Next}' f(b)$, по определению отношения $\mathbf{Next}'$, $f(a) \in C_{i}, f(b) \in C_{{i+1}}$, где $i+1\in[2, \dots, k]$. В этом случае $f(a)=a$, а для $f(b)$ возможны 2 варианта:
	\begin{itemize}
		\item когда $f(b) \in \{C_{2}, \dots, C_{k}\}$, $b=c$ и $a \,\mathbf{Next} \,c$;
		\item когда $f(b) \in C_{k+1} \& f(a) \in C_{k}$, в качестве $c$ можно рассмотреть $\forall c \in C_{k+1}$, и тогда $a\, \mathbf{Next} \,c$.
	\end{itemize}	

	\item В случае если $f(a),f(b)\in C_{k+1}$, имеем $a\in C_{j}, b\in C_{j+1}$ где $\{C_j,C_{j+1}\} \subset W \setminus \{C_{1}, \dots, C_{k}\}$) и тогда в качестве $c$ мы возьмём $\forall x\in C_{j+1}$. 
 В этом случае $f(c)=f(b) \in C_{k+1} \subset F_{fin}$.

$\forall a, b \in W$ если $f(a) R'_{e} f(b)$, то возможны 2 варианта:
	\begin{itemize}
		\item если $f(a), f(b) \in C_{i}$, где $i\in \{1, \dots, k\}$, тогда $a\, R_{e} \, b$, где $a, b \in C_{i}$, $i \in [1, \dots, k]$. В этом случае $c \in C_{i}$;
		\item если $f(a), f(b) \in C_{k+1}$, тогда $a \, R_{e} \, b$ и $a, b \in W \setminus \{C_{1}, \dots, C_{{k}}\}$.
	\end{itemize}
Доказательство для случая отношений $R_{i}$ полностью повторяет рассуждения приведённые выше, в силу определения отношений $R_{i}$ как подмножеств $R_{e}$.
\end{itemize}
\end{proof}

\begin{theorem}
Пусть $M = \left\langle F_{inf}, V \right\rangle$ -- неограниченная по времени $\mathcal{LTK}.sl$-модель, $\alpha$ --- произвольная формула модальной степени $m$, $m\in \omega$. 
Тогда $\forall x \in\bigcup_{j\in[1,k-m]} C_{j} \subset F_{inf}$ ($m<k$) справедливо: 
$$\left\langle M, x \right\rangle \not\models \alpha\Leftrightarrow \left\langle N, x \right\rangle \not\models \alpha,$$
где $N= \langle F_{fin} , V' \rangle = \langle \bigcup_{j\in[1,k+1]} C_{j}, \mathbf{Next}', R'_{e}, R'_{1}, \dots, R'_{n}, V' \rangle$.
\end{theorem}

\begin{proof}
Докажем, что утверждение справедливо для всех формул логики $\mathcal{LTK}.sl$.
Доказательство будем вести индукцией по длине формулы $\alpha$. При $l(\alpha)=0$ имеем $\alpha=p$. По определению, модальная степень формулы в этом случае также равна 0 и утверждение верно $\forall x\in\bigcup_{j\in[1,k]} C_{j}$. 

Предположим, что утверждение теоремы верно $\forall\beta$: $l(\beta)<t$, т.е. 
$$\langle M,x\rangle \not\models \beta \Leftrightarrow \langle N,x\rangle \not\models \beta.$$
Докажем для $l(\alpha)=t$. Случаи $\alpha\in\{\neg\varphi, \Box_e\varphi, \Box_i\varphi, \varphi\vee\psi, \varphi\wedge\psi\}$ удовлетворяют индуктивной гипотезе, поскольку модальная степень формулы $\alpha$ не увеличивается путём добавления операторов $\{\neg, \Box_e, \Box_i\}$ к подформуле $\varphi$ меньшей длины и потенциально увеличивается добавлением $\{\vee, \wedge\}$ только до значения $max(d(\varphi), d(\psi))$, где $\varphi$ и $\psi$ также короче по длине (по определению истинности таких формул на моделях логики).

Пусть $\alpha=N\varphi$, $l(\varphi)=l(\alpha)-1$ и $d(\alpha) = d(\varphi)+1$. По индуктивной гипотезе $\langle M,x\rangle\not\models\varphi \Leftrightarrow \langle N,x\rangle\not\models\varphi$, где $x\in\bigcup_{j\in[2,k-(m-1)]} C_{j}$. По определению $N$ верно, что $\forall x\in C_{i} \langle M,x\rangle \models N\varphi \Leftrightarrow \forall y\in C_{{i+1}}$ (т.е. $x\,  \mathbf{Next} \, y$) 
$\left\langle M,y\right\rangle \models\varphi$, следовательно, $\exists x\in C_{i} \langle M,x\rangle \not\models N\varphi \Leftrightarrow \exists y\in C_{{i+1}}$
$\left\langle M,y\right\rangle \not\models\varphi$.

Тогда $\forall \hat{x}\in\bigcup_{j\in[1,k-m]} C_{j}$
$\langle M,\hat{x}\rangle\not\models N \varphi \Leftrightarrow \langle N,\hat{x} \rangle \not\models N \varphi$.
\end{proof}

Отметим, что полученная таким образом модель конечна по времени, но имеет неограниченную (а значит потенциально счётную) мощность сгустков. Чтобы получить конечную модель, применим модифицированный метод фильтрации --- ограниченной на сгустки.


\subsection{Ограниченная фильтрация для $\mathcal{LTK}.sl$}

Завершая построение конечной модели, адекватной нашей логике,
применим технику фильтрации к полученному в предыдущем разделе конечному по времени фрейму $F_{fin}$.

Пусть $M= \left\langle W, \mathbf{Next}, R_e, R_1, \dots, R_n V \right\rangle$ --- модель, построенная на бесконечном ${LTK}.sl$-фрейме, определённая ранее, $\Phi \subseteq For(L^{\mathcal{LTK}.sl})$ --- набор формул, замкнутых относительно подформул. Определим отношение эквивалентности ${\equiv_{\Phi}}$ на сгустках из $W$ следующим образом: $\forall t\in \mathbb{N}, \forall x,y\in C_t$
$$x {\equiv_{\Phi}} y \Longleftrightarrow  [\forall \alpha \in \Phi (\langle M,x\rangle \models \alpha \Leftrightarrow \langle M,y\rangle \models \alpha)].$$

Далее будем используем следующие обозначения:

\begin{itemize}
	\item $Var(\Phi)$ для набора всех переменных формул из $\Phi$;
	\item $[x]_{\equiv_{\Phi}} := \{ y\in W | x {\equiv_{\Phi}} y\}$ для классов эквивалентности;
	\item $W_{\Phi}:= \{[x]_{\equiv_{\Phi}} | \forall x\in W\}$ для множества всех таких классов;
	\item $C_{j_{\Phi}}:= \{[x]_{\equiv_{\Phi}} | \forall x\in C_{j}\subset F_{fin}\}$, $j\in[1,k+1]$, для каждого сгустка таких классов, полученных из сгустков $F_{fin}$.
\end{itemize}

Чтобы ограничить конечным числом все мощности сгустков элементов модели и, тем самым, получить конечную модель, определим фильтрацию множества $\Phi \subseteq For(L^{\mathcal{LTK}.sl})$ моделью
$$N_{\Phi}=\left \langle \bigcup_{j\in[1,k+1]} C_{j_{\Phi}}, \mathbf{Next}'_{\Phi}, R'_{e_{\Phi}}, R'_{1_{\Phi}}, \dots, R'_{n_{\Phi}}, V'_{\Phi} \right \rangle$$
на основе модели $N$ с $p$-морфным фреймом $F_{fin}$ и дополнительной последующей фильтрацией сгустков:
	
\begin{enumerate}
	\item $\forall p\in Var(\Phi) \,\, [V'_{\Phi}(p) = \{[a]_{\equiv_{\Phi}} | \langle N,a\rangle \models p\}];$
	\item $\forall a,b \in \{\bigcup_{j\in[1,k+1]} C_{j}\}, \,\,\, \forall R'\in [\mathbf{Next}', R'_{e}, R'_{1}, \dots, R'_{n}]$\\
	$$(a R' b \Rightarrow [a]_{\equiv_{\Phi}} R'_{\Phi} [b]_{\equiv_{\Phi}});$$
	\item $	\forall a,b \in \{\bigcup_{j\in[1,k+1]} C_{j_{\Phi}}\} $
		\begin{enumerate}
			\item $\forall l\in\{e,1,\dots,n\} \,\,\, ([a]_{\equiv_{\Phi}} R'_{l_{\Phi}} [b]_{\equiv_{\Phi}} \Longrightarrow [\forall \,	\Box_l \alpha \subseteq \Phi$ \\ 
			$$\langle N,a\rangle \models \Box_l \alpha \Rightarrow \langle N,b\rangle \models \alpha]);$$
			\item $ [a]_{\equiv_{\Phi}} \mathbf{Next}'_{\Phi} [b]_{\equiv_{\Phi}} \Longrightarrow ([\forall \,	N\alpha \subseteq \Phi$\\
			$$\langle N,a\rangle \models N\alpha \Rightarrow \langle N,b\rangle \models \alpha]).$$
		\end{enumerate}		
\end{enumerate}

В нашем случае также применимы известные условия построения минимальной и максимальной фильтрации:

\noindent\textbf{--- минимальная фильтрация}
$$N^{\,min}_{\Phi}=\left \langle \bigcup_{j\in[1,k+1]} C_{j_{\Phi}}, \mathbf{Next}', R'^{min}_{e_{\Phi}}, R'^{min}_{1_{\Phi}}, \dots, R'^{min}_{n_{\Phi}}, V'_{\Phi} \right \rangle,$$
где
\begin{itemize}
\item $\forall l\in\{e,1,\dots,n\}$ $R'^{min}_{l_{\Phi}} = \{([a]_{\equiv_{\Phi}}, [b]_{\equiv_{\Phi}}) | (a,b)\in R'_l\},$
%\item $\mathbf{Next}'^{min} = \{([a]_{\equiv_{\Phi}}, [b]_{\equiv_{\Phi}}) | (a,b)\in Next'\}$;
\end{itemize}		
\noindent\textbf{--- максимальная фильтрация}
$$N^{max}_{\Phi}=\left \langle \bigcup_{j\in[1,k+1]} C_{j_{\Phi}}, \mathbf{Next}', R'^{max}_{e_{\Phi}}, R'^{max}_{1_{\Phi}}, \dots, R'^{max}_{n_{\Phi}}, V'_{\Phi} \right \rangle,$$
где
\begin{itemize}
\item $\forall l\in\{e,1,\dots,n\}:$ $[a]_{\equiv_{\Phi}} R'^{max}_{l_{\Phi}} [b]_{\equiv_{\Phi}} \Leftrightarrow [\forall \,	\Box_l \alpha \subseteq \Phi (\langle N,a\rangle \models \Box_l \alpha \Rightarrow \langle N,b\rangle \models \alpha)].$
%\item $[a]_{\equiv_{\Phi}} \mathbf{Next}'^{max}_{\Phi} [b]_{\equiv_{\Phi}} \Leftrightarrow ([\forall \,	N\alpha \subseteq \Phi$ $\langle N,a\rangle \models N\alpha \Rightarrow \langle N,b\rangle \models \alpha]).$
\end{itemize}		

Полученные в результате описанной процедуры сгустки всякий раз будут иметь конечную мощность, в силу выбора множества $\Phi$, конечности числа отношений на фрейме и всех попарных вариантов их пересечений. По построению фильтрованной модели, верна следующая лемма:

\begin{lemma}

Пусть $N = \langle \bigcup_{j\in[1,k+1]} C_{j}, \mathbf{Next}', R'_{e}, R'_{1}, \dots, R'_{n}, V' \rangle$ --- ограниченная по времени p-морфная модель бесконечной $\mathcal{LTK}.sl$-модели $M$,
$\Phi \subseteq For(L^{\mathcal{LTK}.sl})$ -- замкнутое относительно подформул множество формул, модальная степень которых не превосходит $m$ $(m\in \omega, k>m)$,  
$$N_{\Phi}= \left\langle \bigcup_{j\in[1,k+1]} C_{j_{\Phi}}, \mathbf{Next}'_{\Phi}, R'_{e_{\Phi}}, R'_{1_{\Phi}}, \dots, R'_{n_{\Phi}}, V'_{\Phi} \right\rangle$$ 
--- фильтрованный вариант модели $N$ множеством $\Phi$.\\Тогда $\forall x\in \bigcup_{j\in[1,k-m]} C_{j}$, $\forall \alpha \in \Phi$:
$$\left\langle N, x \right\rangle \not\models \alpha \Leftrightarrow \left\langle N_{\Phi}, x \right\rangle \not\models \alpha.$$
\end{lemma}
	
В силу Теоремы 2 и Леммы 1, заключаем финитную аппроксимируемость $\mathcal{LTK}.sl$. Таким образом, в качестве моделей логики могут рассматриваться не только бесконечные модели $M$, но и модели, построенные на конечных $\mathcal{LTK}.sl$-фреймах для каждой соответствующей формулы.


\section{Унификация в $\mathcal{LTK}.sl$}

\subsection{Основные определения теории унификация}

Базовая проблема унификации формулируется в виде вопроса о возможности трансформирования формулы $\varphi(p_1,\dots,p_s)$ логики $\mathcal{L}$ в теорему путем замены её переменных. Если ответ положителен, формула $\varphi(p_1,\dots,p_s)$ называется  \textit{унифицируемой} в $\mathcal{L}$, а подстановка $\sigma:$ $p_i \mapsto \sigma_i, \forall p_i\in Var(\varphi)$ такая, что $\varphi(\sigma_1,\dots,\sigma_s) \in \mathcal{L}$, \textit{унификатором} формулы. \textit{Корневым} (англ. \textit{ground}, сокр. $gu$) будем называть унификатор, представляющий собой подстановку набора констант вместо переменных формулы.

Начало исследованию задачи унификации, положенное в 1960-е годы, \cite{Robin}, главным образом было связано с задачами, возникающими в области информационных наук: унификация рассматривалась как инструмент, позволяющий преобразовать целые блоки исполняемых процедур к виду универсальных макросов, что конечно, довольно далеко от сегодняшних задач, возникающих в области символической логики. Импульс же развитию теории унификации здесь в последние десятилетия можно смело связать с именем С. Гиларди, обнаружившим значимые связи теории с другими задачами, широкие перспективы дальнейших исследований и эффективный подход, основывающийся на понятии проективной формулы, \cite{Ghil1}.

Формула $\varphi(p_1,\dots,p_s)$ называется \textit{проективной} в логике $\mathcal{L}$, если существует унификатор $\tau$ формулы $\varphi$, такой, что $\Box\varphi \rightarrow [p_i \equiv \tau (p_i)] \in \mathcal{L}$ для всех $p_i\in Var(\varphi)$. Такой унификатор называется \textit{проективным}.

Многие известные системы, обладающие <<хорошими>> характеристиками (рефлексивностью, транзитивностью, линейностью или их слабыми вариантами), изучены с точки зрения унификации: для них успешно определён (или опровергнут требуемый) тип унификации, найдены алгоритмы построения лучших унификаторов (или доказано их отсутствие), \cite{DzW,Ghil1,Ghil2, R_CU,BashPM}. Исследования же других систем часто сопряжены с необходимостью модификации имеющихся или поиском новых методов и техник, \cite{Bash2018, BashZver}, что неизбежно ведёт к некоторому снижению активности исследований.

В частности, данное выше определение верно для произвольной логики, расширяющей модальную систему $\mathcal{S}4$, т.к. последняя позволяет оперировать с рефлексивным и транзитивным свойствами модального оператора $\Box$ в логике. Для определения проективной формулы в нашей логике, в отсутствие хотя бы выразимого оператора транзитивной достижимости, воспользуемся более универсальной записью определения: формулу $\varphi(p_1,\dots,p_s)$ будем называть \textit{проективной} в $\mathcal{L}$, если найдётся унификатор $\tau$ формулы $\varphi$ такой, что $\varphi \vdash_{\mathcal{L}} [p_i \equiv \tau (p_i)]$ для всех $p_i\in Var(\varphi)$. Нетрудно заметить, что данное определение несёт тот же смысл, что и данное выше. Как будет показано далее, этого переосмысления, в совокупности с предлагаемой конструкцией $\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e \varphi$, где $N^0 \,\Box_e \varphi = \Box_e \varphi$, в качестве в некотором роде замены транзитивного оператора, оказывается достаточно, чтобы определить проективный унификатор в логике.

Отметим ещё несколько важных для нас определений теории унификации. На множестве всех унификаторов формулы $\varphi$ определено отношение предпорядка <<более общий>>: унификатор $\sigma$ формулы $\varphi(p_1,\dots,p_s)$ называют \textit{более общим}, чем $\sigma_1$ в логике $\mathcal{L}$ (и пишут $\sigma_1 \preceq \sigma$), если найдётся подстановка $\gamma$ такая, что для всех переменных $p_i$ формулы $\sigma$ верно: $\sigma_1 (p_i)\equiv_{\mathcal{L}} \gamma (\sigma (p_i))$.

Относительно данного предпорядка, унификатор $\sigma$ будет называться \textit{максимальным} для формулы $\varphi(p_1,\dots,p_s)$, если для любого другого унификатора $\sigma^i$ либо $\sigma^i \preceq \sigma$, либо $(\sigma^i \npreceq \sigma) \& (\sigma \npreceq \sigma^i)$. Если $\sigma$ --- более общий, чем любой другой унификатор, он называется \textit{наиболее общим} (или кратко \textit{ноу}).

Понятие типа унификации также может быть дано, используя определённый выше предпорядок: логика имеет \textit{нульарный} тип унификации, если, относительно $\preceq$, существуют бесконечные последовательности унификаторов. Если каждая такая последовательность заканчивается максимальным элементом, логика имеет по крайней мере \textit{инфинитарный} тип. В случае если максимальных унификаторов конечное число ---  \textit{финитарный}. Наконец, логика обладает наилучшим --- \textit{унитарным} --- типом унификации, если для любой унифицируемой формулы в логике найдётся ноу.

\subsection{Унитарная унификация в $\mathcal{LTK}.sl$}

Пусть формула $\varphi$ --- формула модальной степени $d(\varphi)=m$, следовательно, $\varphi$ содержит $m$ вложимых операторов $N$. $k+1$ --- число сгустков, определяемое глубиной $p$-морфной $\mathcal{LTK}.sl$-модели, $k>m$, следовательно, для проверки истинности формулы $\varphi$ требуется $k-m$ шагов для любой стартовой точки из промежутка $\{1,\dots,k-m\}$.

%\begin{definition}
%Формула $\varphi(p_1,\dots,p_s)$ называется проективной в $\mathcal{LTK}.sl$, если существует унификатор $\tau$ формулы $\varphi$, такой, что $\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \Box_e \varphi \rightarrow [p_i \equiv \tau (p_i)]\in \mathcal{LTK}.sl$ для всех переменных $p_i\in Var(\varphi)$. Унификатор $\tau$ называется проективным.
%\end{definition}

Следуя Гиларди, \cite{Ghil1}, проективный унификатор определяет наиболее общий унификатор формулы, и, следовательно, в случае применимости ко множеству всех унифицируемых формул логики, устанавливает её унитарный тип.

Следующие два утверждение приводятся без доказательства, т.к. они полностью повторяют рассуждения из \cite{BashZver}, опуская в процессе лишь случай универсальной модальности.

\begin{lemma}
Для любого набора $c_1,\dots,c_r \in \{\top,\bot\}$  и любой формулы $\varphi(p_1,\dots,p_r)$ существует $c \in \{\top,\bot\}$, такая, что 
$$\forall x \in F, \langle F, x\rangle \models \varphi(c_1,\dots,c_r)\equiv c.$$
\end{lemma}

\begin{theorem}
Если формула $\varphi$ унифицируема в $\mathcal{LTK}.sl$, то $\varphi$ имеет корневой унификатор $gu$.
\end{theorem}

Следствием данных утверждений является возможность эффективного использования корневых унификаторов для доказательства унифицируемости формул в логике $\mathcal{LTK}.sl$ --- всякий раз достаточно рассмотреть не более, чем $2^s$ различный подстановок, чтобы определить существование подходящей константной, являющейся унификатором. 


\begin{theorem}
Любая унифицируемая формула в $\mathcal{LTK}.sl$ проективна.
\end{theorem}

\begin{proof}
Пусть $\varphi (p_1, \dots, p_s)$ унифицируемая в $\mathcal{LTK}.{sl}$ формула. Тогда для любой переменной  $p_i \in Var(\varphi)$ определим следующую подстановку $\sigma(p_i)$:
$$\sigma(p_i):= (\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \Box_e \varphi\wedge p_i) \vee (\neg\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \Box_e \varphi\wedge gu(p_i)),$$
где $gu(p_1), \dots, gu(p_s)$ --- корневой унификатор формулы $\varphi (p_1, \dots, p_s)$, полученный по алгоритму из предыдущей теоремы.

Возьмём любую бесконечную модель $M:=\langle F,V\rangle$ с произвольным означиванием $V$. Если $\sigma$ --- унификатор для $\varphi$, тогда $\sigma(\varphi) \in \mathcal{LTK}.{sl}$ и $\forall x \in F$ $\langle M,x\rangle \models_V \sigma (\varphi)$. Докажем, что подстановка $\sigma$ является унификатором для $\varphi$ в логике $\mathcal{LTK}.{sl}$.

1. Если   
$\forall x\in \{C_{1}, \dots, C_{k-m}\} \,\, \langle M,x\rangle \models_{V} \varphi$, то $\langle M,x\rangle \models_V \overset{k-m}{\underset{i=0}{\bigwedge}} N^i \Box_e \varphi$ и, следовательно, второй дизъюнктивный член будет опровергнут на $x$. Если $\langle M,x\rangle \models_V p_i$, тогда $\langle M,x\rangle \models_V \overset{k-m}{\underset{i=0}{\bigwedge}} N^i \Box_e \varphi \wedge p_i$, следовательно, $\langle M,x\rangle \models_V \sigma(p_i)$. Если $\langle M,x\rangle \models_V \neg \, p_i$, тогда $\langle M,x\rangle \not\models_{V} \overset{k-m}{\underset{i=0}{\bigwedge}} N^i \Box_e \varphi \wedge p_i$ и следовательно $\langle M,x\rangle \models_{V} \neg\sigma(p_i)$.  Как следствие, истинностное значение $\varphi (p_1, \ldots, p_s)$ на произвольном элементе $x$ при означивании $V$ совпадает с истинностью $\varphi (\sigma(p_1), \ldots, \sigma(p_s))$ на том же элементе при том же означивании $V$ и, в этом случае, $\langle M,x\rangle \models_V \sigma(\varphi)$.

2. Если  $\exists x\in \{C_{1}, \dots, C_{k-m}\} \langle M,x\rangle \models_V \neg \varphi$, тогда $\langle M,x\rangle \not\models_V \overset{k-m}{\underset{i=0}{\bigwedge}} N^i \, \Box_e \varphi$. В этом случае возможно выполнение второго дизъюнктивного члена, но первый при этом опровергается на $x$. Тогда истинностное значение для всех $\sigma(p_i)$ на $x$ совпадает с $gu(p_i)$ (т.е. $\sigma(\varphi)\equiv gu(\varphi)$), и поскольку $\langle M,x\rangle \models_V gu(\varphi)$ (в силу выбора корневого унификатора, $gu(\varphi) \in \mathcal{LTK}.{sl}$), снова  $\langle M,x\rangle \models_V \sigma(\varphi)$.
Следовательно, $\sigma(\varphi)\in \mathcal{LTK}.{sl}$ для унифицируемой в $\mathcal{LTK}.{sl}$ формулы $\varphi$.

Докажем, что $\sigma(\varphi)$ --- проективный унификатор. Если $\sigma(p_i)$ --- проективный унификатор для $\varphi$, то $\forall p_i \in Var(\varphi)$ по определению, мы получим следующее: 
$$
\varphi\vdash_{\mathcal{LTK}.{sl}} p_i \leftrightarrow [(\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e \varphi\wedge p_i) \vee (\neg\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e\varphi\wedge gu(p_i))].
$$
 Предположим обратное: пусть $\sigma$ не является проективным унификатором. В таком случае если $\vdash_{\mathcal{LTK}.{sl}} \varphi$, то

$$\varphi\nvdash_{\mathcal{LTK}.{sl}} p_i \leftrightarrow [(\overset{m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e \varphi\wedge p_i) \vee (\neg\overset{m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e\varphi\wedge gu(p_i))]. \,\,\,\,\,\,\,\,\,(1)$$
В этом случае
$$\varphi\nvdash_{\mathcal{LTK}.{sl}} p_i \rightarrow [(\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e\varphi\wedge p_i) \vee (\neg\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e\varphi\wedge gu(p_i))], \,\,\,\,\,(2)$$
или
$$\varphi\nvdash_{\mathcal{LTK}.{sl}} [(\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e \varphi\wedge p_i) \vee (\neg\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e\varphi\wedge gu(p_i))] \rightarrow p_i. \,\,\,\,\,(3)$$

Если (2), тогда $\varphi\vdash_{\mathcal{LTK}.{sl}} p_i$, но в этом случае $\varphi\vdash_{\mathcal{LTK}.{sl}} \overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e \varphi\wedge p_i$, благодаря $\vdash_{\mathcal{LTK}.{sl}}\varphi$ и $\vdash_{\mathcal{LTK}.{sl}} p_i$, и поэтому 
$$\varphi\vdash_{\mathcal{LTK}.{sl}} p_i \rightarrow [(\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e \varphi\wedge p_i) \vee (\neg\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e\varphi\wedge gu(p_i))].$$
Следовательно, выполнение (2) невозможно.

Если (3), то $\varphi\vdash_{\mathcal{LTK}.{sl}} [(\overset{k-m}{\underset{i=0}{\bigwedge}} N^i \,\Box_e \varphi\wedge p_i) \vee (\neg\overset{k-m}{\underset{i=0}{\bigwedge}} N^i\,\Box_e\varphi\wedge gu(p_i))]$, но это возможно только при $\varphi\vdash_{\mathcal{LTK}.{sl}} p_i$, поскольку $\varphi\vdash_{\mathcal{LTK}.{sl}} \overset{k-m}{\underset{i=0}{\bigwedge}} N^i\,\Box_e \varphi$. Как следствие, в дизъюнкции $\sigma (p_i)$ может выполняться только первый член. Поэтому справедливо $$\varphi\vdash_{\mathcal{LTK}.{sl}} [(\overset{k-m}{\underset{i=0}{\bigwedge}} N^i\,\Box_e \varphi\wedge p_i) \vee (\neg\overset{k-m}{\underset{i=0}{\bigwedge}} N^i\,\Box_e\varphi\wedge gu(p_i))] \rightarrow p_i,$$
что противоречит (3). Следовательно, $\sigma$ --- проективный унификатор для $\varphi$ в логике $\mathcal{LTK}.{sl}$, поэтому $\varphi$ --- проективная формула.
\end{proof}


\bigskip
\begin{thebibliography}{1} % Ссылки на литературу приводятся только на английском языке (даже если у источника нет англоязычной версии).

    %0
        \bibitem{Karpov} Ю.Г. Карпов,
				{\it Model Checking. Верификация параллельных и распределенных программных систем},
				СПб.: БХВ-Петербург, 2010.
    %1
        \bibitem{KudShap} А.В. Кудинов, И.Б. Шапировский,
				\href{https://doi.org/10.4213/im8476}{\it О разбиениях шкал Крипке конечной высоты},
				Izvestiya: Mathematics, {\bf 81} (2017), 592--617.
    %2
        \bibitem{R_InTrz} В.В. Рыбаков,
				\href{https://doi.org/10.17377/smzh.2017.58.514} {\it Интранзитивные временные многоагентные логики, информация и знание, разрешимость},
				Сибирский математический журнал, {\bf 58} (2017), 1128--1143.
    %3   
        \bibitem{ShapShech} И.Б. Шапировский, В.Б. Шехтман,
				{\it Современная модальная логика: между математикой и информатикой},
				Современная логика: основания, предмет и перспективы развития, М.: ИД Форум, 2018, 265--305.
    %4
        \bibitem{Bash2018} S.I. Bashmakov,
				\href{https://doi.org/10.17516/1997-1397-2018-11-1-3-9}
				{\it Unification in linear modal logic on non-transitive time with the universal modality},
				J. SibFU. Mathematics and Physics, {\bf 11} (2018), 3--9.
    %5
        \bibitem{BashPM} S.I. Bashmakov,
				\href{https://doi.org/10.1007/s11787-021-00287-0}
        {\it Unification in pretabular extensions of S4},
				Logica Universalis, {\bf 15} (2021), 381--397.
    %6        
        \bibitem{BashZver} S.I. Bashmakov, T.Yu. Zvereva,
				\href{https://doi.org/10.18778/0138-0680.2022.16},
        {\it Unification and finite model property for linear step-like temporal multi-agent logic with the universal modality},
				Bulletin of the Section of Logic, {\bf 51} (2022), 345–-361.
    %7
        \bibitem{Chagr} A. Chagrov, M. Zacharyaschev,
				{\it Modal Logic}, Oxford University Press, 1997.
    %8
        \bibitem{DzW} W. Dzik, P. Wojtylak,
				\href{https://doi.org/10.1093/jigpal/jzr028},
				{\it Projective unification in modal logic},
				J. Symbolic Logic, {\bf 20} (2012), 121--153.
    %9
        \bibitem{Ghil1} S. Ghilardi,
				\href{https://doi.org/10.1093/logcom/7.6.733},
				{\it Unification Through Projectivity},
				J. Logic Comput, {\bf 7} (1997), 733--752.
    %10
        \bibitem {Ghil2} S. Ghilardi,
				\href{https://doi.org/10.2307/2586506},
				{\it Unification in Intuitionistic logic},
				J. Symbolic Logic, {\bf 62} (1999), 859--880.
    %11
        \bibitem{GorPassy} V. Goranko, S. Passy,
				\href{https://doi.org/10.1093/logcom/2.1.5},
        {\it Using the universal modality: gains and questions},
				J. Logic and Computation, {\bf 2} (1992) 5--30.
    %12
        \bibitem{Prior} A. Prior,
				{\it Time and Modality}, Oxford University Press, 1957.
    %13
        \bibitem{Robin} J.A. Robinson,
				\href{https://doi.org/10.1145/321250.321253},
				{\it A machine oriented logic based on the resolution principle},
				J. of the ACM, {\bf 12} (1965), 23--41.  
    %14
        \bibitem{R_CU} V.V. Rybakov,
				\href{https://doi.org/10.1007/s11225-011-9354-y}
				{\it Best unifiers in transitive modal logics},
				Studia Logica, {\bf 99} (2011), 321--336.

    %12
        \bibitem{Ryb2015} V.V. Rybakov,
				\href{https://doi.org/10.1093/logcom/exv016},
				{\it Non-transitive linear temporal logic and logical knowledge operations},
				J. Logic and Computation, {\bf 26} (2015), 945--958.
    %13
        \bibitem{VanDerMeyden} R. van der Meyden, Ks. Wong,
				\href{https://doi.org/10.1023/A:1026181001368},
				{\it Complete Axiomatizations for Reasoning about Knowledge and Branching Time},
				Studia Logica, {\bf 75} (2003), 93--123.


\end{thebibliography}
\end{document}
