\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{\ }]


%\newcommand{\sneg}{\mathord{\sim}}
%\newcommand{\sbe}{\subseteq}
%\newcommand{\lra}{\leftrightarrow}
%\newcommand{\Lra}{\Leftrightarrow}
%\newcommand{\infest}{\mathbin{|\kern -.47em\thicksim}}
%\newcommand{\notinfest}{\mathbin{|\kern -.47em\thicksim\kern-.9em{/}}}
%\newcommand{\ph}{\varphi}
%\newcommand{\ra}{\rightarrow}
%\newcommand{\Ra}{\Rightarrow}
\newcommand{\tuple}[1]{\langle #1 \rangle}
%\newcommand{\g}{\Gamma}
%\newcommand{\cL}{\mathcal{L}}
%\newcommand{\cE}{\mathcal{E}}
%\newcommand{\cM}{\mathcal{M}}
%\newcommand{\cW}{\mathcal{W}}
%\newcommand{\cK}{\mathcal{K}}
%\newcommand{\bH}{{\mathbf H}}
%\newcommand{\bT}{{\mathbf T}}
%\newcommand{\bS}{{\mathbf S}}
%\newcommand{\K}{\mathbf{K}}
%\newcommand{\BK}{\mathbf{BK}}
%\newcommand{\BtK}{\mathbf{B3K}}
%\newcommand{\Nfb}{\mathbf{N4}^\bot}
%\newcommand{\Ntb}{\mathbf{N3}^\bot}
%\newcommand{\Nn}{\mathbf{N_9}}
%\newcommand{\Nf}{\mathbf{N_5}}
%\newcommand{\Bf}{\mathbf{B4}}
%\newcommand{\Bt}{\mathbf{B3}}
%\newcommand{\Sf}{\mathbf{S4}}
%\newcommand{\BSf}{\mathbf{BS4}}
%\newcommand{\BtSf}{\mathbf{B3S4}}
%\newcommand{\Frm}{\mathrm{Form}}
%\newcommand{\Prop}{\mathrm{Prop}}
%\newcommand{\id}{\mathrm{id}}
%\newcommand{\Lits}{\mathrm{Lit}^{\mathord{\sim}}}
%\newcommand{\B}{\Box}
%\newcommand{\D}{\Diamond}
%\newcommand{\Bb}{\blacksquare}
\newcommand{\Db}{\blacklozenge}




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


\def\udcs{510.64} %Here the author places classificators of the paper according to Russian classification system
\def\mscs{03B20,03B70} %Here the author places  classificators according to the AMS classification list.
\setcounter{page}{144}

\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{proposition}{Proposition}



\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 Vol. 20, No. 2, pp. 144--145 (2023) \hspace{\fill}{\rm\small УДК \udcs \hspace{-4mm}}}
		\newline  %Volume, pages in Russian, filled by Editorial board
		{\rm\small \textcolor{blue}{https://doi.org/10.33048/semi.2023.20.???}}\hphantom{aaaaaaaaaaaaaaaaaaaaaaaa\;}{\rm\small MSC\ \ \mscs }
	}%\vbox
}




\begin{document}
	\renewcommand{\refname}{References}
	\renewcommand{\proofname}{Proof.}
	\renewcommand{\figurename}{Fig.}
	
	
	
	
	\thispagestyle{empty}
	
	\title[Explosive and paraconsistent equilibrium logic]{\large On modal presentation of explosive and paraconsistent equilibrium logic}
	
	
	\author[S.P. ODINTSOV]{{\bf S.P. Odintsov}\protect\orcidicon{0000-0003-3115-1293}}
	
	
	
	\address{Sergei Pavlovich Odintsov
		\newline\hphantom{iii} Mathematical Institute RAN,
		\newline\hphantom{iii} ul. Gubkina, 8,
		\newline\hphantom{iii} 630090, Moskva, Russia}%
	\email{odintsov.sergey2013@yandex.ru}%
	
	
	\thanks{\sc Odintsov S.P.,
		On modal presentation of paraconsistent equilibrium logic}
	\thanks{\copyright \ 2025 Odintsov S.P.}
	\thanks{\rm The work was executed in Mathematical Institute RAN and supported by is supported by  the Russian Science Foundation (Project No. No.~23-11-00104, https://rscf.ru/project/23-11-00104/)}
	\thanks{\it Received ???, Published ???}%
	
	\semrtop \vspace{1cm}
	\maketitle {\small
		
		\vspace{-12pt}
		\centerline{{\it Communicated by} {\sc ???}
			%({\it filled by Editorial board})
		}
		
		\bigskip
		\bigskip
		
		\begin{quote}
			\noindent{\bf Abstract:} Fari\~{n}as del Cerro, Herzig and Su proved that the non-monotonic consequence relation determined by Answer Set Semantics (ASP) for logic programs with negation-as-failure can be embedded into a monotonic modal logic via a variation of G\"{o}del-Tarski Translation. This article generalizes the mentioned result to ASP for logic programs with two kinds of negation: negation-as-failure and strong negation and to PAS, the paraconsistent version of ASP admitting answer sets that are inconsistent w.r.t. the strong negation.  \medskip
			
			\noindent{\bf Keywords:} logic programs, negation-as-failure, strong negation, equilibrium logic, deductive base, temporal logic, equilibrium modal theory.
		\end{quote}
	}
	
	\bigskip
	The stable model (answer set) semantics for logic programs with negation-as-failure $\neg$ suggested by M.~Gelfond and V.~Lifschitz \cite{GL88} gives rise to a separate paradigm in the setting of Logic Programming, so called Answer Set Programming (ASP). An important fact was established by D.~Pearce \cite{Pe97}, who proved that the intermediate logic  $HT$ of ``here-and-there'', which is known also as the G\"{o}del-Smetanich logic and can be determined by a Kripke frame with two worlds, can serve as a tool for reasoning about answer sets. The main property involved is that answer sets can be viewed as a
	certain kind of minimal $HT$-models, which are called equilibrium models. The same holds for logic programs in the extended language, which includes not only the negation-as-failure $\neg$, but also the strong negation $\sim$ (which was originally introduced in Logic Programming under the name of classical negation \cite{GL91}). In this case \cite{Pe97} answer sets are in one-to one correspondence with equilibrium $\mathbf{N_5}$-models, where $\mathbf{N_5}$ can be considered as $HT$ enriched with the strong negation. More exactly, $\mathbf{N_5}$ is a finite-valued extension of the explosive Nelson logic $\mathbf{N3}$, which can be determined via a 5-element algebra. On the other hand, $\mathbf{N_5}$ is the least conservative extension of $HT$ in the lattice of $\mathbf{N3}$-extensions. The logic $\mathbf{N3}$ is based on the concept of constructible falsity, which was introduced into logic by D.~Nelson \cite{Ne49} via his system of constructive arithmetic with strong negation. The propositional fragment of Nelson's arithmetic, which is denoted now as $\mathbf{N3}$, was subsequently axiomatised by N.~Vorob'ev \cite{Vo52a,Vo52b}.
	
	A second key property relating non-classical logics with ASP was established in \cite{LPV2001}: programs are strongly equivalent wrt answer set semantics if and only if they are
	equivalent viewed as propositional theories  in $HT$ (in $\mathbf{N}_5$ if $\sim$ occurs in the language).
	Here, two
	programs $\Pi_1$ and $\Pi_2$ are called strongly equivalent if for
	any program $\Pi$, $\Pi_1 \cup \Pi$ and $\Pi_2 \cup \Pi$ have the
	same answer sets. This shows that  $HT$ and $\mathbf{N_5}$ can be used  for program transformation and optimisation.
	
	Paraconsistent version of answer set semantics (PAS) admits answer sets that are inconsistent w.r.t. the stong negation. PAS was studied as a logic 	programming semantics by C.~Sakama and K.~Inoue \cite{SI95}.
	Later,  the work  \cite{ADP04} has made some progress towards a logical, declarative style of
	characterization for PAS. However, \cite{ADP04} does not axiomatize or otherwise syntactically characterize the underlying (monotonic) logic of PAS. In \cite{OdPe05}, it was proved that semantical frames for the substructural logics used in \cite{ADP04} can be reduced to a simpler  Routley frames \cite{Ro74} with additional falsity constant. This provides a description of paraconsistent answer sets as a special kind of minimal Routley models. It is proved in \cite{OdPe05} that these Routley models determine an extension of the  paraconsistent Nelson logic $\mathbf{N4}^\bot$\cite{Od05}. This extension was denoted $\mathbf{N_9}$ due to the reason that it can be determined via a 9-element algebra. Again, $\mathbf{N_9}$ is the least conservative extension of $HT$ in the class of $\mathbf{N4}^\bot$-extensions. Finally, the strong equivalence theorem was proved \cite{OdPe05}: two programs are strongly equivalent iff they are equivalent as $\mathbf{N_9}$-theories.
	
	The next step towards the declarative treatment of ASP was done by L.~Fari\~{n}as del Cerro, A.~Herzig and E.~Su \cite{FdCHSu2014}. They  proved that the non-monotonic consequence relation determined by Answer Set Semantics (ASP) for logic programs with negation-as-failure can be embedded into a monotonic modal logic $\mathbf{MEM}$ via a variation of G\"{o}del-Tarski Translation \cite{Goedel1933}. This article generalizes the mentioned result to the ordinary and paraconsistent versions of ASP for logic programs with two kinds of negation: negation-as-failure and strong negation. To this end we need the possibility to embed the constructive logic with strong negation into a suitable modal logic.
	
	Belnapian version of normal modal logic {\bf BS4} \cite{OdWans2010} relates to  {\bf S4} in exacly the same way as the logic $\mathbf{N4}^{\bot}$ relates to intuitionistic logic. Its semantics can be obtained from that of {\bf S4} via replacement of two-valued valuations by four valued ones.  In each of possible worlds a formula may have one of four truth values $True$, $False$, $Neither$, $Both$ of Belnap-Dunn matrix {\bf BD4} \cite{Belnap77}, which provide a semantics for First Degree Entailment {\bf FDE} \cite{Dunn76}. In \cite{OdWans2010} it was proved that $\mathbf{N4}^{\bot}$ is faithfully embedded into the logic {\bf BS4} via the translation $T_B$, a natural modification of  G\"{o}del-Tarski translation. This result shows that modal companions of Nelson's logic extensions defined via $T_B$ belong to the lattice of {\bf BS4}-extensions (see \cite{VishOd2025} for details). So logics based on {\bf BS4}-extensions looks suitable for the goals of this article.
	
	In our reasoning we will essentailly follow the line depicted in \cite{FdCHSu2014}, but we make one serious modification. Following \cite{Font16} we understand a logic as a structural Tarskian consequence relation defined over some propositional language. According to this definition {\bf MEM} of \cite{FdCHSu2014} is rather a theory than a logic because it is not closed under substitutions. In our work we try maximally distinguish `logical' and `theoretical' parts of construction. First we define a kind of Belnapian temporal logic $\mathbf{BSK_{t2}}$ and proof that the Belnapian version $T_B$ of G\"{o}del-Tarski translation faithfully embeds the logic $\mathbf{N_9}$ (the deductive base of PAS) into $\mathbf{BSK_{t2}}$, and the same holds for $\mathbf{N_5}$ and the explosive version of  $\mathbf{BSK_{t2}}$. Further, we define theories over $\mathbf{BSK_{t2}}$ and its explosive extension and prove that equilibrium entailments over  $\mathbf{N_9}$ and $\mathbf{N_5}$ can be embedded into this theories.
	
	The paper is structured as follows. Section~1 contains neccessary information on contsructive logics, Belnapian modal logics and semantics of logic programs with negations. In Section~2 we define a special temporal logic $\mathbf{BSK_t}$ such that future and past modalities of  $\mathbf{BSK_t}$ are defined via accessibility relations that are not mutually inverse. We introduce also the logic $\mathbf{BSK_{t2}}$ that extends $\mathbf{BSK_t}$ imposing further restrictions on both accessibility relations. Section~3 investigates the $\blacksquare$-free fragment  of $\mathbf{BSK_{t2}}$ ($\blacksquare$ stands for the necessity in the past). We prove that this fragment of $\mathbf{BSK_{t2}}$  is a modal companion of the deductive base of the equilibrium entailment. Finally, in Section~4 we embed the equilibrium entailment into $\mathbf{BSK_{t2}}$.




	
	
	\section{Preliminaries}
	
	As usual by a {\em propositional language} $\mathcal{L}$ we mean a finite tuple of logical connectives and constants. The set $\mathrm{Form}_{\mathcal{L}}$ of $\mathcal{L}$-formulas is constructed in a usual way from the fixed countable set $\mathrm{Prop}$ of propositional variables and the constants of $\mathcal{L}$ with the help of $\mathcal{L}$-connectives. The languages we consider will include the implication connective $\rightarrow$. We will define logics in different propositional languages via Hilbert style deductive systems. And we assume that  every deductive system under consideration includes the standard axioms of intuitionistic logic $\mathbf{Int}$ in the list of its axioms and the rules of {\em modus ponens} (MP) and of substitution (SUB)
	\[ \text{(MP)}\ \ \frac{\varphi, \varphi\rightarrow\psi}{\psi}, \ \ \ \text{SUB}\ \ \frac{\varphi(p_1,\ldots,p_n)}{\varphi(\psi_1,\ldots,\psi_n)}\] in the set of its inference rules. With every logic $L$ defined in the language $\mathcal{L}$ we associate the inference relation $\vdash_L$. For a subset  $\Gamma\cup\{\varphi\}\subseteq\mathrm{Form}_{\mathcal{L}}$,  $\Gamma\vdash_{L}\varphi$ means that $\varphi$ can be obtained from the elements of $\Gamma$ and the theorems of $L$ with the help of (MP). Recall that a theorem of $L$ is a formula, which can be inferred from the axioms of $L$ with the help of all inference rules, not only (MP). We write $\varphi\in L$ instead of `$\varphi$ is a theorem of $L$'. 
	
	For a logic $L$ in the language $\mathcal{L}$, we denote by $\mathcal{E} L$ the family of all axiomatic extensions of $L$ in the same language.
	
	If $L_i$ is a logic in the language $\mathcal{L}_i$, $i=1,2$,  $L_1\cup L_2$ denotes a logic in the language $\mathcal{L}_1\cup\mathcal{L}_2$ defined by the union of axioms of $L_1$ and $L_2$ and the union of rules of these logics.
	
	A proper subset $\Gamma\subseteq\mathrm{Form}_{\mathcal{L}}$ is said to be a {\em prime} $L${\em -theory} if (i) $\Gamma$ contains all $L$-theorems; (ii) $\Gamma$ is closed under (MP) ($\varphi,\;\varphi\rightarrow\psi\in\Gamma$ implies $\psi\in\Gamma$); (iii) $\Gamma$ satisfies the disjunction property ($\varphi\vee\psi\in\Gamma$ implies $\varphi\in\Gamma$ or $\psi\in\Gamma$). Notice that the axioms of $\mathbf{Int}$ and (MP) allow to prove in a standard way  the Extension Lemma for every logic $L$ considered in the article. 
	
	\begin{lemma}\label{extlem} Let $\Gamma\not\vdash_{L}\varphi$. Then there exists a prime $L$-theory $\Sigma$ such that $\Gamma\subseteq\Sigma$ and $\Sigma\not\vdash_{L}\varphi$.
	\end{lemma}
	
	\subsection{Constructive logics with strong negation}
	
	The paraconsistent version $\mathbf{N4}^\bot$ \cite{Od05} of Nelson's constructive logic with strong negation is defined in the propositional language $\mathcal{L}^{\mathord{\sim}}$ including the absurdity constant $\bot$ and logical connectives $\wedge$, $\vee$, $\rightarrow$, $\mathord{\sim}$, standing respectively for conjunction, disjunction, weak implication and strong negation.   The set $\mathrm{Lit}^{\mathord{\sim}}$  of {\em literals} is defined as $\mathrm{Prop}\cup\{ \mathord{\sim} p\mid p\in \mathrm{Prop}\}$. Arbitrary $\mathbf{S}\subseteq \mathrm{Lit}^{\mathord{\sim}}$ can be represented as $\mathbf{S}=({\mathbf S}^+,{\mathbf S}^-)$, where
		\[ {\mathbf S}^+=\mathbf{S}\cap \mathrm{Prop}\ \ \mbox{and}\ \ {\mathbf S}^-=\{ p\mid \mathord{\sim} p\in\mathbf{S}\} \] 
	We say that $\mathbf{S}$ is {\em consistent} if ${\mathbf S}^+\cap {\mathbf S}^-=\varnothing$.
		
	
	The Hilbert style deductive system for $\mathbf{N4}^\bot$ has  (SUB) and (MP) as its only inference rules. The axioms include the standard list of axioms of intuitionistic logic in the language $\{\wedge,\vee,\rightarrow,\bot\}$:
	\begin{center}
		\begin{tabular}{l@{\qquad\qquad}l}
			\textbf{I1.} $p\rightarrow ( q\rightarrow p)$ & \textbf{I2.} $( p\wedge q)\rightarrow  p$ \\
			\textbf{I3.} $( p\rightarrow ( q\rightarrow\gamma))\rightarrow(( p\rightarrow q)\rightarrow ( p\rightarrow\gamma))$ & \textbf{I4.} $( p\wedge q)\rightarrow  q$ \\
			\textbf{I5.} $( p\rightarrow q)\rightarrow(( p\rightarrow\gamma)\rightarrow( p\rightarrow( q\wedge\gamma)))$ &
			\textbf{I6.} $ p\rightarrow( p\vee q)$ \\
			\textbf{I7.} $( p\rightarrow\gamma)\rightarrow(( q\rightarrow\gamma)\rightarrow(( p\vee q)\rightarrow\gamma))$  & \textbf{I8.} $ q\rightarrow( p\vee q)$  \\
			\textbf{I9.} $\bot\rightarrow p$ &
		\end{tabular}
	\end{center}

    \noindent
	plus the following strong negation axioms (where $\alpha \leftrightarrow \beta$ is an abbreviation for
	$(\alpha \rightarrow  \beta ) \wedge (\beta \rightarrow \alpha )$):
	
	\begin{center}
		\begin{tabular}{l@{\qquad\qquad}l}
			\textbf{N1.} $\sim( p \rightarrow  q) \leftrightarrow  (p \land  \mathord{\sim}  q)$ &
			\textbf{N2.}
			$ \mathord{\sim} ( p \land  q) \leftrightarrow   (\mathord{\sim}  p \vee \mathord{\sim} q)$ \\
			\textbf{N3.}
			$ \mathord{\sim} ( p\lor q) \leftrightarrow ( \mathord{\sim}  p \land  \mathord{\sim}  q)$ &
			\textbf{N4.}
			$\mathord{\sim}  \mathord{\sim}  p \leftrightarrow   p$ \\
			\textbf{N5.} $ \mathord{\sim} \bot$ &
		\end{tabular}
	\end{center}

	The explosive logic $\mathbf{N3}^\bot$ is obtained via adding $(p\wedge\mathord{\sim} p)\rightarrow q$ to the list of $\mathbf{N4}^\bot$-axioms, symbolically $\mathbf{N3}^\bot=\mathbf{N4}^\bot+\{ (p\wedge\mathord{\sim} p)\rightarrow q\}$. Notice that intuitionistic logic $\mathbf{Int}$ coincides with the $\mathord{\sim}$-free fragment of both logics, $\mathbf{N4}^\bot$ and $\mathbf{N3}^\bot$.  
	
	Kripke style semantics for Nelson's Logics is defined as follows. We say that a pair 
	$\mathcal{W}=\langle W,\leq\rangle$ is a {\em frame} if $\leq$ is a preorder on $W$, i.e., a reflexive and transitive relation.  An $\mathbf{N4}^\bot${\em -model} (4{\em -model} over frame $\mathcal{W}$) is a tuple $\mathcal{M}=\langle \mathcal{W},
		v^+,v^-\rangle$, where $\mathcal{W}$ is a frame and valuations $v^+, v^-:\mathrm{Prop}\rightarrow \langle W,\leq\rangle^+$ are such that for $x,y\in W$, $p\in\mathrm{Prop}$, and $\epsilon\in\{ +,-\}$ we have 
		\begin{equation}(x\in v^\epsilon(p)\ \text{and}\ x\leq y)\ \text{implies}\ y\in v^\epsilon(p).
			\label{cone}
		\end{equation} 
	In other words, both $v^+(p)$ and $v^-(p)$ are {\em cones} w.r.t. $\leq$.
		
		
	 	An  $\mathbf{N4}^\bot$-model $\mathcal{M}=\langle \mathcal{W},v^+,v^-\rangle$ is said to be an $\mathbf{N3}^\bot${\em -model} (3{\em -model} over $\mathcal{W}$) if
				\begin{equation}
		{v^+(p)} \cap {v^-(p)}\ =\ \varnothing \ \ \text{for all}\ \ p \in \mathrm{Prop}.
		\label{cons}
		\end{equation}
		Now we define two different relations $\models^+$ and $\models^-$ for verification and falsification of formulas in worlds of the model. Naturally, we use $v^+$ and $v^-$ to define verification and falsification of propositional variables: 
		\[{ \mathcal{M}, x\models^+ p}\ \Leftrightarrow\ {x \in v^+(p)}\,; \quad { \mathcal{M}, x\models^- p}\ \Leftrightarrow\ {x \in v^-(p)}\]
		Verification and falsification of complex formulas are defined as follows:
		
		\medskip
		\begin{tabular}{lll}
			
			$ \mathcal{M}, x\vDash^+ \alpha\wedge \beta$ & iff & $ \mathcal{M}, x\vDash^+ \alpha$ and $ \mathcal{M}, x\vDash^+ \beta$ \\
			
			\smallskip
			$ \mathcal{M}, x\vDash^- \alpha\wedge \beta$ & iff & $ \mathcal{M}, x\vDash^- \alpha$ or $ \mathcal{M}, x\vDash^- \beta$ \\
			
		
			
		 $ \mathcal{M}, x\vDash^+ \alpha\vee \beta$ & iff & $ \mathcal{M}, x\vDash^+ \alpha$ or $ \mathcal{M}, x\vDash^+ \beta$ \\
			
			\smallskip
			$ \mathcal{M}, x\vDash^- \alpha\vee \beta$ & iff & $ \mathcal{M}, x\vDash^- \alpha$ and $ \mathcal{M}, x\vDash^- \beta$ \\ 
			
			$ \mathcal{M}, x \vDash^+ \alpha\rightarrow \beta$ & iff & $\forall y\geq x$\ ($ \mathcal{M}, y\nvDash^+ \alpha$ or $ \mathcal{M}, y\vDash^+ \beta$) \\
			
			\smallskip
			$ \mathcal{M}, x\vDash^- \alpha\rightarrow \beta$ & iff & $ \mathcal{M}, x\vDash^+ \alpha$ and $ \mathcal{M}, x\vDash^- \beta$ \\
			
			\smallskip
			$ \mathcal{M}, x\nvDash^+ \bot$ & and &  $ \mathcal{M}, x\vDash^- \bot$ \\
			
			$ \mathcal{M}, x\vDash^+ \sim \alpha$ & iff &  $ \mathcal{M}, x\vDash^- \alpha$ \\
			
			$ \mathcal{M}, x\vDash^- \sim \alpha$ & iff & $ \mathcal{M}, x\vDash^+ \alpha$
			
		\end{tabular}
	
	\smallskip\noindent
	The persistence condition (\ref{cone}) can be generalized to arbitrary formulas, i.e., for every $\varphi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ and $\epsilon\in\{ +,-\}$ we have
	\begin{equation}
		(\mathcal{M},x\models^\epsilon \varphi\ \text{and}\ x\leq y)\ \text{implies}\ \mathcal{M},y\models^\epsilon \varphi.
		\label{conef}
	\end{equation}

	If $\mathcal{M}$ is an $\mathbf{N3}^\bot$-model, the consistency condition~(\ref{cons}) also can be generalized to arbitrary formulas, i.e., for any $\varphi$ and $x$ we have
  	\begin{equation} 
  		\mathcal{M},x\not\models^+\varphi\ \ \text{or}\ \ \mathcal{M},x\not\models^-\varphi.
  	\label{consf}
  \end{equation}	
	
	\medskip
	We say that $\varphi$ is {\em true} on $\mathcal{M}$ and write $\mathcal{M}\models\varphi$ if $\mathcal{M},x\models^+\varphi$ for all $x\in W$. We write $\mathcal{W}\models_4\varphi$ if $\varphi$ is true on every 4-model over $\mathcal{W}$, and $\mathcal{W}\models_3\varphi$ if $\mathcal{M}\models\varphi$ for every 3-model $\mathcal{M}$ over $\mathcal{W}$. For  $\Gamma\subseteq\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ and a world $x$ of $\mathcal{M}$, we write $\mathcal{M}\models\Gamma$   ($\mathcal{M},x\models^{\epsilon}\Gamma$, $\epsilon\in\{ +,-\}$)  if $\mathcal{M}\models\varphi$ ($\mathcal{M},x\models^{\epsilon}\varphi$) for all $\varphi\in\Gamma$.  If $\mathcal{M}\models\Gamma$, we say that $\mathcal{M}$ is a {\em model} of $\Gamma$. In a similar way, we write $\mathcal{W}\models_{\epsilon}\Gamma$ and say that $\mathcal{W}$ is an $\epsilon$-{\em model} of $\Gamma$, where $\epsilon\in\{ 3,4\}$, if $\mathcal{W}\models_{\epsilon}\varphi$ for all $\varphi\in\Gamma$. Finally, we write $\Gamma\models_{\mathcal{M}}\varphi$ if for every world $x$ of $\mathcal{M}$ we have $\mathcal{M},x\models\varphi$, whenever $\mathcal{M},x\models\Gamma$.
	
	For $L\in\mathcal{E}\mathbf{N4}^\bot$ and a class of frames $\mathcal{K}$ we say that 
	
	\begin{itemize}
		
		\item $L$ is {\em weakly} 3-{\em complete} (4-{\em complete}) w.r.t. $\mathcal{K}$ if  for every $\varphi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$
		\[ \varphi\in L\ \ \text{iff}\ \ \mathcal{M}\models\varphi\ \text{for every 3-model (4-model)} \ \mathcal{M}\  \text{over}\ \mathcal{W}\in\mathcal{K}.\]
			
		\item $L$ is {\em strongly} 3-{\em complete} (4-{\em complete}) w.r.t. $\mathcal{K}$ if  for every  $\Gamma\subseteq\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ and $\varphi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ we have
		\[ \Gamma\vdash_L\varphi\ \ \text{iff}\ \ \Gamma\models_{\mathcal{M}}\varphi\ \text{for every 3-model (4-model)} \ \mathcal{M}\  \text{over}\ \mathcal{W}\in\mathcal{K}.\]
		
		\end{itemize}
	
		Obviously, the strong 4- or 3-completeness implies the weak 4- or 3-completeness w.r.t. the same class of frames.
	
	The following characterization of $\mathbf{N4}^\bot$ \cite{Lo72} and $\mathbf{N3}^\bot$ \cite{Th69} is well known:
	
	\begin{itemize}
		\item $\mathbf{N4}^\bot$ is strongly 4-complete w.r.t. the class of all frames;
		\item $\mathbf{N3}^\bot$ is strongly 3-complete w.r.t. the class of all frames.
		\end{itemize} 
	
	Recall that $HT=\mathbf{Int}+\{ p\vee(p\rightarrow q)\vee\neg q\}$, where $\neg q$ abbreviates $q\rightarrow\bot$, is the greatest extension of $\mathbf{Int}$ different from the classical logic $\mathbf{CL}$. $HT$ is known as G\"{o}del-Smetanich logic or "hear-and-there"\ logic. We are interested in $\mathbf{N4}^\bot$- and $\mathbf{N3}^\bot$-extensions via the same axiom:
	\[ \mathbf{N_9}=\mathbf{N4}^\bot+\{ p\vee(p\rightarrow q)\vee\neg q\}\ \ \text{and}\ \ \mathbf{N_5}=\mathbf{N3}^\bot+\{ p\vee(p\rightarrow q)\vee\neg q\}.\]
	Both logics $\mathbf{N_9}$ and $\mathbf{N_5}$ are determined by the same  two-element partially ordered frame $\mathcal{W}^{HT}=\langle W^{HT},\leq\rangle$, where $W^{HT}=\{ h,t\}$ and $h\leq t$. More exactly, we have:
		\begin{itemize}
		\item $\mathbf{N_9}$ is strongly 4-complete w.r.t. the class $\{ \mathcal{W}^{HT}\}$;
		\item $\mathbf{N_5}$ is strongly 3-complete w.r.t. the class $\{ \mathcal{W}^{HT}\}$.
	\end{itemize} 
	%\[ \varphi\in\mathbf{N_9} \ \ \text{iff}\ \ \mathcal{W}^{HT}\models_4\varphi;\ \ \ \varphi\in\mathbf{N_5}\ \  \text{iff}\ \ \mathcal{W}^{HT}\models_3\varphi.\] 
	The choice of notation $\mathbf{N_9}$ and $\mathbf{N_5}$ is conditioned by the facts that $\mathbf{N_9}$ can be determined by a 9-element algebra \cite{OdPe05}, and $\mathbf{N_5}$ by a 5-element algebra \cite{Pe97}. 
	
	Since we have only two worlds, an $\mathbf{N_9}$-model $\mathcal{M}$ (over $\mathcal{W}^{HT}$) is completely determined by sets of literals verified in the worlds $h$ and $t$, so it can be identified with a pair $\langle{\mathbf H},{\mathbf T}\rangle$, where ${\mathbf H},{\mathbf T}\subseteq \mathrm{Lit}^{\mathord{\sim}}$	and
	\[ {\mathbf H}^+=\{ p\mid \mathcal{M},h\models^+ p\},\ \ {\mathbf H}^-=\{ p\mid \mathcal{M},h\models^- p\},\] \[ {\mathbf T}^+=\{ p\mid \mathcal{M},t\models^+ p\},\ \ {\mathbf T}^-=\{ p\mid \mathcal{M},t\models^- p\}.\]
	In view of (\ref{cone}) we have ${\mathbf H}\subseteq{\mathbf T}$. 	If $\mathcal{M}$ is an $\mathbf{N_5}$-model, the pair $\langle{\mathbf H},{\mathbf T}\rangle$ satisfies additionally the condition that ${\mathbf H}$ and ${\mathbf T}$ are consistent. 
	
	Further, we put
	\[ \mathbf{B4}=\mathbf{N4}^\bot +\{ p\vee \neg p\}\ \ \text{and}\ \ \mathbf{B3}=\mathbf{N3}^\bot + \{ p\vee\neg p\}.\]
	These logics can be considered as expansions of four- and three-valued Belnap-Dunn logics (see \cite{Od2008} and \cite{MOd2013} for details) via connectives $\rightarrow$ and $\bot$. They are characterized by a one-element frame $\mathcal{W}^T=\langle\{ t\}, \leq\rangle$:
	\begin{itemize}
		\item $\mathbf{B4}$ is strongly 4-complete w.r.t. the class $\{ \mathcal{W}^{T}\}$;
		\item $\mathbf{B3}$ is strongly 3-complete w.r.t. the class $\{ \mathcal{W}^{T}\}$.
	\end{itemize} 
	%\[ \varphi\in\mathbf{B4} \ \ \text{iff}\ \ \mathcal{W}^{H}\models_4\varphi;\ \ \ \varphi\in\mathbf{B3}\ \  \text{iff}\ \ \mathcal{W}^{H}\models_3\varphi.\]
	Naturally, every $\mathbf{B4}$-model $\mathcal{M}$ (over $\mathcal{W}^T$) can be identified with the set ${\mathbf T}$ of literals verified at $t$, i.e.
	\[ {\mathbf T}^+=\{ p\mid \mathcal{M},h\models^+ p\},\ \ {\mathbf T}^-=\{ p\mid \mathcal{M},h\models^- p\},\]
	If $\mathcal{M}$  is a $\mathbf{B3}$-model, then ${\mathbf T}$ must be consistent.
	
	\subsection{Belnapian modal logics}
	
The Belnapian versions $\mathbf{BK}$ and $\mathbf{BS4}$ of normal modal logics $\mathbf{K}$ and, respectively, $\mathbf{S4}$ were defined in \cite{OdWans2010}. We define  $\mathbf{BK}$ in the language  $\mathcal{L}^{\Box}= \mathcal{L}^{\mathord{\sim}}\cup\{\Box\}$ as it was done in \cite{OdWans2017}. The possibility operator is defined as $\Diamond\varphi:=\mathord{\sim}\Box\mathord{\sim}\varphi$. We also need the following abbreviations: $\neg\varphi:=\varphi\rightarrow\bot$, $\varphi\Leftrightarrow\psi:=(\varphi\leftrightarrow\psi)\wedge(\mathord{\sim}\varphi\leftrightarrow\mathord{\sim}\psi)$. The list of axioms of $\mathbf{BK}$ includes the following groups of axioms:

\begin{itemize} 
	
	\item[I.] The  axioms of classical logic in the language $\{\wedge,\vee,\rightarrow,\bot\}$.
	
	\smallskip
	\item[II.] The strong negation axioms of  $\mathbf{N4}^\bot$ plus
	\[ {\neg\mathord{\sim}\Box  p \leftrightarrow \Box\neg\mathord{\sim} p}\]
	
	\smallskip
	\item[III.] The modal axiom of $\mathbf{K}$: $\Box(p\rightarrow q)\rightarrow(\Box p\rightarrow\Box q)$
			
	\end{itemize}

	The list of inference rules includes (SUB), (MP) and the normalization rule (NR$_{\Box}$):
	\[ \frac{\varphi}{\Box\varphi}\]
	The following formulas are $\mathbf{BK}$-theorems:
	\begin{equation}
		\neg\Box p\leftrightarrow\Diamond\neg p, \ \ \neg\Diamond p\leftrightarrow\Box\neg p, \ \ \Diamond(p\wedge q)\rightarrow(\Diamond p\wedge\Diamond q)
		\label{BKtheorems}
	\end{equation}
	
	
	Logic $\mathbf{BS4}$ is an extension of $\mathbf{BK}$ obtained via adding the modal axioms of $\mathbf{S4}$, i.e.,
	\[ \mathbf{BS4}=\mathbf{BK} +\{ \Box p\rightarrow p,\ \Box p\rightarrow \Box\Box p \}.\]
	The explosive extensions of $\mathbf{BK}$ and $\mathbf{BS4}$ are defined as follows:
	\[ \mathbf{B3K}=\mathbf{BK}+\{ (p\wedge\mathord{\sim} p)\rightarrow q\}, \ \ \ \mathbf{B3S4}=\mathbf{BS4}+\{ (p\wedge\mathord{\sim} p)\rightarrow q\}\]
	
	
	
	To define Kripke style semantics for $\mathbf{BK}$ we use the same frames as for $\mathbf{K}$. Namely, we say that a pair 
	$\mathcal{W}=\langle W,R\rangle$ is an $\mathbf{K}$-{\em frame} if $R$ is a binary relation on $W$.   A $\mathbf{BK}${\em -model} (4{\em -model} over $\mathcal{W}$) is a tuple $\mathcal{M}=\langle \mathcal{W},
	v^+,v^-\rangle$, where $v^+, v^-:\mathrm{Prop}\rightarrow 2^W$.
	
	An $\mathbf{S4}$-{\em frame} $\mathcal{W}=\langle W,R\rangle$ is a $\mathbf{K}$-frame, where $R$ is preorder. A $\mathbf{BS4}${\em -model} is a $\mathbf{BK}$-model over an $\mathbf{S4}$-frame. 
	
	A $\mathbf{B3K}${\em -model} $\mathcal{M}=\langle \mathcal{W},v^+,v^-\rangle$ (3{\em -model} over $\mathcal{W}$) is a $\mathbf{BK}$-model  satisfying the consistency condition (\ref{cons}). A $\mathbf{B3S4}${\em -model} $\mathcal{M}=\langle \mathcal{W},v^+,v^-\rangle$ is a $\mathbf{B3K}$-model over an $\mathbf{S4}$-frame.
	
	The verification $\models^+$ and falsification $\models^-$ relations between worlds and formulas are defined in exactly the same way as for $\mathbf{N4}^\bot$-models in case of propositional variables, constant $\bot$, and  connectives $\vee$, $\wedge$, $\mathord{\sim}$. For $\rightarrow$ and $\Box$ we have: 
	

	\medskip
	\begin{tabular}{lll}
		
	
		
		$ \mathcal{M}, x \vDash^+ \alpha\rightarrow \beta$ & iff & $ \mathcal{M}, x\nvDash^+ \alpha$ or $ \mathcal{M}, x\vDash^+ \beta$ \\
		
		\smallskip
		$ \mathcal{M}, x\vDash^- \alpha\rightarrow \beta$ & iff & $ \mathcal{M}, x\vDash^+ \alpha$\ and\ $ \mathcal{M}, x\vDash^- \beta$ \\
		
		$ \mathcal{M}, x \vDash^+ \Box\alpha$ & iff & $\forall y (xRy\ \text{implies}\ \mathcal{M}, y\vDash^+ \alpha)$ \\
		
		
		$ \mathcal{M}, x\vDash^- \Box\alpha$ & iff & $\exists y (xRy\ \text{and}\ \mathcal{M}, y\vDash^- \alpha)$ \\
		
	\end{tabular}
	
	\smallskip\noindent
	It is easy to see that for possibility operator we have then:
	
		\medskip
	\begin{tabular}{lll}
		
			
		$ \mathcal{M}, x \vDash^+ \Diamond\alpha$ & iff & $\exists y (xRy\ \text{and}\ \mathcal{M}, y\vDash^+ \alpha)$ \\
		
		
		$ \mathcal{M}, x\vDash^- \Diamond\alpha$ & iff & $\forall y (xRy\ \text{implies}\ \mathcal{M}, y\vDash^- \alpha)$  \\
		
	\end{tabular}
	
	\smallskip\noindent
	
	Again for a $\mathbf{B3K}$-model $\mathcal{M}$ the consistency condition~(\ref{cons}) can be generalized to arbitrary formulas, i.e. $\mathcal{M},x\not\models^+\varphi$ or $\mathcal{M},x\not\models^-\varphi$ for any $\varphi$ and $x$. 
	
	The truth of a formulas in a $\mathbf{BK}$-model is defined via the verification relation, i.e.,  $\mathcal{M}\models\varphi$ means that $\mathcal{M},x\models^+\varphi$ for all $x\in W$. For a $\mathbf{K}$-frame $\mathcal{W}$ we write $\mathcal{W}\models_4\varphi$ if $\mathcal{M}\models\varphi$ for every 4-model $\mathcal{M}$ over $\mathcal{W}$, and $\mathcal{W}\models_3\varphi$ if $\mathcal{M}\models\varphi$ for every 3-model $\mathcal{M}$ over $\mathcal{W}$. For $\Gamma\cup\{\varphi\}\subseteq\mathrm{Form}_{\mathcal{L}^{\Box}}$, the relations $\mathcal{M}\models\Gamma$, $\Gamma\models_{\mathcal{M}}\varphi$, $\mathcal{W}\models_4\Gamma$, and $\mathcal{W}\models_3\Gamma$ are defined in an obvious way. 
	For  $L\in\mathcal{E}\mathbf{BK}$ and a class of $\mathbf{BK}$-frames $\mathcal{K}$, the sense of expressions `$L$ is weakly 4{\em -complete} (3{\em -complete}) w.r.t. the class $\mathcal{K}$' and `$L$ is strongly 4{\em -complete} (3{\em -complete}) w.r.t. the class $\mathcal{K}$' is defined in exactly the same way as for $\mathbf{N4}^\bot$-extensions.
	
	If $\mathcal{W}=\langle W,R\rangle$ is an $\mathbf{S4}$-frame, $\mathcal{M}=\langle\mathcal{W},v^+,v^-\rangle$ is a 4-model over $\mathcal{W}$, and $K\subseteq W$ is a cone w.r.t. $R$ ($x\in K$ and $xRy$ imply $y\in K$), then
	\[ \mathcal{W}^K:=\langle K,R\cap K^2\rangle, \ \ \mathcal{M}^K=\langle\mathcal{W}^K,v^+_K,v^-_K\rangle,\]
	where $v^+_K(p)=v^+(p)\cap K$ and $v^-_K(p)=v^-(p)\cap K$. For any $x\in K$, $\varphi\in\mathrm{Form}_{\mathcal{L}^{\Box}}$, and $\epsilon\in\{ +,- \}$ we have 
		\begin{equation}
			\mathcal{M},x\models^{\epsilon}\varphi\ \ \text{iff}\ \ \mathcal{M}^K,x\models^{\epsilon}\varphi 
			\label{genmodel}
			\end{equation}
	
	In \cite{OdWans2010} the following results were proved:
	
	\begin{itemize}
		\item $\mathbf{BK}$ is strongly 4-complete w.r.t. the class of all $\mathbf{K}$-frames;
		\item $\mathbf{B3K}$ is strongly 3-complete w.r.t. the class of all $\mathbf{K}$-frames;
		\item $\mathbf{BS4}$ is strongly 4-complete w.r.t. the class of all $\mathbf{S4}$-frames;
		\item $\mathbf{B3S4}$ is strongly 3-complete w.r.t. the class of all $\mathbf{S4}$-frames.
	\end{itemize} 

Moreover, it was proved in \cite{OdWans2010} that $\mathbf{N4}^\bot$ and $\mathbf{N3}^\bot$ are faithfully embedded into $\mathbf{BS4}$ and, respectively, into $\mathbf{B3S4}$ via an analog $T_B$ of the G\"{o}del-Tarski translation that embeds $\mathbf{Int}$ into $\mathbf{S4}$. The  translation $T_B:\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}\rightarrow\mathrm{Form}_{\mathcal{L}^{\Box}}$ is defined as follows:

\begin{minipage}{0.5 \textwidth}
	\begin{align*}
		T_B p &= \Box p \\
		T_B (\varphi \vee \psi) &= T_B \varphi \vee T_B \psi\\
		T_B (\varphi \wedge \psi) &= T_B \varphi \wedge T_B \psi\\
		T_B (\varphi \rightarrow \psi) &= \Box (T_B \varphi \rightarrow  T_B \psi)\\
		T_B \bot &= \bot\\
	\end{align*}
\end{minipage}
\begin{minipage}{0.4 \textwidth}
	\begin{align*}
		T_B \mathord{\sim} p &= \Box \mathord{\sim} p\\
		T_B \mathord{\sim}(\varphi \vee \psi) &= T_B \mathord{\sim} \varphi \wedge T_B \mathord{\sim} \psi\\
		T_B \mathord{\sim}(\varphi \wedge \psi) &= T_B \mathord{\sim} \varphi \vee T_B  \mathord{\sim} \psi\\
		T_B  \mathord{\sim} (\varphi \rightarrow\psi) &=  T_B \varphi \wedge T_B\mathord{\sim}    \psi \\
		T_B  \mathord{\sim}  \mathord{\sim}  \varphi &= T_B \varphi \\
		T_B \mathord{\sim}\bot &= \mathord{\sim}\bot\\
	\end{align*}
\end{minipage}
		
	 A logic $M\in\mathcal{E}\mathbf{BS4}$ is said to be a {\em modal companion} of $L\in\mathcal{E}\mathbf{N4}^\bot$ if $T_B$ faithfully embeds $L$ into $M$, i.e.
	\[ \varphi\in L\ \ \text{iff}\ \ T_B\varphi\in M\] 
	for all $\varphi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$. According to this definition $\mathbf{BS4}$ is a modal companion of $\mathbf{N4}^\bot$, and $\mathbf{B3S4}$ is a modal companion of $\mathbf{N3}^\bot$.
	
	Let $\mathcal{M}=\langle W,R, v^+,v^-\rangle$ be a {\bf BS4}-model. Define the new valuations
	$$v'^+(p)=\{ w\in W \mid \mathcal{M},w\models^+\Box p\}\ \ \mbox{and}\ \ v'^-(p)=\{ w\in W \mid \mathcal{M},w\models^+\Box\mathord{\sim} p\}.$$
	It is obvious that $\mathcal{M}'=\langle W,R, v'^+,v'^-\rangle$ is an ${\bf N4}^{\bot}$-model too.
	
	\begin{lemma}\label{useit}\cite{OdWans2010} Let $\mathcal{M}=\langle W,R, v^+,v^-\rangle$ be a {\bf BS4}-model, $x\in W$, and  $\varphi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$. Then
		$$\mathcal{M}',x\models^+\varphi\ \Leftrightarrow\ \mathcal{M},x\models^+ T_B\varphi .$$
	\end{lemma}

This simple fact allows to prove (see \cite{OdWans2010}) that $\mathbf{BS4}$ is a modal companion of $\mathbf{N4}^\bot$, and $\mathbf{B3S4}$ is a modal companion of $\mathbf{N3}^\bot$.
	
	
	 
	 
	\subsection{Logic programming preliminaries} .
	
	
	By a {\em logic program}  $\Pi$ we mean a set of rules of the form
		\[(r)\ \
		\ \alpha_1\vee\ldots\vee \alpha_k\leftarrow \beta_1\wedge\ldots\wedge
		\beta_n\wedge\neg \beta_{n+1}\wedge\ldots\wedge\neg \beta_{n+m},\] where
		$\alpha_i,\beta_j\in\mathrm{Lit}^{\mathord{\sim}}$.  
		We say that logic program $\Pi$ is {\em normal} if $k=1$ for all rules in 	$\Pi$, and that $\Pi$ is {\em positive} (w.r.t. $\neg$) if $m=0$ for all rules in $\Pi$. 
		
		Thus, the programs under consideration may contain two kinds of negation: the default negation, or negation-as-failure, denoted as $\neg$ (usually written as `not') and the strong or explicit negation \cite{GL91} that may occur in $\alpha_i$ and $\beta_j$. In what follows we will identify a rule of the form ($r$) with a formula
			\[(\beta_1\wedge\ldots\wedge
			\beta_n\wedge\neg \beta_{n+1}\wedge\ldots\wedge\neg \beta_{n+m})
		\ \rightarrow\ (\alpha_1\vee\ldots\vee \alpha_k)\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}},\] where $\neg\beta_j$ is understood as $\beta_j\rightarrow\bot$. A set ${\mathbf H}\subseteq\mathrm{Lit}^{\mathord{\sim}}$ is a model of a logic program $\Pi$ if ${\mathbf H}$ is a $\mathbf{B4}$-model of the set of all formulas corresponding to the rules of $\Pi$. 
		 
		 Now we recall the definition of stable models. Notice that originally Gelfond and Lifschitz \cite{GL88} defined stable models for positive normal programs.
		 
		 Let $\Pi$ be a logic program and ${\mathbf T}\subseteq\mathrm{Lit}^{\mathord{\sim}}$. The {\em Gelfond-Lifschitz reduct} ({\em GL-reduct}) of $\Pi$ w.r.t. ${\mathbf T}$ is a positive program obtained from $\Pi$ in two steps. First, we exclude from $\Pi$ all rules containing $\neg\beta_i$ for $\beta_i\in{\mathbf T}$. Second, we delete all conjunctive terms of the form $\neg\beta_i$ from the rest of rules.
		 
		 We say that ${\mathbf T}\subseteq\mathrm{Lit}^{\mathord{\sim}}$ is a {\em stable model} of $\Pi$ if ${\mathbf T}\models\Pi^{{\mathbf T}}$, and ${\mathbf H}\models\Pi^{{\mathbf T}}$ for ${\mathbf H}\subseteq{\mathbf T}$ implies ${\mathbf H}={\mathbf T}$. In other words, ${\mathbf T}$ is a minimal w.r.t. inclusion $\mathbf{B4}$-model of $\Pi^{{\mathbf T}}$.

		Now we define the relation $\unlhd$ among $\mathbf{N_9}$-models as follows. Let $\langle{\mathbf H}_1,{\mathbf T}_1\rangle$ and $\langle {\mathbf H}_2,{\mathbf T}_2 \rangle$ be $\mathbf{N_9}$-models. We set
		\[\langle {\mathbf H}_1, {\mathbf T}_1 \rangle \unlhd \langle {\mathbf H}_2, {\mathbf T}_2
		\rangle\ \ \text{iff}\ \ {\mathbf T}_1 = {\mathbf T}_2\ \ \text{and}\ \ {\mathbf H}_1 \subseteq {\mathbf H}_2.\]
		An $\mathbf{N_9}$-model of the form $\langle {\mathbf T},{\mathbf T} \rangle$ is called {\em total}.
		
		For an arbitrary subset $\Gamma\subseteq\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$, a total model $\langle {\mathbf T},{\mathbf T} \rangle$ is said to be an {\em equilibrium model of} $\Gamma$ if  $\langle {\mathbf T},{\mathbf T} \rangle\models\Gamma$ and there is no ${\mathbf H}\subseteq\mathrm{Lit}^{\mathord{\sim}}$ such that ${\mathbf H}\neq{\mathbf T}$ and $\langle{\mathbf H},{\mathbf T} \rangle\models\Gamma$. In other words an equilibrium model of $\Gamma$ is a total model of $\Gamma$, which is $\unlhd$-minimal in the class of $\mathbf{N_9}$-models of $\Gamma$.
		
		For logic programs, there is a close connection between stable and equilibrium models.
		
		\begin{theorem} \cite{OdPe05} For a logic program $\Pi$, a set ${\mathbf T}\subseteq\mathrm{Lit}^{\mathord{\sim}}$ is a stable model of  $\Pi$ iff $\langle {\mathbf T},{\mathbf T} \rangle$ is an equilibrium model of $\Pi$. 
		\end{theorem}
		Originally \cite{OdPe05} this statement was proved via the reduction to the results of \cite{ADP04}, a short direct proof can be found in \cite{MOd2013}.

		In what follows, $\mathcal{E} l_9(\Gamma)$ denotes the set of all equilibrium models of $\Gamma$, and $\mathcal{E} l_5(\Gamma)$ denotes the set of all consistent equilibrium models of $\Gamma$, i.e. the set of those equilibrium models of $\Gamma$ that are $\mathbf{N_5}$-models.  We define  equilibrium consequence relations as follows:
		\[ \Gamma\mathbin{|\kern -.47em\thicksim}^9_{el} \varphi\ \  \text{iff}\ \ \langle {\mathbf H},{\mathbf T} \rangle\vDash \varphi\ \  \text{for every} \langle {\mathbf H},{\mathbf T} \rangle\in\mathcal{E} l_9(\Gamma).\] 
		\[ \Gamma\mathbin{|\kern -.47em\thicksim}^5_{el} \varphi\ \  \text{iff}\ \ \langle {\mathbf H},{\mathbf T} \rangle\vDash \varphi\ \  \text{for every} \langle {\mathbf H},{\mathbf T} \rangle\in\mathcal{E} l_5(\Gamma).\] 
		
		


\section{Special temporal logic}

Similar to \cite{FdCHSu2014} we define a special temporal logic, where the future ($\Box$, $\Diamond$) and past ($\blacksquare$, $\blacklozenge$) modalities are defined via accessibility relations that are not mutually inverse, but however are closely connected. Prior to do it we recall the definition of a fusion of modal logics, and of the temporary version of $\mathbf{BS4}$ defined in \cite{OdWans2010}.

Let $\mathcal{L}^{\blacksquare}:=\mathcal{L}^{\mathord{\sim}}\cup\{\blacksquare\}$, $\mathcal{L}^{t}:=\mathcal{L}^{\Box}\cup\{\blacksquare\}$, and $\blacklozenge\varphi:=\mathord{\sim}\blacksquare\mathord{\sim}\varphi$.

For $L\in\mathcal{E}\mathbf{BK}$, we denote by $L_{\blacksquare}$ the logic in the language $\mathcal{L}^{\blacksquare}$ defined via the same axioms and rules as $L$ but with $\Box$ replaced by $\blacksquare$. Clearly,  $L_{\blacksquare}\in\mathcal{E}\mathbf{BK}_{\blacksquare}$.

For $L^1,\, L^2\in\mathcal{E}\mathbf{BK}$, we put $L^1\ast L^2:=L^1\cup L^2_{\blacksquare}$. We say that $L^1\ast L^2$ is a {\em fusion} of logics $L^1$ and $L^2$.

The temporal version $\mathbf{BS4_t}$ of $\mathbf{BS4}$ was defined in \cite{OdWans2010} as	\[\mathbf{BS4_t}=\mathbf{BS4}\ast\mathbf{BS4} + \{  p\rightarrow \Box \blacklozenge p,\;  p\rightarrow \blacksquare\Diamond p\}.\]

Frames and models are defined for $\mathbf{BS4}_t$ in the same way as for $\mathbf{BS4}$. For connectives of $\mathcal{L}^{\Box}$, the verification and falsification also are defined as for $\mathbf{S4}$-frames. For $\blacksquare$ we have:

\medskip
\begin{tabular}{lll}
	
	$ \mathcal{M}, x \vDash^+ \blacksquare\alpha$ & iff & $\forall y (yRx\ \text{implies}\ \mathcal{M}, y\vDash^+ \alpha)$ \\
	
	$ \mathcal{M}, x\vDash^- \blacksquare\alpha$ & iff & $\exists y (yRx\ \text{and}\ \mathcal{M}, y\vDash^- \alpha)$ \\
	
\end{tabular}

\smallskip
As a consequence for $\blacklozenge$ we have:

\medskip
\begin{tabular}{lll}
	
	$ \mathcal{M}, x \vDash^+ \blacklozenge\alpha$ & iff & $\exists y (yRx\ \text{and}\ \mathcal{M}, y\vDash^+ \alpha)$ \\
	
	
	$ \mathcal{M}, x\vDash^- \blacklozenge\alpha$ & iff & $\forall y (yRx\ \text{implies}\ \mathcal{M}, y\vDash^- \alpha)$  \\
	
\end{tabular}

\smallskip
All related notions are modified for the language $\mathcal{L}^t$ in an obvious way. 
Naturally, $\mathbf{BS4_t}$ is strongly 4-complete w.r.t. the class of all $\mathbf{S4}$-frames, and $\mathbf{B3S4_t}=\mathbf{B3S4_t}+\{ (p\wedge\mathord{\sim} p)\rightarrow q\}$ is strongly 3-complete w.r.t. the class of all $\mathbf{S4}$-frames.

Further, let us consider the fusion  \[\mathbf{BSK}=\mathbf{BS4}\ast\mathbf{BK}\]
and its explosive extension $\mathbf{B3SK}=\mathbf{BSK}+\{ (p\wedge\mathord{\sim} p)\rightarrow q\}$.

A $\mathbf{BSK}$-frame is a tuple $\mathcal{W}=\langle W,R,S \rangle$, where $R$ is a preoder on $W$ and $S\subseteq W^2$. A $\mathbf{BSK}$-model $\mathcal{M}=\langle \mathcal{W},v^+,v^- \rangle$ is a  $\mathbf{BSK}$-frame $\mathcal{W}$ augmented with two valuations $v^+,v^-:\mathrm{Prop}\rightarrow 2^W$. One can combine in an obvious way the completeness results for $\mathbf{BS4}$, $\mathbf{BK}$ and their explosive extensions from \cite{OdWans2010} to obtain the following 

\begin{theorem} Logic $\mathbf{BSK}$  ($\mathbf{B3SK}$) is strongly 4-complete (3-complete) w.r.t. the class of $\mathbf{BSK}$-frames.
\end{theorem} 

We denote by $\mathrm{id}_W$ the diagonal of $W$, i.e., $\mathrm{id}_W=\{ (a,a)\mid a\in W\}$.

\begin{proposition} Let $\mathcal{W}=\langle W,R,S \rangle$ be a $\mathbf{BSK}$-frame and $\epsilon\in\{ 3,4\}$. The following equivalences hold:
	
	\medskip
	\begin{tabular}{llll}
		{\em 1)} & $\mathcal{W}\models_{\epsilon} p\rightarrow\blacksquare\Diamond p$ & iff & $S\subseteq R^{-1}$; \\
		
		{\em 2)} & $\mathcal{W}\models_{\epsilon} p\rightarrow\Box(p\vee\blacklozenge p)$ & iff & $R\subseteq S^{-1}\cup\mathrm{id}_W$.
	\end{tabular}
\end{proposition}

\begin{proof} We fix some $\mathbf{BSK}$-frame $\mathcal{W}=\langle W,R,S \rangle$.
	
	1) This is one of standard axioms of temporal logic, and since $\mathord{\sim}$ does not occur in this formula the three- or four-valued case should not differ from the ordinary one. However we provide this proof to be self contained. Let  $S\subseteq R^{-1}$, and  let $\mathcal{M}=\langle \mathcal{W},v^+,v^- \rangle$ be a model over $\mathcal{W}$. Assume that $\mathcal{M},x\models^+ p$ and choose some $y$ with $xSy$. We have then $yRx$ by $S\subseteq R^{-1}$, and so $\mathcal{M},y\models^+\Diamond p$. Since $y$ is an arbitrary $S$-successor of $x$, we have $\mathcal{M},x\models^+\blacksquare\Diamond p$. We have thus proved that $S\subseteq R^{-1}$ implies $\mathcal{W}\models_4 p\rightarrow\blacksquare\Diamond p$ and, in particular,  $\mathcal{W}\models_3 p\rightarrow\blacksquare\Diamond p$.
	
To prove the inverse implication we assume that $S\not\subseteq R^{-1}$ and $x,y\in W$ are such that $xSy$ but $\neg(yRx)$. Let $\mathcal{M}=\langle \mathcal{W},v^+,v^- \rangle$ be such that $v^+(p)=\{ x\}$ and $v^-(q)=\varnothing$ for all $q\in\mathrm{Prop}$. Obviously, $\mathcal{M}$ is a $\mathbf{B3SK}$-model. In this case we have $\mathcal{M},x\models^+ p$ and $\mathcal{M},y\not\models^+ \Diamond p$, whence $\mathcal{M},x\not\models^+\blacksquare\Diamond p$. Thus,  $S\not\subseteq R^{-1}$ implies $\mathcal{W}\not\models_3 p\rightarrow\blacksquare\Diamond p$, moreover,  $\mathcal{W}\not\models_4 p\rightarrow\blacksquare\Diamond p$.

\medskip 
2) First we assume that $R\subseteq S^{-1}\cup\mathrm{id}_W$. Let $\mathcal{M}=\langle \mathcal{W},v^+,v^- \rangle$ be a model over $\mathcal{W}$ and $x,y\in W$ be such that $\mathcal{M},x\models^+ p$ and $xRy$. If $x=y$, then $\mathcal{M},y\models^+ p\vee\blacklozenge p$. If $x\neq y$, then $ySx$, and we again have $\mathcal{M},y\models^+ p\vee\blacklozenge p$. Consequently, $\mathcal{M},x\models^+ \Box(p\vee\blacklozenge p)$. We proved thus  $\mathcal{W}\models_4 p\rightarrow\Box(p\vee\blacklozenge p)$, moreover, $\mathcal{W}\models_3 p\rightarrow\Box(p\vee\blacklozenge p)$.

Now we assume that $R\not\subseteq S^{-1}\cup\mathrm{id}_W$ and choose  $x,y\in W$ such that $xRy$, $x\neq y$, and $\neg(ySx)$. As in Item~1 we take a $\mathbf{B3SK}$-model $\mathcal{M}=\langle \mathcal{W},v^+,v^- \rangle$ such that $v^+(p)=\{ x\}$ and $v^-(q)=\varnothing$ for all $q\in\mathrm{Prop}$. We have $\mathcal{M},x\models^+ p$. At the same time the conditions $x\neq y$ and $\neg(ySx)$ imply $\mathcal{M},y\not\models^+ p\vee\blacklozenge p$, whence $\mathcal{M},x\not\models^+ \Box(p\vee\blacklozenge p)$. Thus, $\mathcal{W}\not\models_3 p\rightarrow\Box(p\vee\blacklozenge p)$ and $\mathcal{W}\not\models_4 p\rightarrow\Box(p\vee\blacklozenge p)$.
	
\end{proof}

We define a weak version of $\mathbf{BS4_t}$ as follows:
\[\mathbf{BSK_t}:=\mathbf{BSK}+\{ p\rightarrow\blacksquare\Diamond p,\ p\rightarrow\Box(p\vee\blacklozenge p)\}.\]
We put also $\mathbf{B3SK_t}:=\mathbf{BSK_t}+\{ (p\wedge\mathord{\sim} p)\rightarrow q \}$.

To prove the completeness of $\mathbf{BSK_t}$ and of its axiomatic extensions via different classes of frames we will use the canonical model method.

First we notice that every prime $L$-theory $\Gamma$ over $L\in\mathcal{E}\mathbf{BSK_t}$ is complete and consistent w.r.t. $\neg$. Indeed, $\varphi\vee\neg\varphi\in\Gamma$ since $\mathbf{BSK_t}$ contains  axioms of classical logic in the language $\{\vee,\wedge,\rightarrow,\bot\}$. Consequently, the disjunction property of $\Gamma$ implies $\varphi\in\Gamma$ or $\neg\varphi\in\Gamma$. In particular, any two prime $L$-theories are incomparable w.r.t. set-theoretical inclusion $\subseteq$, i.e. for prime $L$-theories $\Gamma$ and $\Delta$ we have:
\begin{equation} \Gamma\neq\Delta\ \ \text{implies}\ \ \Gamma\setminus\Delta\neq\varnothing.
	\label{incomp}
	\end{equation}
If $\varphi,\neg\varphi\in\Gamma$, then $(\varphi\wedge\neg\varphi)\rightarrow\psi\in\Gamma$ implies that $\Gamma=\mathrm{Form}_{\mathcal{L}^t}$.

For $L\in\mathcal{E}\mathbf{BSK_t}$, the {\em canonical $L$-frame} is defined as $\mathcal{W}^L=\langle W^L,R^L,S^L \rangle$, where

\begin{itemize}
	
	\item $W^L$ is the set of all prime $L$-theories;
	
	\item $\Gamma R^L \Delta$ iff $\Gamma_{\Box}\subseteq\Delta$, where $\Gamma_{\Box}=\{ \varphi \mid \Box\varphi\in\Gamma\}$;
	
	\item $\Gamma S^L \Delta$ iff $\Gamma_{\blacksquare}\subseteq\Delta$, where $\Gamma_{\blacksquare}=\{ \varphi \mid \blacksquare\varphi\in\Gamma\}$;
	
	\end{itemize}

The {\em canonical $L$-model} has the form $\mathcal{M}^L=\langle \mathcal{W},v^+_L,v^-_L \rangle$, where
\[v^+_L(p)=\{ \Gamma\in W^L \mid p\in\Gamma\}\  \text{and}\ v^-_L(p)=\{ \Gamma\in W^L \mid \sim p\in\Gamma\}.\]

The abbreviations $\Diamond\varphi:=\mathord{\sim}\Box\mathord{\sim}\varphi$ and $\blacklozenge\varphi:=\mathord{\sim}\Diamond\mathord{\sim}\varphi$ easily imply that 
\[\Gamma R^L \Delta\ \text{iff}\ \Delta^{\Diamond}\subseteq\Gamma;\ \ \Gamma S^L \Delta\ \text{iff}\ \Delta^{\blacklozenge}\subseteq\Gamma,\] where $\Delta^{\Diamond}=\{ \Diamond\varphi \mid \varphi\in\Delta\}$ and $\Delta^{\blacklozenge}=\{ \blacklozenge\varphi \mid \varphi\in\Delta\}$. Further, by induction on the structure of formulas one can easily prove the canonical model lemma:

\begin{lemma}\label{canonmodel} Let $L\in\mathcal{E}\mathbf{BSK_t}$. For every prime $L$-theory $\Gamma$ and formula $\varphi$, the following equivalences hold:
	$$\mathcal{M}^L,\Gamma\models^+\varphi\ \ \mbox{iff}\ \ \varphi\in\Gamma;\ \ \mathcal{M}^L,\Gamma\models^-\varphi\ \ \mbox{iff}\ \ \sim\varphi\in\Gamma.$$
\end{lemma}



\begin{theorem}\label{BSKtcomp} Logic $\mathbf{BSK_t}$  $(\mathbf{B3SK_t})$ is strongly 4-complete (3-complete) w.r.t. the class of $\mathbf{BSK}$-frames $\langle W,R,S \rangle$ such that 
\begin{equation}
R=S^{-1}\cup \mathrm{id}_W.
\label{RS}
\end{equation}
		\end{theorem}

\begin{proof} We omit the routine correctness proof and check the completeness. Let $\Gamma\nvdash_{\mathbf{BSK_t}}\varphi$. By Lemma~\ref{extlem} there is a prime $\mathbf{BSK_t}$-theory $\Delta$ with $\Gamma\subseteq\Delta$ and $\varphi\not\in\Delta$. According to Lemma~\ref{canonmodel}, we have 
	\[\mathcal{M}^{\mathbf{BSK_t}},\Delta\models^+\psi\ \text{for all}\ \psi\in\Gamma\ \text{and}\ \mathcal{M}^{\bf BK},\Delta\not\models^+\varphi.\]
	It remains to check that the canonical $\mathbf{BSK_t}$-frame $\mathcal{W}^{\mathbf{BSK_t}}$ is a $\mathbf{BSK}$-frame, i.e., that the relation $R^{\mathbf{BSK_t}}$ is reflexive and transitive, and that 
	\begin{equation} R^{\mathbf{BSK_t}}=(S^{\mathbf{BSK_t}})^{-1}\cup \mathrm{id}_{W^{\mathbf{BSK_t}}}.
		\label{BSKtfr}
	\end{equation}
	As well as in case of normal modal logics (see \cite[Theorem~5.16]{ChagZML}) we can we can check that the axiom $\Box p\rightarrow p$ implies that $R^{\mathbf{BSK_t}}$ is reflexive, and that $\Box p\rightarrow\Box\Box p$ implies that $R^{\mathbf{BSK_t}}$ is transitive.
	
	Let us check \eqref{BSKtfr}. For brevity we will omit the upper index $(\cdot)^{\mathbf{BSK_t}}$. Assume that $R\not\subseteq S^{-1}\cup\mathrm{id}_W$. In this case there are $\Gamma,\Delta\in W$ such that $\Gamma R\Delta$, $\Gamma\neq\Delta$, and $\neg(\Delta S\Gamma)$. The latter is equivalent to $\Delta^{\blacksquare}\not\subseteq\Gamma$. Let $\blacksquare\varphi\in\Delta$ and $\varphi\not\in\Gamma$. The completeness of $\Gamma$ implies $\neg\varphi\in\Gamma$. By \eqref{incomp} and $\Gamma\neq\Delta$ there is $\psi\in\Gamma\setminus\Delta$, so $\neg\varphi\wedge\psi\in\Gamma$. The axiom $p\rightarrow\Box(p\vee\blacklozenge p)$ implies
	\[ (\neg\varphi\wedge\psi)\rightarrow\Box((\neg\varphi\wedge\psi)\vee\blacklozenge (\neg\varphi\wedge\psi))\in\Gamma. \]
	By (MP) and  $\Gamma R\Delta$ we obtain $(\neg\varphi\wedge\psi)\vee\blacklozenge (\neg\varphi\wedge\psi)\in\Delta$. Since $\psi\not\in\Delta$, we have $\neg\varphi\wedge\psi\not\in\Delta$, so $\blacklozenge (\neg\varphi\wedge\psi)\in\Delta$.
	From $\blacklozenge (\neg\varphi\wedge\psi)\rightarrow(\blacklozenge\neg\varphi\wedge\blacklozenge\psi)\in\mathbf{BSK_t}$, we conclude $\blacklozenge\neg\varphi\in\Delta$. 
	By \eqref{BKtheorems} $\neg\blacksquare\varphi\in\Delta$, which contradicts to the $\neg$-consistency of $\Delta$. We have thus proved $R\subseteq S^{-1}\cup\mathrm{id}_W$.
	
	Now we prove that $S\subseteq R^{-1}$. Let  $\Gamma,\Delta\in W$ be such that $\Gamma S\Delta$, i.e., $\Delta^{\blacklozenge}\subseteq\Gamma$.
	If $\Box\varphi\in\Delta$, then $\blacklozenge\Box\varphi\in\Gamma$. By axiom $p\rightarrow\blacksquare\Diamond p$ we have $\neg\varphi\rightarrow\blacksquare\Diamond\neg\varphi\in\Gamma$. By \eqref{BKtheorems} $\blacksquare\Diamond\neg\varphi\leftrightarrow\neg\blacklozenge\Box\varphi\in\Gamma$. Consequently, $\neg\varphi\rightarrow\neg\blacklozenge\Box\varphi\in\Gamma$, whence $\blacklozenge\Box\varphi\rightarrow\varphi\in\Gamma$. Finally, $\varphi\in\Gamma$. We have thus proved that $\Gamma S\Delta$ implies $\Delta R\Gamma$, which completes the proof of 4-completeness for $\mathbf{BSK_t}$.
	
	In case of $\mathbf{B3SK_t}$  we only have to check that the canonical $\mathbf{B3SK_t}$-model is a 3-model, i.e., that $\{p,\sim p\}\subseteq\Gamma$ does not hold for any $p\in\mathrm{Prop}$ and $\Gamma\in W^{\mathbf{B3SK_t}}$. This fact readily follows from the $\mathbf{B3SK_t}$-axiom $(p\wedge\mathord{\sim} p)\rightarrow q$.   
	
	
\end{proof} 

Now it is natural to say that $\mathcal{W}=\langle W,R,S \rangle$ is a $\mathbf{BSK_t}${\em -frame}, if $\mathcal{W}$ is a $\mathbf{BSK}$-frame and $R=S^{-1}\cup \mathrm{id}_W$.

We consider some further conditions on the accessibility relations of a $\mathbf{BSK_t}$-frame $\langle W,R,S \rangle$:

\begin{itemize}
	\item[$(1^R)$] $\forall x,y,z\in W ((xRy\ \&\ xRz\ \&\ x\neq y\ \&\ x\neq z)\Rightarrow y=z)$;
	
	\item[$(2^S)$] $\forall x,y (xSy\ \Rightarrow\ ySy)$;
	
	\item[$(3^S)$] $\forall  x,y,z\in W ((xSy\ \&\ ySz\ \Rightarrow\ y=z)$.
\end{itemize}

We  will need also $\mathcal{L}^t$-formulas:
\[ \mathbf{alt}_2:\; \Box p\vee \Box(p\rightarrow q) \vee \Box((p\wedge q)\rightarrow r), \ \ \blacksquare\cdot\mathbf{T}_{\blacksquare}:\; \blacksquare(\blacksquare p\rightarrow p).\]


\begin{proposition}\label{1t3t} Let $\mathcal{W}=\langle W,R,S \rangle$ be a $\mathbf{BSK_t}$-frame and $\epsilon\in\{ 3,4\}$. Then the following equivalences hold:
	
	\medskip
	\begin{tabular}{llll}
		
		\medskip
		$(1)$ & $\mathcal{W}\models_{\epsilon} \mathbf{alt}_2$ &  iff & $R$ satisfies $(1^R)$; \\
		
		\medskip
		$(2)$ & $\mathcal{W}\models_{\epsilon} \blacksquare\cdot\mathbf{T}_{\blacksquare}$ & iff & $S$ satisfies $(2^S)$; \\
		
		\medskip
		$(3)$ & $\mathcal{W}\models_{\epsilon} \blacksquare( p\rightarrow\blacksquare p)$ &  iff & $S$ satisfies $(3^S)$.
				
	\end{tabular}

\end{proposition}

\begin{proof} (1) It is clear that the validity of a formula which does not contain $\mathord{\sim}$ and $\blacksquare$ on a frame $\langle W,R,S \rangle$ is equivalent to the validity of this formulas on a frame $\langle W,R \rangle$ for normal modal logics. It is also known (see,e.g. \cite[Prop.~3.45]{ChagZML}) that the validity of $\mathbf{alt}_2$ is equivalent to the condition that every world has at most 2 different $R$-successors. In view of reflexivity of $R$ in $\mathbf{BSK_t}$-frames we obtain that the validity of $\mathbf{alt}_2$ in a $\mathbf{BSK_t}$-frame $\langle W,R,S \rangle$ is equivalent to the condition that every world has at most one proper $R$-successor, i.e., to $(1^R)$.

\smallskip	
(2) Again, it is known \cite[Prop.~3.30]{ChagZML} that the validity of $\blacksquare p\rightarrow p$ on $\langle W,R,S \rangle$ is equivalent to the reflexivity of $S$. The additional $\blacksquare$ in front of this formula restricts this condition to worlds that are $S$-successors. So the validity of $\blacksquare\cdot\mathbf{T}_{\blacksquare}$ is equivalent to 	$(2^S)$.

\smallskip	
(3) Assume that $\mathcal{W}=\langle W,R,S \rangle$ satisfies $(3^S)$, i.e., every  $S$-successor has no proper $S$-successors, and that $\mathcal{M}$ is a 4-model over $\mathcal{W}$. Check that $\mathcal{M}\models\blacksquare(p\rightarrow\blacksquare p)$. Let $x,y\in W$ and $xSy$. If $\mathcal{M},y\models^+ p$ and $ySz$, then $y=z$ by $(3^S)$ and $\mathcal{M},z\models^+ p$. So $\mathcal{M},y\models^+ p\rightarrow\blacksquare p$ and $\mathcal{M},x\models^+ \blacksquare(p\rightarrow\blacksquare p)$. 

Assume that $\mathcal{W}=\langle W,R,S \rangle$ is such that $xSy$, $ySz$, and $y\neq z$. Consider a 3-model $cM$ over $\mathcal{W}$ such that $v^+(p)=\{ y\}$ and $v^-(y)=\varnothing$. Then $\mathcal{M},y\models^+ p$, $\mathcal{M},y\not\models^+ \blacksquare p$, and so $\mathcal{M},x\not\models^+ \blacksquare(p\rightarrow\blacksquare p)$.
	\end{proof} 

Now we put
\[\mathbf{BSK_{t2}}:= \mathbf{BSK_t}+\{ \mathbf{alt}_2,\ \blacksquare( p\leftrightarrow\blacksquare p) \},\ \mathbf{B3SK_{t2}}:= \mathbf{BSK_{t2}}+\{ (p\wedge\mathord{\sim} p)\rightarrow q \}.\]

A $\mathbf{BSK_t}$-frame $\mathcal{W}=\langle W,R,S \rangle$ is said to be a $\mathbf{BSK_{t2}}${\em -frame} if it satisfies the conditions $(1^R)$, $(2^S)$, $(3^S)$.

\begin{theorem}\label{BSKt2comp} Logic $\mathbf{BSK_{t2}}$  $(\mathbf{B3SK_{t2}})$ is strongly 4-complete (3-complete) w.r.t. the class of $\mathbf{BSK_{t2}}$-frames.
\end{theorem}

\begin{proof} Since $\blacksquare( p\leftrightarrow\blacksquare p)$ is equivalent to the conjunction of $\blacksquare\cdot\mathbf{T}_{\blacksquare}$ and $\blacksquare( p\rightarrow\blacksquare p)$, the correctness part follows from Proposition~\ref{1t3t}.
	For the completeness part, it would be enough to check that the canonical  $\mathbf{BSK_{t2}}$-frame, which we denote for brevity as $\mathcal{W}_2=\langle W_2,R_2,S_2 \rangle$ is a $\mathbf{BSK_{t2}}$-frame. That $\mathcal{W}_2$ is a $\mathbf{BSK_{t}}$-frame can be checked as in the proof of Theorem~\ref{BSKtcomp}. The axiom $\mathbf{alt}_2$ implies that  every $\Gamma\in W_2$ has at most two $R_2$-successors. This fact and the reflexivity of $R_2$ imply the condition $(1^{R})$.
	
	Now we check that $\Gamma S_2\Delta$ implies $\Delta S_2\Delta$ for all $\Gamma,\Delta\in W_2$. Let $\Gamma S_2\Delta$, i.e., $\Gamma_{\blacksquare}\subseteq\Delta$. Assume that $\blacksquare\varphi\in\Delta$. Since $\blacksquare(\blacksquare\varphi\rightarrow\varphi)$ is a theorem of $\mathbf{BSK_{t2}}$ we have $\blacksquare(\blacksquare\varphi\rightarrow\varphi)\in\Gamma$, whence $\blacksquare\varphi\rightarrow\varphi\in\Delta$. Applying (MP) we obtain $\varphi\in\Delta$. So $\Delta_{\blacksquare}\subseteq\Delta$, and the condition $(2^{S})$ holds for $\mathcal{W}_2$.
	
	Finally, we assume that $\Gamma,\Delta,\Sigma\in W_2$ are such that $\Gamma_{\blacksquare}\subseteq\Delta$ and $\Delta_{\blacksquare}\subseteq\Sigma$. We have to check that $\Delta=\Sigma$. Let $\varphi\in\Delta$. Since $\blacksquare(\varphi\rightarrow\blacksquare\varphi)\in\Gamma$, we have $\varphi\rightarrow\blacksquare\varphi\in\Delta$. By (MP) $\blacksquare\varphi\in\Delta$, and so $\varphi\in\Sigma$. We proved $\Delta\subseteq\Sigma$. By \eqref{incomp} we conclude $\Delta=\Sigma$. Thus, the condition $(3^{S})$ holds for the canonical $\mathbf{BSK}_{t2}$-frame too.
	\end{proof} 



\section{$\blacksquare$-free fragments of $\mathbf{BSK_{t2}}$ and $\mathbf{B3SK_{t2}}$}

We define 
		\[ \mathbf{BS4_{2}}=\mathbf{BS4}+\{ \mathbf{alt}_2 \},\ \  \mathbf{B3S4_{2}}=\mathbf{BS4_{2}}+\{(p\wedge\mathord{\sim} p)\rightarrow q\}\]
	
	\begin{proposition}\label{WHTcomp}
		
		\begin{enumerate}
			
			\item Logic $\mathbf{BS4_{2}}$  $(\mathbf{B3S4_{2}})$ is strongly 4-complete (3-complete) w.r.t. the class of $\mathbf{BS4}$-frames satisfying $(1^R)$.
			
			\item Logic $\mathbf{BS4_{2}}$  $(\mathbf{B3S4_{2}})$ is strongly 4-complete (3-complete) w.r.t. the class $\{\mathcal{W}^{HT}\}$.
			
			\end{enumerate}
		
	\end{proposition}

\begin{proof} (1) As above we use \cite[Theorem~5.16]{ChagZML} to check that the canonical frames of logics $\mathbf{BS4_{2}}$ and $\mathbf{B3S4_{2}}$ are $\mathbf{BS4}$-frames satisfying $(1^R)$. According to this theorem the axiom $\Box p\rightarrow p$ implies the reflexivity of canonical frames. In a similar way, $\Box p\rightarrow \Box\Box p$ and $\mathbf{alt}_2$ imply the transitivity and the condition $(1^R)$ respectively.
	
	(2) We consider the case of $\mathbf{BS4_{2}}$. It is clear that $\mathcal{W}^{HT}$ is a $\mathbf{BS4}$-frame satisfying $(1^R)$, so $\Gamma\vdash_{\mathbf{BS4_{2}}}\varphi$ implies $\Gamma\models_{\mathcal{M}}\varphi$ for every 4-model $\mathcal{M}$ over $\mathcal{W}^{HT}$. 
	
	Let $\Gamma\nvdash_{\mathbf{BS4_{2}}}\varphi$. Then $\mathcal{M},x\models^+\Gamma$ and $\mathcal{M},x\not\models^+\varphi$ for some 4-model $\mathcal{M}$ over a $\mathbf{BS4}$-frame $\mathcal{W}=\langle W,R \rangle$ satisfying $(1^R)$. By \eqref{genmodel} we have 
	\[ \mathcal{M}^{x\uparrow},x\models^+\Gamma\ \ \text{and}\ \ \mathcal{M}^{x\uparrow},x\not\models^+\varphi,\]
	where $x\uparrow=\{ y\in W\mid xRy\}$. The condition $(1^R)$ implies that $|x\uparrow|\leq 2$, i.e., $\mathcal{W}^{x\uparrow}$ is isomorphic to $\mathcal{W}^{HT}$ or $\mathcal{W}^T$. Since $\mathcal{W}^T$ can be identified with the upper world of $\mathcal{W}^{HT}$, we obtain $\mathcal{M}',x\models^+\Gamma$ and $\mathcal{M}',x\not\models^+\varphi$ for some 4-model $\mathcal{M}'$ over $\mathcal{W}^{HT}$ and $x\in\{ h,t\}$.
	\end{proof}
	
	
	\begin{corollary}\label{conservativity}   Logic $\mathbf{BS4_{t2}}$ $(\mathbf{B3S4_{t2}})$ is a conservative extension of $\mathbf{BS4_{2}}$ $(\mathbf{BS4_{2}})$.
		\end{corollary}
	
	\begin{proof} This statement readily follows from the observation that   $\langle W,R,S \rangle$ is a $\mathbf{BSK_{t2}}$-frame iff $R=S^{-1}\cup\mathrm{id}_W$ and $\langle W,R \rangle$ is a $\mathbf{BS4}$-frame satisfying $(1^R)$.
		\end{proof}
	
	
	\begin{theorem} The logic $\mathbf{BS4_{2}}$ $(\mathbf{B3S4_{2}})$ is a modal companion of $\mathbf{N_9}$ $(\mathbf{N_5})$, i.e., for every $\varphi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ the following two equivalences hold:
		
		\medskip
		\begin{center}
		\begin{tabular}{lll}
	 $\varphi\in \mathbf{N_9}$ & iff & $T_B \varphi\in \mathbf{BS4_{2}}$, \\ 
	 
	 $\varphi\in \mathbf{N_5}$ & iff & $T_B \varphi\in \mathbf{B3S4_{2}}$.
	 
	 \end{tabular}
 \end{center}
	
\end{theorem}

\begin{proof} We consider the case of $\mathbf{N_9}$. If $T_B\varphi\not\in\mathbf{BS4_2}$, then by Item~2 of Proposition~\ref{WHTcomp} $\mathcal{M},x\not\models^+ T_B\varphi$ for some 4-model $\mathcal{M}$ over $\mathcal{W}^{HT}$ and $x\in\{ h,t\}$. By Lemma~\ref{useit} we have $\mathcal{M}',x\not\models\varphi$. Moreover, $\mathcal{M}'$ is obviously an $\mathbf{N_9}$-model. Consequently, $\varphi\not\in \mathbf{N_9}$.
	
If $\varphi\not\in\mathbf{N_9}$. Then $\mathcal{M},x\not\models^+\varphi$ for a suitable $\mathbf{N_9}$-model  and $x\in\{ h,t\}$. Obviously, $\mathcal{M}$ is a $\mathbf{BS4}$-model over $\mathcal{W}^{HT}$. Since $v^+(p)$ and $v^-(p)$ are cones for any $p\in\mathrm{Prop}$, we have
	$$x\in v^+(p)\ \Leftrightarrow\ \mathcal{M},x\models^+\Box p\ \ \mbox{and}\ \ w\in v^-(p)\ \Leftrightarrow\ \mathcal{M},w\models^+\Box\mathord{\sim} p,$$
	which implies $\mathcal{M}'=\mathcal{M}$. We have then $\mathcal{M},w\not\models^+ T_B\varphi$ by Lemma~\ref{useit}, and so $T_B\varphi\not\in{\bf BS4}$.
	
	
		\end{proof}
	
	This theorem together with Proposition~\ref{conservativity} yields
	
	\begin{corollary}
		The translation $T_B$ faithfully embeds the logic $\mathbf{N_9}$ $(\mathbf{N_5})$ into the special temporal logic $\mathbf{BSK_{t2}}$ $(\mathbf{B3SK_{t2}})$.	\end{corollary}

\section{Equilibrium theory over $\mathbf{BS4_{t2}}$}

We define a theory  $\mathbf{BKE}$ as the least set of formulas closed under the rules of $\mathbf{BS4_{t2}}$, containing the axioms of $\mathbf{BS4_{t2}}$ as well as the following formulas:


	
	\begin{equation} \Diamond(\bigwedge_{\alpha\in A}\Box\alpha \wedge \bigwedge_{\beta\in B}\Box\beta\wedge\bigwedge_{\gamma\in C}\Box\neg\gamma)\rightarrow\Diamond\blacklozenge (\bigwedge_{ \alpha\in A\cup C}\neg\alpha \wedge \bigwedge_{\beta\in B}\beta),
	\label{BKEax} \end{equation}
	
	where $A$, $B$, $C$ are disjoint finite subsets of $\mathrm{Lit}^{\mathord{\sim}}$, and $A\neq\varnothing$.
	
	It is clear that $\mathbf{BKE}$ contains all theorems of $\mathbf{BS4_{t2}}$ and is closed under the rules (NR$_{\Box}$) and (NR$_{\blacksquare}$), but  it need not be closed under (SUB). Substituting to the axioms  \eqref{BKEax} we obtain formulas which are not of the form \eqref{BKEax}. So $\mathbf{BKE}$ is namely a theory over $\mathbf{BS4_{t2}}$, not an axiomatic extension.
	
	The theory $\mathbf{B3KE}$ is defined in exactly the same way but over $\mathbf{B3S4_{t2}}$.
	
	Now we describe   models of theories $\mathbf{BKE}$ and $\mathbf{B3KE}$.  
	
	First, for a model $\mathcal{M}=\langle W,R,v^+,v^- \rangle$ and $x\in W$ we denote by $At_x$ the set of all literals true at $x$:
	\[ At_x=\{ \alpha \mid \alpha\in\mathrm{Lit}^{\mathord{\sim}}\ \text{and}\ \mathcal{M},x\models^+\alpha\}.\]
	We say that $\mathcal{M}=\langle W,R,S, v^+,v^- \rangle$ is a $\mathbf{BKE}${\em -model} if $\langle W,R,S \rangle$ is a $\mathbf{BS4_{t2}}$-frame, i.e., $R$ and $S$ are related by \eqref{RS},  $R$ is a preoder on $W$ satisfying $(1^R)$,  $S$ satisfies $(2^S)$, $(3^S)$, and for every $x\in W$ the following two conditions are satisfied:
	
	\begin{itemize} 
		
		\item[$(1^E)$] if $x$ is an {\em isolated point}, i.e., there is no $y\in W$ such that $y\neq x$, and $y R x$ or $xRy$, then $At_x=\varnothing$.
		
		\item[$(2^E)$] if $x$ is a proper $R$-successor of some  $y\in W$ and $At_x\neq\varnothing$, then for every proper subset $B\subsetneq At_x$ there is $z\in W$ such that $xSz$ and $At_z=B$.
		
		\end{itemize}
	
	$\mathbf{B3KE}${\em -models} are $\mathbf{BKE}$-models satisfying the consistency condition \eqref{cons}.
	
	\begin{theorem} Let $\varphi\in\mathrm{Form}_{\mathcal{L}^t}$. The following equivalences are true:
		
		\smallskip
		\begin{enumerate}
			\item $\varphi\in\mathbf{BKE}$ iff  $\mathcal{M}\models\varphi$ for every $\mathbf{BKE}$-model;
			
			\smallskip
			\item $\varphi\in\mathbf{B3KE}$ iff  $\mathcal{M}\models\varphi$ for every $\mathbf{B3KE}$-model;
		\end{enumerate}
	
	\end{theorem}

\begin{proof} (1) First we prove that $\varphi\in\mathbf{BKE}$ implies the truth of $\varphi$ on all $\mathbf{BKE}$-models. Since $\mathbf{BKE}$-models are based on $\mathbf{BS4_{t2}}$-frames, Theorem~\ref{BSKt2comp} implies that it would be enough to check the truth of axioms \eqref{BKEax} on $\mathbf{BKE}$-models. Let $\mathcal{M}=\langle W,R,S, v^+,v^- \rangle$ be a $\mathbf{BKE}$-model and $x\in W$.  Assume that 
	\[ \mathcal{M},x\models^+ \Diamond(\bigwedge_{\alpha\in A}\Box\alpha \wedge \bigwedge_{\beta\in B}\Box\beta\wedge\bigwedge_{\gamma\in C}\Box\neg\gamma),\]
	where $A$, $B$, $C$ are disjoint finite subsets of $\mathrm{Lit}^{\mathord{\sim}}$, and $A\neq\varnothing$.
	Then there is $y\in W$ such that $xRy$ and 
	\[ \mathcal{M},y\models^+ \bigwedge_{\alpha\in A}\Box\alpha \wedge \bigwedge_{\beta\in B}\Box\beta\wedge\bigwedge_{\gamma\in C}\Box\neg\gamma.\]
	Reflexivity of $R$ implies $A\cup B\subseteq At_y$. Since $\mathcal{M},y\models^+\neg\alpha$ is equivalent to $\mathcal{M},y\not\models^+\alpha$, we have $C\cap At_y=\varnothing$. If $x$ has no proper $R$-successors, then  $x=y$. In this case $A\neq\varnothing$  and $(1^E)$ imply that there is $z$ such that $x\neq z$ and $zRx$. By $(2^E)$ there is an $S$-successor $u$ of $x$ such that $At_u=B$. So  we have $\mathcal{M},x\models^+ \blacklozenge (\bigwedge_{ \alpha\in A\cup C}\neg\alpha \wedge \bigwedge_{\beta\in B}\beta)$ and
	\begin{equation}  \mathcal{M},x\models^+ \Diamond\blacklozenge (\bigwedge_{ \alpha\in A\cup C}\neg\alpha \wedge \bigwedge_{\beta\in B}\beta).
		\label{consequent}
		\end{equation}
	Otherwise we can assume that $y$ is a proper $R$-successor of $x$. From $(2^E)$ we again obtain that $\blacklozenge (\bigwedge_{ \alpha\in A\cup C}\neg\alpha \wedge \bigwedge_{\beta\in B}\beta)$ is verified at $y$, and \eqref{consequent} as a consequence.
	
	\smallskip
	To prove the inverse implication  we define the canonical frame $\mathcal{W}^E$ for the theory $\mathbf{BKE}$ in exactly the same way as it was done earlier for axiomatic extensions of $\mathbf{BSK_t}$. We put $\mathcal{W}^E=\langle W^E,R^E,S^E \rangle$, where $W^E$ is the set of all prime $\mathbf{BSK_{t2}}$-theories containing $\mathbf{BKE}$,
	\[ \Gamma R^E \Delta\ \  \text{iff}\ \Gamma_{\Box}\subseteq\Delta,\ \ \ \Gamma S^E \Delta\ \ \text{iff}\ \ \Gamma_{\blacksquare}\subseteq\Delta.\] 
	
	If $\varphi\in\mathrm{Form}_{\mathcal{L}^t}$, we denote the set of its propositional variables as $\mathrm{var}(\varphi)$ and put
	\[ \mathrm{Lit}_{\varphi}=\{ p,\mathord{\sim} p \mid p\in\mathrm{var}(\varphi)\}.\] 
	For $\varphi\not\in\mathbf{BKE}$ we define a kind of canonical model 
	$\mathcal{M}^E_{\varphi}=\langle \mathcal{W}^E, v^+_E,v^-_E \rangle$ putting
	\[v^+_{\varphi}(p)=\{ \Gamma\in W^L \mid p\in\Gamma\cap\mathrm{var}(\varphi)\},\ \ v^-_{\varphi}(p)=\{ \Gamma\in W^L \mid \mathord{\sim} p\in\Gamma\cap\mathrm{Lit}_{\varphi}\}.\]
	The analog of canonical model lemma (Lemma~\ref{canonmodel}) can also be proved for $\mathcal{M}^E_{\varphi}$ by induction on the structure of formulas. For every $\psi\in \mathrm{Form}_{\mathcal{L}^t}$ and $\Gamma\in W^E$ we have 
		\begin{equation}
		\mathcal{M}^E_{\varphi},\Gamma\models^+\psi\ \ \mbox{iff}\ \ \psi\in\Gamma;\ \ \mathcal{M}^E_{\varphi},\Gamma\models^-\psi\ \ \mbox{iff}\ \ \sim\psi\in\Gamma.
		\label{canmodME}
			\end{equation}
	
	  That $\mathcal{W}^E$ is a $\mathbf{BSK_{t2}}$-frame can be proved in exactly the same way as in Theorem~\ref{BSKt2comp}. Let us check that $\mathcal{M}^E_{\varphi}$ is a $\mathbf{BKE}$-model. 
	  
	 We take some $\Gamma\in W^E$ that has no proper $R^E$-successors. If $\Gamma\cap\mathrm{Lit}_{\varphi}\neq\varnothing$, we choose finite disjoint $A$, $B$, $C\subseteq\mathrm{Lit}_{\varphi}$ such that 
	  \[ A\cup B=\Gamma\cap\mathrm{Lit}_{\varphi},\ \ A\neq\varnothing, \ \ C=\mathrm{Lit}_{\varphi}\setminus \Gamma.\]
	  Then $\mathcal{M}^E_{\varphi},\Gamma\models^+\bigwedge_{\alpha\in A}\alpha\wedge\bigwedge_{\beta\in B}\beta\wedge\bigwedge_{\gamma\in C}\neg\gamma$. Since $R^E$ is reflexive and
	$\Gamma$ has no other 	$R^E$-successors, we have 
	\[\mathcal{M}^E_{\varphi},\Gamma\models^+\bigwedge_{\alpha\in A}\Box\alpha\wedge\bigwedge_{\beta\in B}\Box\beta\wedge\bigwedge_{\gamma\in C}\Box\neg\gamma.\] 
	The reflexivity of $R^E$ yields $\mathcal{M}^E_{\varphi},\Gamma\models^+\Diamond(\bigwedge_{\alpha\in A}\Box\alpha\wedge\bigwedge_{\beta\in B}\Box\beta\wedge\bigwedge_{\gamma\in C}\Box\neg\gamma)$. Finally, by \eqref{canmodME} we obtain $\Diamond(\bigwedge_{\alpha\in A}\Box\alpha\wedge\bigwedge_{\beta\in B}\Box\beta\wedge\bigwedge_{\gamma\in C}\Box\neg\gamma)\in\Gamma$. Since $\Gamma$ contains all $\mathbf{BKE}$-axioms, we have $\Diamond\blacklozenge (\bigwedge_{ \alpha\in A\cup C}\neg\alpha \wedge \bigwedge_{\beta\in B}\beta)\in\Gamma$, which is equivalent by~\eqref{canmodME} to
	\begin{equation}\mathcal{M}^E_{\varphi},\Gamma\models^+\Diamond\blacklozenge (\bigwedge_{ \alpha\in A\cup C}\neg\alpha \wedge \bigwedge_{\beta\in B}\beta).
		\label{DbD}
		\end{equation}
	The lack of proper $R^E$-successors implies $\mathcal{M}^E_{\varphi},\Gamma\models^+\blacklozenge (\bigwedge_{ \alpha\in A\cup C}\neg\alpha \wedge \bigwedge_{\beta\in B}\beta)$. This fact together with $A\cup B\cup C=\mathrm{Lit}_{\varphi}$ implies in turn  that $\Gamma$ has an $S^E$-successor $\Delta$ with $At_{\Delta}=B$.
	Since $At_{\Gamma}\neq At_{\Delta}$, $\Delta$ is a proper $S^E$-successor or, equivalently, $R^E$-predecessor of $\Gamma$. We have thus proved that $At_{\Gamma}\neq\varnothing$ implies that $\Gamma$ is not an isolated point. So $(1^E)$ holds for $\mathcal{M}^E_{\varphi}$.
	
	Let $\Gamma,\Delta\in W^E$ be such that $\Gamma R^E\Delta$, $\Gamma\neq\Delta$, $\Delta\cap\mathrm{Lit}_{\varphi}\neq\varnothing$, and $B\subsetneq\Delta\cap\mathrm{Lit}_{\varphi}$. In this case $\Delta$ has no proper $R^E$-successors, and arguing as above we obtain that $\Delta$ has an $S^E$-successor $\Sigma$ with $At_{\Sigma}=B$. Thus, $\mathcal{M}^E_{\varphi}$ satisfies $(2^E)$ too. 
	
	We have proved that $\mathcal{M}^E_{\varphi}$ is a $\mathbf{BKE}$-model. Since $\varphi\not\in\mathbf{BKE}$, by extension lemma there is $\Gamma\in W^E$ such that $\varphi\not\in\Gamma$, whence $\mathcal{M}^E_{\varphi},\Gamma\not\models^+\varphi$.
	
	(2) That $\mathbf{BKE}$-axioms are true on $\mathbf{B3KE}$-models readily follows from the previous item. It is obvious too that a canonical model \[\mathcal{M}^{3E}_{\varphi}=\langle W^{3E}, R^{3E}, S^{3E}, v^+_{3E}, v^-_{3E} \rangle\]  defined as above, but with $W^{3E}$ consisting of all prime theories extending $\mathbf{B3KE}$, is a 3-model.                                                                                                    

\end{proof}
	
	
	\begin{theorem} Let $\varphi, \psi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$. Then 
		\[ \varphi\mathbin{|\kern -.47em\thicksim}^9_{el}\psi\ \ \text{iff}\ \ (T_B\varphi\wedge\blacksquare\neg T_B\varphi)\rightarrow T_B\psi\in\mathbf{BKE}.\]
		\[ \varphi\mathbin{|\kern -.47em\thicksim}^5_{el}\psi\ \ \text{iff}\ \ (T_B\varphi\wedge\blacksquare\neg T_B\varphi)\rightarrow T_B\psi\in\mathbf{B3KE}.\]
	
	\end{theorem}

\begin{proof} We consider only the case of paraconsistent equilibrium consequence. Assume that $\varphi\mathbin{|\kern -.47em\thicksim\kern-.9em{/}}^9_{el}\psi$, i.e., there is an equilibrium model $\langle {\mathbf T},{\mathbf T} \rangle$ of $\varphi$ such that 
	$\langle {\mathbf T},{\mathbf T} \rangle\not\models\psi$.
Recall that an equilibrium model of $\varphi$ is a total $\mathbf{N_9}$-model $\langle {\mathbf T},{\mathbf T} \rangle$ such that
\[ \langle {\mathbf T},{\mathbf T} \rangle\models\varphi\ \ \text{and}\ \ \langle {\mathbf H},{\mathbf T} \rangle\not\models\varphi\ \ \text{for all}\ \ {\mathbf H}\subsetneq{\mathbf T}.\] 

Let us consider a $\mathbf{BKE}$-model $\mathcal{M}^{{\mathbf T}}=\langle W^{{\mathbf T}},R^{{\mathbf T}},S^{{\mathbf T}},v^+_{{\mathbf T}},v^-_{{\mathbf T}} \rangle$, where
\begin{itemize}
	\item  $W^{{\mathbf T}}=\{ {\mathbf H} \mid {\mathbf H}\subseteq{\mathbf T}\}$;
	\item  $R^{{\mathbf T}}=\{ ({\mathbf H},{\mathbf H})\mid {\mathbf H}\in W^{{\mathbf T}}\}\cup \{ ({\mathbf H},{\mathbf T}) \mid {\mathbf H}\subseteq{\mathbf T}\}$;
	\item $S^{{\mathbf T}}=\{ ({\mathbf H},{\mathbf H})\mid {\mathbf H}\in W^{{\mathbf T}}\setminus\{{\mathbf T}\}\} \cup \{ ({\mathbf T},{\mathbf H}) \mid {\mathbf H}\subsetneq{\mathbf T}\}$;
	\item $v^+_{{\mathbf T}}(p)=\{ {\mathbf H} \mid p\in{\mathbf H}\}$, $v^-_{{\mathbf T}}(p)=\{ {\mathbf H} \mid \mathord{\sim} p\in{\mathbf H}\}$, $p\in\mathrm{Prop}$.
	
\end{itemize}
It is clear that $R^{{\mathbf T}}$ is a partial order of depth $2$ with the greatest element ${\mathbf T}$, $S^{{\mathbf T}}$ satisfies \eqref{RS} and has the only irreflexive point ${\mathbf T}$. So $\langle W^{{\mathbf T}},R^{{\mathbf T}},S^{{\mathbf T}} \rangle$ is a $\mathbf{BSK_{t2}}$-frame. The valuations $v^+_{{\mathbf T}}$, $v^-_{{\mathbf T}}$ are defined so that $At_{{\mathbf H}}={\mathbf H}$ for all ${\mathbf H}\in W^{{\mathbf T}}$.

Further, for every ${\mathbf H}\in W^{{\mathbf T}}$ with ${\mathbf H}\neq{\mathbf T}$, the generated submodel $\mathcal{M}^{{\mathbf H}\uparrow}:=(\mathcal{M}^{{\mathbf T}})^{{\mathbf H}\uparrow}$ is of the form $\langle {\mathbf H},{\mathbf T} \rangle$. Moreover, since ${\mathbf H}\subseteq{\mathbf T}$, we can consider $\langle {\mathbf H},{\mathbf T} \rangle$ as an $\mathbf{N_9}$-model, i.e. $(\mathcal{M}^{{\mathbf H}\uparrow})'=\mathcal{M}^{{\mathbf H}\uparrow}$. If ${\mathbf H}={\mathbf T}$, then $\mathcal{M}^{{\mathbf T}\uparrow}={\mathbf T}$ and it can be identified with the total model $\langle {\mathbf T},{\mathbf T} \rangle$. By Lemma~\ref{useit} and \eqref{genmodel} we have for every $\chi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ and ${\mathbf H}\in W^{{\mathbf T}}$,

\begin{equation} \mathcal{M}^{{\mathbf T}},{\mathbf H}\models^+ T_B\chi\ \ \text{iff}\ \ \langle {\mathbf H},{\mathbf T} \rangle\models \chi. 
	\label{TBHT}
	\end{equation}

From this observation we obtain
\[ \mathcal{M}^{{\mathbf T}},{\mathbf T}\models^+ T_B\varphi\ \ \text{and}\ \ \mathcal{M}^{{\mathbf T}},{\mathbf H}\models^+ \neg T_B\varphi\ \ \text{for}\ \ {\mathbf H}\subsetneq{\mathbf T}.\]
We also have  $\mathcal{M}^{{\mathbf T}},{\mathbf T}\models^+ \blacksquare\neg T_B\varphi$, since $\{{\mathbf H} \mid {\mathbf H}\subsetneq{\mathbf T}\}$ is the set of all $S^{{\mathbf T}}$-successors of ${\mathbf T}$. From $\langle {\mathbf T},{\mathbf T} \rangle\not\models\psi$ and \eqref{TBHT} we have $\mathcal{M}^{{\mathbf T}},{\mathbf T}\not\models^+ T_B\psi$, whence
\[ \mathcal{M}^{{\mathbf T}},{\mathbf T}\not\models^+(T_B\varphi\wedge\blacksquare\neg T_B\varphi)\rightarrow T_B\psi.\]
We have thus proved the right-to-left implication.

Let us assume now that $(T_B\varphi\wedge\blacksquare\neg T_B\varphi)\rightarrow T_B\psi\not\in\mathbf{BKE}$, i.e., that there are a $\mathbf{BKE}$-model $\mathcal{M}=\langle W,R,S,v^+,v^- \rangle$ and $x\in W$ such that
\[ \mathcal{M},x\not\models^+(T_B\varphi\wedge\blacksquare\neg T_B\varphi)\rightarrow T_B\psi.\]
Then we have
\[ \mathcal{M},x\models^+ T_B\varphi,\ \ \mathcal{M},y\not\models^+ T_B\varphi \ \text{whenever}\ xSy, \ \ \mathcal{M},x\not\models^+ T_B\psi.\]
If there is $y$ such that $xRy$ and $x\neq y$, then $ySx$  by \eqref{RS}, and $xSx$ by $(2^S)$. So we have simultaneously $\mathcal{M},x\models^+ T_B\varphi$ and $\mathcal{M},x\not\models^+ T_B\varphi$. Consequently, $x$ has no proper $R$-successors.  Assume that $At_x=\varnothing$. By Lemma~\ref{useit} and \eqref{genmodel} we have $\varnothing\models\varphi$ and $\varnothing\not\models\psi$. Thus, $\langle \varnothing,\varnothing \rangle$ is an equilibrium model of $\varphi$ that refutes  $\varphi\mathbin{|\kern -.47em\thicksim}^9_{el}\psi$.

In case $At_x\neq\varnothing$ by $(1^E)$ we obtain that $x$ is not an isolated point. Since $x$ has no proper $R$-successors there is $y$ such that $y\neq x$ and $yRx$. Take some ${\mathbf H}\subsetneq At_x$. By $(2^E)$ there is $z$ such that $At_z={\mathbf H}$ and $xSz$. Applying again Lemma~\ref{useit} and \eqref{genmodel} we obtain $\langle {\mathbf H}, At_x \rangle\not\models\varphi$. Thus, $\langle At_x,At_x \rangle$ is an equilibrium model of $\varphi$ that refutes $\psi$. So, $\varphi\mathbin{|\kern -.47em\thicksim\kern-.9em{/}}^9_{el}\psi$.

	\end{proof}

	
	
	

	
	
	
	
	\bigskip
	\begin{thebibliography}{1} % Ссылки на литературу приводятся только на английском языке (даже если у источника нет англоязычной версии).
		
		\bibitem{ADP04}
		J.~Alcantara, C.~Demasio, L.M.~Pereira, {\em A Declarative Characterisation of Disjunctive Paraconsistent Answer Sets}, R.~L\'{o}pez de M\'{a}ntaras, L.~Saitta (eds.), Proc. of ECAI 2004, IOS Press, 2004, 951-957. 
		
		\bibitem{Belnap77} 
		N.~Belnap, \href{https://link.springer.com/chapter/10.1007/978-94-010-1161-7_2}{\em A useful four-valued logic}, J.\,M.~Dunn, G.~Epstein (eds), Modern Uses of Multiple-Valued Logic, Dordrecht, D.\ Reidel, 1977, 5--37.
		
		\bibitem{ChagZML}
		A.~Chagrov, M.~Zakhariaschev, \href{https://global.oup.com/academic/product/modal-logic-9780198537793?cc=ru&lang=en&}{\em Modal Logic}, Oxford, Clarendon Press, 1997.
				
		%\bibitem{Dietr94}
		%J.~Dietrich, {\em Deductive bases of nonmonotonic inference operations. Technical report}, NTZReport, %Universit\"{a}t Leipzig, 1994.
		
		\bibitem{Dunn76}
		J.M.~Dunn, \href{https://www.jstor.org/stable/4319017}{\em  Intuitive semantics for first-degree entailments and `coup\-led trees'},  Philosophical Studies, \textbf{29} (1976), 149--168.
		
		\bibitem{FdCHSu2014}
		L.~Fari\~{n}as del Cerro, A.~Herzig, E.I.~Su, \href{https://www.sciencedirect.com/science/article/pii/S1570868314000172}{\em Capturing equilibrium models in modal logic}, Journal of Applied Logic, \textbf{12}:2 (2014), 192--207.
		
			\bibitem{Font16}
		J.~Font, \href{https://www.collegepublications.co.uk/logic/mlf/?00026}{\em Abstract Algebraic Logic: An Introductory Textbook}, College Publications, 2016.
		
		\bibitem{GL88}
		M.~Gelfond, V.~Lifschitz, {\em The stable model semantics for logic programming}, Proc. of ICLP'88, The {MIT} Press, 1988, 1070--1080.
				
		\bibitem{GL91}
		M.~Gelfond, V.~Lifschitz, \href{https://doi.org/10.1007/BF03037169}{\em Classical negation in logic programs and disjunctive databases},
		New Generation Computing, \textbf{9}  (1991), 365--385.
		
		\bibitem{Goedel1933}
		K.~G\"{o}del, {\em Eine Interpretation des intuitionistischen Aussagenkalk\"{u}ls}, Ergebnisse eines mathematischen Kolloquiums, \textbf{4} (1933), 39--40.
		
		\bibitem{LPV2001}
		V.~Lifschitz, D.~Pearce, A.~Valverde,  \href{https://dl.acm.org/doi/10.1145/383779.383783}{\em Strongly equivalent logic programs}, ACM Transactions on Computational Logic, \textbf{2}:2 (2001), 526--541.
		
		\bibitem{Lo72}
		E.G.K.~L\'{o}pez-Escobar, \href{https://www.sciencedirect.com/science/article/pii/1385725872900534}{\em Refutability and Elementary Number Theory}, Indagationes Mathematicae, \textbf{34} (1972), 362--374.
		
		\bibitem{MOd2013}
		N.V.~Mayatski, S.P.~Odintsov, \href{https://www.tandfonline.com/doi/abs/10.1080/11663081.2013.798971}{\em On deductive bases for paraconsistent answer set semantics}, Journal of Applied Non-Classical Logic, \textbf{23}:1--2 (2013), 131--146.
		
		\bibitem{Ne49}
		D.~Nelson, \href{https://www.jstor.org/stable/2268973}{\em Constructible falsity}, Journal of Symbolic Logic, \textbf{14} (1949):16--26.
		
		\bibitem{Od05}
		S.P.~Odintsov, \href{https://doi.org/10.1007/s11225-005-8472-9}{\em The class of extensions of Nelson's paraconsistent logic}, Studia Logica, \textbf{80} (2005), 291--320.
		
		\bibitem{Od2008}
		S.P.~Odintsov \href{https://link.springer.com/book/10.1007/978-1-4020-6867-6}{\em Constructive Negations and Paraconsistency}, Trends in Logic, \textbf{26}, Dordrecht, Springer, 2008.
		
		\bibitem{OdPe05}
		S.~Odintsov, D.~Pearce, (2005). \href{https://doi.org/10.1007/11546207_27} {\em Routley Semantics for Answer Sets}, C.~Baral, G.~Greco, N.~Leone, G.~Terracina  (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2005. Lecture Notes in Computer Science, vol 3662. Springer, Berlin, Heidelberg, 2005, 343--355. 
		
		\bibitem{OdWans2010} 
		S.P.~Odintsov, H.~Wansing, \href{https://www.tandfonline.com/doi/abs/10.3166/jancl.20.279-301}{\em Modal logics with Belnapian truth values}, Journal of Applied Non-Classical Logics, \textbf{20}:3 (2010), 279--301.
		
		\bibitem{OdWans2017}
		S.P.~Odintsov, H.~Wansing, \href{https://link.springer.com/article/10.1007/s11225-017-9753-9}{\em Disentangling FDE-Based Paraconsistent Modal Logics}, Studia Logica, \textbf{105}:1 (2017), 1221–1254.
		
		%\bibitem{Pe93}
		%D.~Pearce, \href{https://ieeexplore.ieee.org/document/6278659}{\em Answer Sets and Constructive Logic. %Part II: extended logic programs and related nonmonotonic formalisms},  L. M. Periera, A. Nerode (eds), %Logic Programming and Non-monotonic Reasoning,  MIT press, 1993, 457--475.
		
		\bibitem{Pe97} D.~Pearce, \href{https://doi.org/10.1007/BFb0023801}{\it A new logical characterization of stable models and answer sets},
		Proceedings of Non-Monotonic Extensions of Logic Programming 1996, LNCS 1216, Springer, 1997,  57--70. 
		
		\bibitem{Ro74}
		R.~Routley. \href{https://doi.org/10.1007/BF02123283}{\em Semantical Analyses of Propositional Systems of Fitch and Nelson}, Studia Logica, \textbf{33}:3 (1974): 283-298.
		
		\bibitem{SI95} C.~Sakama, K.~Inoue, \href{https://doi.org/10.1093/logcom/5.3.265}{\em Paraconsistent Stable Semantics for Extended Disjunctive Programs},  Journal of Logic and Computation,  \textbf{5} (1995), 265--285.
		
		\bibitem{Th69}
		R.H.~Thomason, \href{https://onlinelibrary.wiley.com/doi/10.1002/malq.19690151602}{\em A Semantical Study of Constructible Falsity}, Zeitschrift f\"{u}r Mathematische Logik und Grundlagen der Mathematik, \textbf{15} (1969), 247--257.
		
		\bibitem{VishOd2025}
		A.G.~Vishneva, S.P.~Odintsov \href{https://doi.org/10.4213/mzm14305}{\em Modal companions of special extensions of constructive Nelson's logic (in russian)}, Matematicheskie Zametki, \textbf{117}:3 (2025), 344-364.
		
		\bibitem{Vo52a}
		N.N.~Vorob'ev, {\em A constructive propositional calculus with strong negation (in russian)}, Doklady Akademii Nauk SSSR, \textbf{85} (1952):465--468.
		
		\bibitem{Vo52b}
		N.N.~Vorob'ev, {\em  The problem of deducibility in constructive propositional calculus with strong negation (in russian)}, Doklady Akademii Nauk SSSR, {\bf 85} (1952):689--692.
					
	\end{thebibliography}
\end{document}

