\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{graphicx}
\usepackage{xcolor}
\usepackage{amsmath,amsthm,amsfonts,bbm,proof,mathtools,amssymb,relsize}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{marginnote}
\usepackage{enumerate}
\usepackage{graphicx}
\usepackage[all]{xy}
\usepackage{multicol}
\usepackage{amssymb, color}
\usepackage{epstopdf, soul}
\usepackage{bussproofs}
\usepackage{tcolorbox}
\usepackage{MnSymbol}



\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} %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}














 














\newcommand{\tuple}[1]{\langle #1 \rangle}











\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[Definability in logics with strong negation]{\large Definability in logics with strong negation}
	
	
	\author[S.P. ODINTSOV]{{\bf S.P. Odintsov}\protect\orcidicon{0000-0003-3115-1293}}
	
	
	
	\address{Sergei Pavlovich Odintsov
		\newline\hphantom{iii} Sobolev Institute of Mathematics,
		\newline\hphantom{iii} pr. Koptyuga, 4,
		\newline\hphantom{iii} 630090, Novosibirsk, Russia}%
	\email{odintsov@math.nsc.ru}%
	
	
	\thanks{\sc Odintsov S.P.,
		Definability in logics with strong negation}
	\thanks{\copyright \ 2026 Odintsov S.P.}
	\thanks{\rm  The research presented in this paper has been carried out within the framework of State Contracts of the Sobolev Institute of Mathematics (Project FWNF-2026-0032)}
	\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:} In this paper, we study the logics with strong negation from the point of view of abstract algebraic logic.
			We define the notion of implicative logic with strong negation (sn-implicative logic), which can be considered as an abstract notion of a logic with strong negation, and the notion of weak  definitional equivalence  of logics,  based on  that of weakly structural translation. We also distinguish among sn-implicative logics the subclass of so called bl-logics and prove that for bl-logics weak definitional equivalence  implies definitional equivalence. As examples of weakly definitionally equivalent logics we consider  Nelson's constructive logic $\mathsf{N4}^{\bot}$ and Wansing's connexive logic $\mathsf{C}^{\bot}$. We also prove that sixteen expansions of Heyting-Brouwer logic {\sf HB} via strong negation suggested by H.~Wansing in \cite{Wansing08} are weakly definitionally equivalent. Finally, we prove that all implicative logics satisfying the deduction theorem possess the Beth property {\bf B2} and that all explosive sn-implicative logics satisfying the deduction theorem possess an analog of Beth property adopted to the language with strong negation.   \medskip
			
			\noindent{\bf Keywords:}  implicative logic, implicative logic with strong negation, bl-logic, weakly structural translation, weak definitional equivalence, strong negation, Beth property.
		\end{quote}
	}
	
	\bigskip
	The name ``strong negation'' was suggested by D.~Nelson in his seminal paper \cite{Nelson49}, where he suggested a system of constructive logic based on constructive procedures of verification and falsification of formulas, which are not reducible one to the other. The strong negation connective introduced by Nelson works as a flip-flop between two procedures. To verify the strong negation of a formula we have to falsify this formula and vise versa. This situation is typical for numerous logics with  strong negation, whose relational semantics is given via frames with two different support of truth ($\models^+$) and support of falsity ($\models^-$) relations. As a result the strong negation connective lacks congruence properties on the formula algebra, the Tarski congruence of a logic with strong negation is different from the mutual inferability of formulas, the logic is not closed under the replacement rule, etc. Due to this reason there is a sense to weaken some standard logical notions, e.g., the notion of structural translation used to embed one logic into the other and to establish the definitional equivalence of logics. In \cite{OdWans2010}, the paraconsistent Nelson's logic $\mathsf{N4}^{\bot}$ was embedded into $\mathsf{BS4}$, the Belnapian version of normal modal logic $\mathsf{S4}$, via a translation that is not structural with respect to the strong negation. The expansions of Heyting-Brouwer logics via strong negation was embedded in \cite{OdWans2010} into a temporal version of $\mathsf{BS4}$ via non-structural translations. In \cite{OdWans2017}, the notion of weak definitional equivalence  based on non-structural translations was introduced, and weak definitional equivalence of different Belnapian modal logics was established. Finally, in \cite{OdSkWans19} it was noticed that if the language of logics is rich enough to define bilattice connectives, then the weak definitional equivalence of logics implies that these logics are definitionally equivalent in the ordinary sense.
	
	In this paper, we look at the mentioned results from the point of view of abstract algebraic logic.
	The paper is structured as follows. Section~\ref{prelim}  recalls basic notions and results from algebraic logic. Here we define a logic as a structural Tarski consequence relation, recall the notion of algebraizability in the sense of Blok and Pigozzi \cite{BlokPigozzi}, define the class of implicative logics due to Rasiowa \cite{Rasiowa} and recall that implicative logics admit the most standard form of algebraization, which is explained by the fact that the mutual inferability of formulas in such logics form a congruence on the formula algebra. Finally, we recall the notion of definitional equivalence of logics.  In Section~2 we define the notion of an implicative logic with strong negation (sn-implicative logic), which can be considered as an abstract notion of a logic with strong negation. In sn-implicative logics, the mutual inferability of formulas is not a congruence on a formula algebra. Further, we define the notion of a weak  definitional equivalence  of logics, which is based on  that of weakly structural translation. We also distinguish among sn-implicative logics the subclass of so called $bl$-logics and prove that for $bl$-logics weak definitional equivalence  imply definitional equivalence. Section~3 contains examples of weakly definitionally equivalent logics. We prove that Nelson's constructive logic $\mathsf{N4}^{\bot}$ and Wansing's connexive logic $\mathsf{C}^{\bot}$ are weakly  definitionally equivalent. We also prove that sixteen expansions of Heyting-Brouwer logic {\sf HB} via strong negation suggested by H.~Wansing in \cite{Wansing08} are weakly definitionally equivalent. Moreover, we prove that adding to the languages of these logics constants corresponding to Belnapian truth values $Both$ and $Neither$ turns all these logics to $bl$-logics and all established weak definitional equivalences to definitional equivalences. Section~4 is devoted to the Beth property {\bf B2}. We prove that all implicative logics satisfying the deduction theorem possess {\bf B2} and that all explosive sn-implicative logics satisfying the deduction theorem possess an analog of Beth property adopted to the language with strong negation. Finally, in Section~5 we formulate a series of open problems.
	
	
	
	\section{Preliminaries}\label{prelim}
	In the present section we recall some notions and results from algebraic logic. We will assume throughout that the reader is familiar with elementary notions of universal algebra. For details the reader may consult \cite{burris1981course,Font16}. 
	
	As usual we define a {\em propositional language} $\mathcal{L}\ =\ \left\{ f_1, \ldots, f_k \right\}$  as a finite set of logical connectives.  Fix a countable set $\mathrm{Prop}$ of  propositional variables and consider the absolutely free algebra $\mathcal{F}or_{\mathcal{L}}:=\langle \mathrm{Form}_{\mathcal{L}}; f_1,\ldots,f_k\rangle$ {(the formula algebra)} of language $\mathcal{L}$  with generators $\mathrm{Prop}$. Elements of its universe $\mathrm{Form}_{\mathcal{L}}$ are formulas of the language $\mathcal{L}$ ($\mathcal{L}$-formulas). 
	
	By a {\em substitution} we mean an endomorphism  $s:\mathcal{F} or_{\mathcal{L}}\rightarrow\mathcal{F} or_{\mathcal{L}}$ of the formula algebra.  A formula $\psi$ is said to be a {\em partial case} of $\varphi$ if there is a substitution $s$ such that $\psi=s\varphi$.
	
	A \emph{ (Tarski) consequence relation} over $\mathcal{L}$ is a relation $\vdash$ between sets of $\mathcal{L}$-formulas and $\mathcal{L}$-formulas such that for all $\Gamma,\Delta\subseteq\mathrm{Form}_{\mathcal{L}}$ and $\varphi\in \mathrm{Form}_{\mathcal{L}}$, the following holds
	
	\begin{enumerate}
		\item[R.] (Reflexivity) If $\varphi \in \Gamma$, then $\Gamma \vdash \varphi$
		\item[M.] (Monotonicity) If $\Gamma \vdash \varphi$ and $ \Gamma\subseteq \Delta$, then $\Delta \vdash \varphi$
		\item[C.]  (Cut, transitivity) If $\Gamma \vdash \varphi$ and $\Delta \vdash \psi$ for all $\psi \in \Gamma$, then $\Delta \vdash \varphi$.
	\end{enumerate}
	
	A consequence relation $\vdash$ is said to be {\em structural} if for every substitution $s$ and $\Gamma\cup\{\varphi\}\subseteq\mathrm{Form}_{\mathcal{L}}$, 
	\[
	\Gamma \vdash \varphi \text{ implies }s \Gamma \vdash s \varphi,
	\]
	where $s\Gamma=\{ s\psi \mid \psi\in\Gamma\}$. 
	
	Following \cite{Font16} we say that a {\em logic} is a pair $\mathsf{L}=\langle\mathcal{L},\vdash_\mathsf{L}\rangle$, where $\mathcal{L}$ is a propositional language, and $\vdash_{\mathsf{L}}$ is a structural consequence relation over $\mathcal{L}$. 
	%In what follows we write $\vdash$ instead of $\vdash_{\mathsf{L}}$ if the reference to $\mathsf{L}$ is clear %from the context. 
	For a logic $\mathsf{L}$, we put $\mathrm{Thm}(\mathsf{L})=\{ \varphi \mid \varnothing\vdash_\mathsf{L}\varphi\}$. Elements of $\mathrm{Thm}(\mathsf{L})$ are called {\em theorems of} $\mathsf{L}$ ($\mathsf{L}${\em -theorems}).
	
	The {\em Frege relation} of $\mathsf{L}$ is the following binary relation on $\mathrm{Form}_{\mathcal{L}}$:
	\[\Lambda\mathsf{L}=\{ (\varphi,\psi) \mid \varphi,\psi\in\mathrm{Form}_{\mathcal{L}},\ \{\varphi\}\vdash_{\mathsf{L}}\psi\ \text{and}\ \{\psi\}\vdash_{\mathsf{L}}\varphi\}.\]
	Obviously, $\Lambda\mathsf{L}$ is an equivalence, but it is not necessarily a congruence on the formula algebra $\mathcal{F} or_{\mathcal{L}}$.
	
	It is known \cite[Sec.~5.3]{Font16} that for every logic $\mathsf{L}$ there is  the largest congruence  $\tilde{\Omega}(\mathsf{L})$ on the formula algebra $\mathcal{F}or_{\mathcal{L}}$ contained in $\Lambda\mathsf{L}$. We call $\tilde{\Omega}(\mathsf{L})$  the {\em Tarski congruence}  of  $\mathsf{L}$.
	
	
	
	%A subset $F\subseteq A$ is said to be a \emph{logical filter} of $\mathbf{A}$ w.r.t. $\mathsf{L}$ (an %$\mathsf{L}$-filter, for short) if   for any $\Gamma\cup\{\varphi\}\subseteq \mathrm{Form}_{\mathcal{L}}$ and any %$\cA$-valuation $v$,
	%$\[\Gamma\vdash_{\mathsf{L}}\varphi\ \text{and}\ v(\Gamma)\subseteq F\ \text{imply}\ v(\varphi)\in F.\]
	%We will denote the set of $\mathsf{L}$-filters over $\mathbf{A}$ by %$\mathcal{F}\mathrm{i}_{\mathsf{L}}\mathbf{A}$.
	
	Given a language $\mathcal{L}$, we put $Eq_{\mathcal{L}}= (\mathrm{Form}_{\mathcal{L}})^2$. Elements of $Eq_{\mathcal{L}}$ we call \emph{equations} and write $\varphi =\psi$ instead of $(\varphi,\psi)$. Mappings
	\[ \rho:Eq_{\mathcal{L}}\rightarrow 2^{\mathrm{Form}_{\mathcal{L}}}\ \text{and}\ \tau:\mathrm{Form}_{\mathcal{L}}\rightarrow 2^{Eq_{\mathcal{L}}}\]
	are called a \emph{transformer of equations} and, respectively, a  \emph{transformer of formulas}. A transformer is said to be \emph{structural} if it commutes with substitutions. It can be easily seen that a structural transformer $\rho$ is uniquely determined by a set  $\rho(p=q)=\Delta(p,q)$, in which case $\rho(\epsilon=\delta):=\Delta(\epsilon,\delta)$ for any $\epsilon,\delta\in Fm_{\mathcal{L}}$. In a similar way, a structural transformer $\tau$ is determined by $\tau(p)=E(p)$. 	
	
	
	A logic $\mathsf{L}$ is is said to be \emph{algebraizable} if there are a class $\mathcal{K}$ of $\mathcal{L}$-algebras and  structural transformers $\tau$ and $\rho$, which determing mutually inverse faithful embeddings of consequense relations $\models_{\mathcal{K}}$ and $\vdash_{\mathsf{L}}$  (see \cite[Definition~3.9]{Font16} for more details). Here $\models_{\mathcal{K}}\subseteq 2^{Eq_{\mathcal{L}}}\times Eq_{\mathcal{L}}$ denotes the equiational consequence relation accociated with the class $\mathcal{K}$ (see \cite[Sec.~1.6]{Font16}). In this case, we call $\Delta(p,q)$ and $E(q)$ the \emph{equivalence formulas} and the \emph{defining equations}, respectively. 
	
	It is known \cite[Corollary 3.18]{Font16} that for every  algebraizable logic $\mathsf{L}$, there is a \emph{largest} class of algebras $\mathcal{K}^{*}$ such that $\mathsf{L}$ is algebraizable with respect to it, and that the class $\mathcal{K}^{*}$ forms a quasivariety.  This class is called the \emph{equivalent algebraic semantics} of $\mathsf{L}$.  
	
	In what follows we consider logics containing  the implication connective $\rightarrow$ in their languages. We use  an expression $\varphi\leftrightarrow\psi$ for an abbreviation of two formulas $\varphi\rightarrow\psi$ and $\psi\rightarrow\varphi$, and we write $\Gamma\vdash\varphi\leftrightarrow\psi$ instead of $\Gamma\vdash\varphi\rightarrow\psi$ and $\Gamma\vdash\psi\rightarrow\varphi$. In a similar way, a rule 
	\[\frac{\varphi_1,\ldots,\varphi_n}{\psi\leftrightarrow\chi}\] must be considered as an abbreviation for two rules
	\[\frac{\varphi_1,\ldots,\varphi_n}{\psi\rightarrow\chi}\ \ \ \text{and}\ \ \ \frac{\varphi_1,\ldots,\varphi_n}{\chi\rightarrow\psi}.\]
	
	\begin{definition}\cite[Definition~2.3]{Font16} A logic $\mathsf{L}=\langle\mathcal{L},\vdash_\mathsf{L}\rangle$ is said to be {\em implicative}, if the implication connective $\rightarrow$ belongs to $\mathcal{L}$ and the following conditions are satisfied for $\vdash_{\mathsf{L}}$:
		
		
		\begin{itemize}
			
			\item[(IL1)] $p\rightarrow p\in \mathrm{Thm}(\mathsf{L})$; 
			
			
			\item[(IL2)] $\{ p\rightarrow q, q\rightarrow r\}\vdash_{\mathsf{L}} p\rightarrow r$;
			
			
			\item[(IL3)] $\{ p_1\leftrightarrow q_1, \ldots, p_n\leftrightarrow q_n\}\vdash_{\mathsf{L}} f(p_1,\ldots,p_n)\rightarrow f(q_1,\ldots,q_n)$ 
			for every $n$-ary connective $f\in\mathcal{L}$;
			
			\item[(IL4)] $\{ p,\; p\rightarrow q\}\vdash_{\mathsf{L}} q$
			
			\item[(IL5)] $\{ p\}\vdash_{\mathsf{L}} q\rightarrow p$
			
		\end{itemize}
		
	\end{definition}
	
	Let $\mathcal{A}$ be an algebra of the language $\mathcal{L}$. A homomorphism $v:\mathcal{F} or_{\mathcal{L}}\rightarrow\mathcal{A}$ we call an {\em $\mathcal{A}$-valuation}.
	
	\begin{definition}\cite[Definition~2.5]{Font16}
		Let $\mathsf{L}=\langle\mathcal{L},\vdash_{\mathsf{L}}\rangle$  be an implicative logic. An {$\mathsf{L}$-algebra} is an algebra $\mathcal{A}$ of the language $\mathcal{L}$ containing an element $1$ such that:
		
		\medskip
		\begin{itemize}
			
			\item[(AL1)] for every $\Gamma\cup\{\varphi\}\subseteq\mathrm{Form}_\mathcal{L}$ and an $\mathcal{A}$-valuation $v$
			$$(\Gamma\vdash_{\mathsf{L}}\varphi\ \text{and}\  v(\Gamma)\subseteq\{1\})\ \ \Rightarrow \ \ v(\varphi)=1; $$
			
			\medskip
			\item[(AL2)] $a\rightarrow b=1$ and $b\rightarrow a=1$ implies $a=b$ for all $a,b\in \mathcal{A}$.
			
		\end{itemize}
		
		%\medskip
		%The class of all $\mathsf{L}$-algebras we denote as $\Alg^* \mathsf{L}$.
		
	\end{definition}
	
	
	
	\begin{theorem}\cite[Proposition~3.13]{Font16} Every implicative logic $L$ is algebraizable with respect to the class of all $\mathsf{L}$-algebras with the equivalence formulas $\{ p\rightarrow q,\; q\rightarrow p\}$ and the defining identity $p=1$.
	\end{theorem}
	
	This theorem shows that implicative logics are logics admitting the standard way of algebraization as, e.g., classical logic and boolean algebras, intuitionistic logic and Heyting algebras, normal modal logic $\mathsf{S4}$ and topoboolean algebras, etc.
	
	We say that a logic $\mathsf{L}=\langle\mathcal{L},\vdash_L\rangle$ with $\rightarrow\in\mathcal{L}$ {\em has the deduction theorem} (is a {\em logic with DT}) if for every $\Gamma\cup\{\varphi,\psi\}\subseteq\mathrm{Form}_{\mathcal{L}}$, the following equivalence holds:
	\[ \Gamma\cup\{\varphi\}\vdash_{\mathsf{L}}\psi\ \ \text{implies}\ \ \Gamma\vdash_{\mathsf{L}}\varphi\rightarrow\psi.\]
	Notice that the inverse implication holds for every implicative logic by (IL4).
	
	Recall that an inference rule $$\frac{\psi_1,\ldots,\psi_n}{\varphi}$$ is {\em derivable} is a logic $\mathsf{L}$ if $\{\psi_1,\ldots,\psi_n\}\vdash_{\mathsf{L}}\varphi$.
	
	\begin{proposition} Let $\mathsf{L}=\langle\mathcal{L},\vdash_{\mathsf{L}}\rangle$ be an implicative logic with DT. 
		\begin{enumerate} 
			\item $\tilde{\Omega}(\mathsf{L})=\Lambda\mathsf{L}$.
			
			\item The replacement rule is derivable in $\mathsf{L}$:
			\[ (RR)\ \ \ \frac{p_1\leftrightarrow q_1,\ldots, p_n\leftrightarrow q_n}{\theta(p_1,\ldots,p_n)\leftrightarrow\theta(q_1,\ldots,q_n)},\] 
			where $\theta$ is an arbitrary $\mathcal{L}$-formula.
			
		\end{enumerate}
	\end{proposition}
	
	\begin{proof} 1. The fact that $\Lambda\mathcal{L}$ is a congruence easily follows from DT and (IL3).
		
		2. This can be proved by a standard induction on the complexity of $\theta$. The inductive base  follows from (IL1), and the inductive step for every $f\in\mathcal{L}$ from (IL3).
	\end{proof}
	
	
	
	
	Following \cite{Gyuris99}  we present the notion of definitional equivalence of logics based on structural translations between their languages.
	
	\begin{definition} Let $\mathcal{L}_1$ and $\mathcal{L}_2$ be propositional languages. A mapping  $\theta\!: \mathrm{Form}_{\mathcal{L}_1}\rightarrow \mathrm{Form}_{\mathcal{L}_2}$ is called a  {\em structural translation} if there is a mapping  $\alpha\!:\mathcal{L}_1\rightarrow\mathrm{Form}_{\mathcal{L}_2}$ such that 
		\[ \theta(p)=p,\ p\in \mathsf{Prop};\ \ \ \theta(c(\varphi_1,\ldots,\varphi_n))=\alpha(c)( \theta(\varphi_1),\dots, \theta(\varphi_n)),\]
		where $c\in\mathcal{L}_1$ and $\varphi_1,\ldots,\varphi_n\in \mathrm{Form}_{\mathcal{L}_1}$. Moreover, we admit that if $c\in\mathcal{L}_1$ is a constant, then its translation $\alpha(c)$ may contain propositional variables, but the formula $\alpha(c)=\alpha(c)(p_1,\ldots,p_k)$ is equivalent to any of its partial cases w.r.t. the Tarski congruence, i.e., \[(\alpha(c)(p_1,\ldots,p_k),\alpha(c)(\xi_1,\ldots,\xi_k))\in\tilde{\Omega}(\mathcal{L}_1)\ \  \text{for any}\ \ \xi_1,\ldots,\xi_k\in \mathrm{Form}_{\mathcal{L}_2}.\] 
		 
		
		
	\end{definition}
	
	
	
	\begin{definition}
		
		Let $\mathsf{L}_1=\langle\mathcal{L}_1,\vdash_{\mathsf{L}_1}\rangle$ and $\mathsf{L}_2=\langle\mathcal{L}_2,\vdash_{\mathsf{L}_2}\rangle$ be  logics, and let  \[\theta\!: \mathrm{Form}_{\mathcal{L}_1}\rightarrow \mathrm{Form}_{\mathcal{L}_2}\ \text{and}\ \rho\!: \mathrm{Form}_{\mathcal{L}_2}\rightarrow \mathrm{Form}_{\mathcal{L}_1}\] be structural translations. 
		
		We say that $\mathsf{L}_1$ and $\mathsf{L}_2$  are {\em definitionally equivalent via}  $\theta$ and $\rho$ if the following conditions hold:
		
		\medskip
		\begin{enumerate}
			
			\item if $\Gamma\cup \{ \varphi \}\subseteq \mathrm{Form}_{\mathcal{L}_1}$, then $\Gamma\vdash_\mathsf{L_1} \varphi$ implies $\theta(\Gamma)\vdash_\mathsf{L_2} \theta(\varphi)$;
			
			\smallskip
			\item if $\Gamma\cup \{ \varphi \}\subseteq \mathrm{Form}_{\mathcal{L}_2}$, then $\Gamma\vdash_\mathsf{L_2} \varphi$ implies $\rho(\Gamma)\vdash_\mathsf{L_1} \rho(\varphi)$;
			
			\smallskip
			\item for every $\varphi\in \mathrm{Form}_{\mathcal{L}_1}$ and $\psi\in \mathrm{Form}_{\mathcal{L}_2}$,
			\[ (\varphi,\rho\theta(\varphi))\in \tilde{\Omega}(\mathsf{L}_1)\ \ \mbox{and}\ \ (\psi,\theta\rho(\psi))\in \tilde{\Omega}(\mathsf{L}_2).\]
			
		\end{enumerate}
		
	\end{definition}
	
	The above notion of definitional equivalence is connected with that of term equivalence of classes of algebras (see, e.g., \cite{McKenMcNulTayl87}). In \cite[Theorem~4.6]{SpVer08} it was proved  that under some natural additional conditions the term equivalence of equivalent algebraic semantics for two algebraizable logics $\mathsf{L}_1$ and $\mathsf{L}_2$ implies that logics $\mathsf{L}_1$ and $\mathsf{L}_2$ are definitionally equivalent.
	
	\section{Implicative logics with strong negation}
	
	In this section we weaken the notion of implicative logic adopting it to the case when the strong negation connective $\sim$ belongs to the language. In what follows $\varphi\Leftrightarrow\psi$ is an abbreviation for $\varphi\leftrightarrow\psi$ and $\mathord{\sim}\varphi\leftrightarrow\mathord{\sim}\psi$. The abbreviations $\Gamma\vdash\varphi\Leftrightarrow\psi$ and
	\[\frac{\varphi_1,\ldots,\varphi_n}{\psi\Leftrightarrow\chi}\]
	we understand in the same way as in the case of $\leftrightarrow$.		
	\begin{definition} A logic $\mathsf{L}=\tuple{\mathcal{L},\vdash_{\mathsf{L}}}$ is said to be an {\em  implicative logic with strong negation} ({\em sn-implicative logic}), if $\to,\mathord{\sim}\in\mathcal{L}$ and the following conditions hold:
		
		
		\begin{itemize}
			
			\item[(SN1)] $p\to p,\ p\leftrightarrow\mathord{\sim}\mathord{\sim} p\in \mathrm{Thm}(\mathsf{L})$
			
			
			\item[(SN2)] $\{ p\to q, q\to r\}\vdash_{\mathsf{L}} p\to r$
			
			
			\item[(SN3$+$)] $\{ p_1\leftrightarrow q_1, \ldots, p_n\leftrightarrow q_n\}\vdash_{\mathsf{L}} f(p_1,\ldots,p_n)\to f(q_1,\ldots,q_n)$ for every $n$-ary connective $f\in\mathcal{L}\setminus\{\mathord{\sim}\}$
			
			\item[(SN3$-$)] $\{ p_1\Leftrightarrow q_1, \ldots, p_n\Leftrightarrow q_n\}\vdash_{\mathsf{L}} \mathord{\sim} f(p_1,\ldots,p_n)\to \mathord{\sim} f(q_1,\ldots,q_n)$ for every $n$-ary connective $f\in\mathcal{L}\setminus\{\mathord{\sim}\}$.
			
			\item[(SN4)] $\{ p,\; p\to q\}\vdash_{\mathsf{L}} q$
			
			\item[(SN5)] $\{ p\}\vdash_{\mathsf{L}} q\to p$
			
			\item[(SN6)] $\{ p\leftrightarrow q\}\nvdash_{\mathsf{L}} \mathord{\sim} p\leftrightarrow\mathord{\sim} q$
			
		\end{itemize}
		
	\end{definition}
	
	The {\em strong Frege relation} of $\mathsf{L}$ is defined as follows 
	\[ \Lambda^s(\mathsf{L})=\{ (\varphi,\psi) \mid (\varphi,\psi),(\mathord{\sim}\varphi,\mathord{\sim}\psi)\in\Lambda(\mathsf{L})\}.\]
	
	We define the {\em weak Tarski congruence}  $\tilde{\Omega}_w(\mathsf{L})$ of $\mathsf{L}$ as the largest equivalence on $\mathcal{F}or_{\mathcal{L}}$ contained in $\Lambda\mathsf{L}$ and compatible with all connectives in $\mathcal{L}\setminus\{\mathord{\sim}\}$. As well as in the case of Tarski congruence the existence of $\tilde{\Omega}_w(\mathsf{L})$ follows from the fact that the lattice of $\mathcal{L}\setminus\{\mathord{\sim}\}$-congruences on the formula algebra is a complete sublattice in the lattice of equivalences. 
	
	\begin{proposition}\label{WILRR} Let $\mathsf{L}=\tuple{\mathcal{L},\vdash_{\mathsf{L}}}$ be an sn-implicative logic with DT. 
		
		\begin{enumerate}
			\medskip
			\item $\tilde{\Omega}(\mathsf{L})=\Lambda^s{\mathsf{L}}\,\subsetneqq\,\Lambda{\mathsf{L}}=\tilde{\Omega}_w(\mathsf{L})$, in particular,
			\[ \tilde{\Omega}(\mathsf{L})=\{ (\varphi,\psi) \mid (\varphi,\psi),(\mathord{\sim}\varphi,\mathord{\sim}\psi)\in\tilde{\Omega}_w(\mathsf{L})\}.\]
			
			\medskip
			\item The replacement rule {\em (RR)} is not derivable in $L$. At the same time the {\em positive replacement rule} {\em (PR)} and the {\em weak replacement rule} {\em (WR)} are derivable in $L$:
			\[ \text{(PR)}\ \ \ \frac{p_1\leftrightarrow q_1,\ldots, p_n\leftrightarrow q_n}{\theta(p_1,\ldots,p_n)\leftrightarrow\theta(q_1,\ldots,q_n)},\] 
			where $\theta$ is $\mathord{\sim}$-free $\mathcal{L}$-formula. 
			\[ \text{(WR)}\ \ \ \frac{p_1\Leftrightarrow q_1,\ldots, p_n\Leftrightarrow q_n}{\chi(p_1,\ldots,p_n)\leftrightarrow\chi(q_1,\ldots,q_n)},\]
			where $\chi$ is arbitrary $\mathcal{L}$-formula.
			
		\end{enumerate}
		
	\end{proposition}
	
	\begin{proof} 1. The relation $\Lambda^s{\mathsf{L}}\,\subsetneqq\,\Lambda{\mathsf{L}}$ follows from (SN6). The equality $\Lambda{\mathsf{L}}=\tilde{\Omega}_w(\mathsf{L})$ follows from the fact that $\Lambda{\mathsf{L}}$ is an $\mathcal{L}\setminus\{\mathord{\sim}\}$-congruence, which can be inferred from DT and (SN3$^+$). Finally, from DT, (SN3$^+$) and (SN3$^-$) we infer that $\Lambda^s{\mathsf{L}}$ is a congruence. If a congruence is contained in $\Lambda{\mathsf{L}}$, it is contained in $\Lambda^s{\mathsf{L}}$ too, whence $\tilde{\Omega}(\mathsf{L})=\Lambda^s{\mathsf{L}}$.
		
		2. The derivability of (PR) follows from (SN1) and (SN3$^+$) by induction on the structure of $\theta$. For (WR) the proof follows the same scheme, but in this case we have to consider inductive steps for all  $\mathord{\sim} f$, where $f\in\mathcal{L}\setminus\{\mathord{\sim}\}$, and we do it using (SN3$^-$).
	\end{proof}
	
	Now we weaken the structurality condition for translations of propositional languages.
	
	\begin{definition} Let $\mathcal{L}_1$ and $\mathcal{L}_2$ be propositional  languages and $\mathord{\sim}\in\mathcal{L}_1\cap\mathcal{L}_2$. A mapping $\theta\!: \mathrm{Form}_{\mathcal{L}_1}\to \mathrm{Form}_{\mathcal{L}_2}$ is said to be a {\em weakly structural translation}, if there are two mappings $\alpha$ and $\beta$ assigning to every connective $c\in\mathcal{L}_1\setminus\{\mathord{\sim}\}$ of arity $n$ formulas  $\alpha(c)(p_1,q_1\ldots,p_n,q_n)$ and $\beta(c)(p_1,q_1\ldots,p_n,q_n)$ from $\mathrm{Form}_{\mathcal{L}_2}$ such that 
		$$\theta(p)= p\ \text{and}\ \theta(\mathord{\sim} p)= \mathord{\sim} p\  \text{for}\ p\in \mathsf{Prop},$$ 
		$$\theta(\mathord{\sim}\mathord{\sim} \varphi)=\theta( \varphi),$$
		$$\theta(c( \varphi_1,\ldots, \varphi_n))=\alpha(c)(\theta(\varphi_1),\theta(\mathord{\sim} \varphi_1),\ldots,\theta(\varphi_n), \theta(\mathord{\sim} \varphi_n)),$$
		$$\theta(\mathord{\sim} c(\varphi_1,\ldots, \varphi_n))=\beta(c)(\theta(\varphi_1),\theta(\mathord{\sim} \varphi_1),\ldots,\theta(\varphi_n), \theta(\mathord{\sim} \varphi_n)),$$
		where  $\varphi,\varphi_1,\ldots,\varphi_n\in \mathrm{Form}_{\mathcal{L}_1}$.
		If $c\in\mathcal{L}_1$ is a constant then $\alpha(c)$ and $\beta(c)$ may contain propositional variables, say $\alpha(c)=\psi(p_1,\ldots,p_k)$ and $\beta(c)=\chi(p_1,\ldots,p_k)$, but we assume that these formulas are equivalent to their partial cases w.r.t. the Tarski congruence, i.e.,
		$$(\psi(p_1,\ldots,p_k),\psi(\xi_1,\ldots,\xi_k)), (\chi(p_1,\ldots,p_k),\chi(\xi_1,\ldots,\xi_k)) \in\tilde{\Omega}(\mathcal{L}_2)$$ for any $\xi_1,\ldots,\xi_k\in\mathrm{Form}_{\mathcal{L}_2}$. 
		
		
	\end{definition}
	
	\begin{definition}\label{weak-d-def} Let $\mathsf{L}_1=\tuple{\mathcal{L}_1,\vdash_{\mathsf{L}_1}}$ and $\mathsf{L}_2=\tuple{\mathcal{L}_2,\vdash_{\mathsf{L}_2}}$ be sn-implicative logics. Let 
		$$\theta\!: \mathrm{Form}_{\mathcal{L}_1}\to \mathrm{Form}_{\mathcal{L}_2}\ \text{and}\ \rho\!: \mathrm{Form}_{\mathcal{L}_2}\to \mathrm{Form}_{\mathcal{L}_1}$$ be weakly structural translations. 
		
		We say that $\mathsf{L}_1$ and $\mathsf{L}_2$  are {\em weakly definitionally equivalent via}  $\theta$ and $\rho$, if the following conditions hold:
		
		
		\begin{enumerate}
			
			\item if $\Gamma\cup \{ \varphi \}\subseteq \mathrm{Form}_{\mathcal{L}_1}$, then $\Gamma\vdash_\mathsf{L_1} \varphi$ implies $\theta(\Gamma)\vdash_\mathsf{L_2} \theta(\varphi)$.
			
			\item if $\Gamma\cup \{ \varphi \}\subseteq \mathrm{Form}_{\mathcal{L}_2}$, then $\Gamma\vdash_\mathsf{L_2} \varphi$ implies $\rho(\Gamma)\vdash_\mathsf{L_1} \rho(\varphi)$.
			
			\item for every $\varphi\in \mathrm{Form}_{\mathcal{L}_1}$ and $\psi\in \mathrm{Form}_{\mathcal{L}_2} $,
			\[ (\varphi,\rho\theta(\varphi))\in \tilde{\Omega}_w(\mathsf{L_1})\ \ \mbox{and}\ \ (\psi,\theta\rho(\psi))\in \tilde{\Omega}_w(\mathsf{L_2}).\]
			
		\end{enumerate}
		
	\end{definition}
	
	Our next goal is to distinguish the class of sn-implicative logics, for which the notion of weak  definitional equivalence coincides with that of a definitional equivalence.
	
	\begin{definition}
		Let $\mathsf{L}=\tuple{\mathcal{L},\vdash_{\mathsf{L}}}$ be an sn-implicative logic. We say that $\mathsf{L}$ is a  {\em bl-logic}, if there is a formula $\odot(p,q)\in \mathrm{Form}_{\mathcal{L}}$ such that for every $\varphi, \psi\in \mathrm{Form}_{\mathcal{L}}$ the following holds
		\[ (\odot( \varphi, \psi),\varphi)\in\tilde{\Omega}_w(\mathsf{L})\ \  \mbox{and}\ \ (\mathord{\sim}\odot( \varphi, \psi),\psi)\in\tilde{\Omega}_w(\mathsf{L}).\]
	\end{definition}
	
	Examples of logics satisfying this definition are the logics based on bilattices, e.g., Modal bilattice logic $\mathsf{MBL}$ \cite{RJJ,OdSkWans19}. This fact explains the name "$bl$-logic".
	
	
	\begin{definition}
		\begin{enumerate}
			
			\item  Let $\mathsf{L}=\tuple{\mathcal{L},\vdash_{\mathsf{L}}}$ be a logic and $R\subseteq(\mathrm{Form}_{\mathcal{L}})^2$. We say that  $\chi(p_1,\ldots,p_n)\in\mathrm{Form}_{\mathcal{L}}$  is {\em  agreed with}  $R$, if 
			\[(\varphi_1,\psi_1), \ldots, (\varphi_n,\psi_n)\in R\ \text{implies}\ (\chi(\varphi_1,\ldots,\varphi_n),\chi(\psi_1,\ldots,\psi_n))\in R.\]
			
			\item Let $\mathsf{L}_1=\tuple{\mathcal{L}_1,\vdash_{\mathsf{L}_1}}$ and $\mathsf{L}_2=\tuple{\mathcal{L}_2,\vdash_{\mathsf{L}_2}}$ be logics, $R\subseteq(\mathrm{Form}_{\mathcal{L}_2})^2$ and  $\to,\mathord{\sim}\in\mathcal{L}_1\cap\mathcal{L}_2$. A weakly structural translation  $\theta\!\!: \mathrm{Form}_{\mathcal{L}_1}$ $\to$ $\mathrm{Form}_{\mathcal{L}_2}$ determined by the mappings  $\alpha$ and $\beta$ is said to be {\em  agreed with}  $R$,  if for every $n$-ary connective $c\in\mathcal{L}_1\setminus\{\mathord{\sim}\}$ the formulas   
			$\alpha(c)(p_1,q_1,\ldots,p_n,q_n)$ and  $\beta(c)(p_1,q_1,\ldots,p_n,q_n)$ are agreed with  $R$.
			
		\end{enumerate}
	\end{definition}
	
	Recall that for a logic $\mathsf{L}=\tuple{\mathcal{L},\vdash_{\mathsf{L}}}$, a rule 
	
	\[\frac{\varphi_1,\ldots,\varphi_n}{\psi}\]
	is {\em admissible} in $\mathsf{L}$ if for every substitution $s$ we have $s\psi\in\mathrm{Thm}(\mathsf{L})$ whenever $\{s\varphi_1,\ldots,s\varphi_n\}\subseteq\mathrm{Thm}(\mathsf{L})$.
	
	\begin{proposition}
		If $\mathsf{L}=\tuple{\mathcal{L},\vdash_{\mathsf{L}}}$ is an sn-implicative logic with DT, then $\chi(p_1,\ldots,p_n)\in\mathrm{Form}_{\mathcal{L}}$  is agreed with  $\tilde{\Omega}_w(\mathsf{L})$ iff the rule
		
		\begin{equation}\frac{ p_1\leftrightarrow q_1,\ldots,p_n\leftrightarrow q_n}{\chi(p_1,\ldots,p_n)\leftrightarrow\chi(q_1,\ldots,q_n)}
			\label{*}
		\end{equation} is admissible in $\mathsf{L}$.
	\end{proposition}
	
	\begin{proof} Assume that $\chi(p_1,\ldots,p_n)$  is agreed with  $\tilde{\Omega}_w(\mathsf{L})$ and 
		\begin{equation} \varphi_1\leftrightarrow \psi_1,\ldots,\varphi_n\leftrightarrow \psi_n\in\mathrm{Thm}(\mathsf{L})
			\label{**}.\end{equation}
		Then $(\varphi_1,\psi_1),\ldots,(\varphi_n,\psi_n)\in\Lambda\mathsf{L}$ by (SN5). Since $\Lambda\mathsf{L}=\tilde{\Omega}_w(\mathsf{L})$ by Proposition~\ref{WILRR} we obtain $(\chi(\varphi_1,\ldots,\varphi_n),\chi(\psi_1,\ldots,\psi_n))\in\tilde{\Omega}_w(\mathsf{L})$. Applying again Proposition~\ref{WILRR} we obtain that $\chi(\varphi_1,\ldots,\varphi_n)$ and $\chi(\psi_1,\ldots,\psi_n)$ are mutually inferable in $\mathsf{L}$, whence $\chi(\varphi_1,\ldots,\varphi_n)\leftrightarrow\chi(\psi_1,\ldots,\psi_n)\in\mathrm{Thm}(\mathsf{L})$ by DT. 
		
		Now we assume that \eqref{*} is an admissible rule of $\mathsf{L}$. If \[(\varphi_1,\psi_1),\ldots,(\varphi_n,\psi_n)\in\tilde{\Omega}_w(\mathsf{L})=\Lambda\mathsf{L},\] then by DT we arrive at \eqref{**}. The admissibility of the rule~\eqref{*} implies $\chi(\varphi_1,\ldots,\varphi_n)\leftrightarrow\chi(\psi_1,\ldots,\psi_n)\in\mathrm{Thm}(\mathsf{L})$, which is equivalent to the relation $(\chi(\varphi_1,\ldots,\varphi_n),\chi(\psi_1,\ldots,\psi_n))\in\tilde{\Omega}_w(\mathsf{L})$.
	\end{proof}
	
	\begin{theorem}\label{wde->de} Let $\mathsf{L}_1=\tuple{\mathcal{L}_1,\vdash_{\mathsf{L}_1}}$ and $\mathsf{L}_2=\tuple{\mathcal{L}_2,\vdash_{\mathsf{L}_2}}$  be  $bl$-logics with DT. Let  $\theta:\mathrm{Form}_{\mathcal{L}_1}\to\mathrm{Form}_{\mathcal{L}_2}$ and $\rho:\mathrm{Form}_{\mathcal{L}_2}\to\mathrm{Form}_{\mathcal{L}_2}$ be two weakly structural translations such that $\mathsf{L}_1$ and $\mathsf{L}_2$ are weakly definitionally equivalent via $\theta$ and $\rho$. Assume that $\theta$  is agreed with $\tilde{\Omega}_w(\mathsf{L}_2)$,  $\rho$  is agreed with $\tilde{\Omega}_w(\mathsf{L}_1)$. 
		Then there are structural translations $\theta'$ and $\rho'$ commuting with $\mathord{\sim}$ and such that logics $L_1$ and $L_2$ are  definitionally equivalent via $\theta'$ and $\rho'$.
	\end{theorem}
	
	\begin{proof} Since $\theta$ is  a weakly structural translation it is determined by some mappings $\alpha$ and $\beta$ acting from $\mathcal{L}_1\setminus\{ \sim\}$ to $\mathrm{Form}_{\mathcal{L}_2}$. Let $\gamma$ and $\delta$ be mappings from $\mathcal{L}_2\setminus\{ \sim\}$ to $\mathrm{Form}_{\mathcal{L}_1}$ that determine $\rho$. 
		
		Since $\mathsf{L}_1$ and $\mathsf{L}_2$ are $bl$-logics, there are formulas $\odot_1(p,q)\in\mathrm{Form}_{\mathcal{L}_1}$ and $\odot_2(p,q)\in\mathrm{Form}_{\mathcal{L}_2}$ such that 
		\[ (\odot_i( \varphi, \psi),\varphi)\in \tilde{\Omega}_w(\mathsf{L}_i) \ \ \mbox{and}\ \ (\mathord{\sim}\odot_i( \varphi, \psi),\psi)\in \tilde{\Omega}_w(\mathsf{L}_i)\] for all $\varphi,\psi\in\mathrm{Form}_{\mathcal{L}_i}$, $i\in\{ 1,2\}$. 
		For every $f\in\mathcal{L}_1\setminus\{\mathord{\sim}\}$ of arity $n$ and $g\in\mathcal{L}_2\setminus\{\mathord{\sim}\}$ of arity $m$ we put			
		\[\zeta(f)=\odot_2(\alpha(f)(p_1,\mathord{\sim}p_1,\ldots,p_n,\mathord{\sim}p_n), \beta(f)(p_1,\mathord{\sim}p_1,\ldots,p_n,\mathord{\sim}p_n)),\]
		\[\eta(g)=\odot_1(\gamma(g)(p_1,\mathord{\sim}p_1,\ldots,p_m,\mathord{\sim}p_m), \delta(g)(p_1,\mathord{\sim}p_1,\ldots,p_m,\mathord{\sim}p_m)).\]
		Defining 
		\[\zeta(\mathord{\sim})=\mathord{\sim}p\ \ \mbox{and}\ \ \eta(\mathord{\sim})=\mathord{\sim}p.\]
		we obtain two mappings  $\zeta:\mathcal{L}_1\to \mathrm{Form}_{\mathcal{L}_2}$ and $\eta:\mathcal{L}_2\to \mathrm{Form}_{\mathcal{L}_1}$, which can be used to define structural translations
		\[\theta':\mathrm{Form}_{\mathcal{L}_1}\to \mathrm{Form}_{\mathcal{L}_2}\ \ \text{and}\ \ \rho':\mathrm{Form}_{\mathcal{L}_2}\to \mathrm{Form}_{\mathcal{L}_1}.\]
		By definition $\theta'$ and $\rho'$ commute with $\mathord{\sim}$. Moreover, they are connected with $\theta$ and $\rho$ as follows.
		
		\begin{lemma}\label{EquivTrans} For every $\varphi\in\mathrm{Form}_{\mathcal{L}_1}$ and $\psi\in\mathrm{Form}_{\mathcal{L}_2}$, we have
			\[(\theta(\varphi),\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_2) \ \mbox{and}\ \ (\rho(\psi),\rho'(\psi))\in\tilde{\Omega}_w(\mathsf{L}_1).\]
		\end{lemma}
		
		\begin{proof} We prove that $(\theta(\varphi),\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_2)$  by induction on the structure of formulas, the proof of the second relation is similar. For $p\in\mathrm{Prop}$ by definition we have
			\[ \theta'(p)=p=\theta(p)\ \ \mbox{and}\ \ \theta'(\mathord{\sim}p)=\mathord{\sim}\theta'(p)=\mathord{\sim}p=\theta(\mathord{\sim}p).\]
			For every $\varphi\in\mathrm{Form}_{\mathcal{L}_2}$, we obviously have  $(\varphi,\varphi)\in\Lambda\mathsf{L}_2=\tilde{\Omega}_w(\mathsf{L}_2)$,  in particular, $(p,p),(\mathord{\sim} p,\mathord{\sim} p)\in\tilde{\Omega}_w(\mathsf{L}_2)$. 
			
			Let $f$ be an $n$-ary connective of $\mathcal{L}_1$. Assume that for $\varphi_1$, \ldots, $\varphi_n\in\mathrm{Form}_{\mathcal{L}_1}$ we  proved
			\[(\theta(\varphi_i),\theta'(\varphi_i)),\,(\theta(\mathord{\sim}\varphi_i),\theta'(\mathord{\sim}\varphi_i))\in\tilde{\Omega}_w(\mathsf{L}_2), \ i=1,\ldots,n.\]
			We have then
			\[\theta'(f(\varphi_1,\ldots, \varphi_n))=\odot_2(\alpha(f)(\theta'( \varphi_1),\theta'(\mathord{\sim}\varphi_1),\ldots),\beta(f)(\theta'( \varphi_1),\mathord{\sim}\theta'(\mathord{\sim}\varphi_1),\ldots)), \]
			and by the properties of $\odot_2(p,q)$ 
			\[(\theta'(f(\varphi_1,\ldots, \varphi_n)),\alpha(f)(\theta'( \varphi_1),\theta'(\mathord{\sim}\varphi_1),\ldots))\in\tilde{\Omega}_w(\mathsf{L}_2).\]
			The induction hypothesis and the assumption that $\theta$ is agreed with $\tilde{\Omega}_w(\mathsf{L}_2)$ yield 
			\[(\theta'(f(\varphi_1,\ldots, \varphi_n)),\alpha(f)(\theta( \varphi_1),\theta(\mathord{\sim}\varphi_1),\ldots))\in\tilde{\Omega}_w(\mathsf{L}_2),\]
			i.e., $(\theta'(f(\varphi_1,\ldots, \varphi_n)),\theta(f(\varphi_1,\ldots, \varphi_n)))\in\tilde{\Omega}_w(\mathsf{L}_2)$.
			For a negated formula we have $\theta'(\mathord{\sim} f( \varphi_1,\ldots, \varphi_n))=\mathord{\sim}\theta'(f( \varphi_1,\ldots, \varphi_n))$=
			\[ \mathord{\sim}\odot_2(\alpha(f)(\theta'( \varphi_1),\mathord{\sim}\theta'(\varphi_1),\ldots),\beta(f)(\theta'(\varphi_1),\mathord{\sim}\theta'(\varphi_1),\ldots)). \]
			Applying again the properties of $\odot_2(p,q)$ we obtain
			\[(\theta'(\mathord{\sim} f( \varphi_1,\ldots, \varphi_n)),\beta(f)(\theta'(\varphi_1),\mathord{\sim}\theta'(\varphi_1),\ldots))\in\tilde{\Omega}_w(\mathsf{L}_2).\]
			The fact that  $\beta(f)$ agrees with $\tilde{\Omega}_w(\mathsf{L}_2)$ implies
			\[(\theta'(\mathord{\sim} f( \varphi_1,\ldots, \varphi_n)),\beta(f)(\theta(\varphi_1),\mathord{\sim}\theta(\varphi_1),\ldots)))\in\tilde{\Omega}_w(\mathsf{L}_2),\]
			i.e., $(\theta'(\mathord{\sim} f(\varphi_1,\ldots, \varphi_n)),\theta(\mathord{\sim} f(\varphi_1,\ldots, \varphi_n)))\in\tilde{\Omega}_w(\mathsf{L}_2)$.
		\end{proof}
		
		Let $\varphi_1,\ldots,\varphi_n,\psi\in\mathrm{Form}_{\mathcal{L}_1}$.  By the above lemma
		\[ (\theta(\varphi_1),\theta'(\varphi_1)),\ldots, (\theta(\varphi_n),\theta'(\varphi_n)),\ (\theta(\psi),\theta'(\psi))\in\tilde{\Omega}_w(\mathsf{L}_2).\] The equality $\tilde{\Omega}_w(\mathsf{L}_2)=\Lambda\mathsf{L}_2$ implies then 
		\[ \theta'(\varphi_1)\vdash_{\mathsf{L}_2}\theta(\varphi_1),\ldots, \theta'(\varphi_n)\vdash_{\mathsf{L}_2}\theta(\varphi_n)\ \text{and}\ \theta(\psi)\vdash_{\mathsf{L}_2}\theta'(\psi).\] This fact and the transitivity of $\vdash_{\mathsf{L}_2}$ entail that 
		\[\theta(\varphi_1),\ldots,\theta(\varphi_n)\vdash_{\mathsf{L}_2}\theta(\psi)\ \ \mbox{implies}\ \theta'(\varphi_1),\ldots,\theta'(\varphi_n)\vdash_{\mathsf{L}_2}\theta'(\psi).\]
		This fact and the assumption that $\theta$  embeds $\mathsf{L_1}$ into $\mathsf{L_2}$ imply that $\theta'$  embeds $\mathsf{L_1}$ into $\mathsf{L_2}$ too. In a similar way, one can prove that $\rho'$  embeds $\mathsf{L_2}$ into $\mathsf{L_1}$.
		
		It remains to check Item~3 of Definition~\ref{weak-d-def}. We have by assumption  $(\varphi,\rho\theta(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$ for every $\varphi\in\mathrm{Form}_{\mathcal{L}_1}$, and by Lemma~\ref{EquivTrans}, $(\theta(\varphi),\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_2)$, which is equivalent to $\theta(\varphi)\vdash_{\mathsf{L}_2}\theta'(\varphi)$ and $\theta'(\varphi)\vdash_{\mathsf{L}_2}\theta(\varphi)$. Since $\rho$ embeds $\mathsf{L_2}$ into $\mathsf{L_1}$, we obtain $\rho\theta(\varphi)\vdash_{\mathsf{L}_1}\rho\theta'(\varphi)$ and $\rho\theta'(\varphi)\vdash_{\mathsf{L}_1}\rho\theta(\varphi)$, i.e., $(\rho\theta(\varphi),\rho\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$. By Lemma~\ref{EquivTrans}, $(\rho\theta'(\varphi),\rho'\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$. Applying twice the transitivity of weak Tarski congruence, we conclude $(\varphi,\rho'\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$. Since both $\theta'$ and $\rho'$ commute with $\mathord{\sim}$, from $(\mathord{\sim}\varphi,\rho'\theta'(\mathord{\sim}\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$ we obtain $(\mathord{\sim}\varphi,\mathord{\sim}\rho'\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$
		Finally, the conjunction $(\varphi,\rho'\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$ and $(\mathord{\sim}\varphi,\mathord{\sim}\rho'\theta'(\varphi))\in\tilde{\Omega}_w(\mathsf{L}_1)$ is equivalent to $(\varphi,\rho'\theta'(\varphi))\in\tilde{\Omega}(\mathsf{L}_1)$ by Item~1 of  Proposition~\ref{WILRR}. 
		Arguing in a similar way we obtain  $(\psi,\theta'\rho'(\psi))\in\tilde{\Omega}(\mathsf{L}_2)$ for $\psi\in\mathrm{Form}(\mathcal{L}_2)$.
		
	\end{proof}
	
	\section{Examples of weakly  definitionally equivalent logics}
	
	In this section we will consider logics in different languages, but all these logics are local consequence relations defined via models of the form $\mathcal{M}=\langle W,\leq,v^+,v^-\rangle$, where $W$ is a non-empty set of worlds (information states), $\leq\,\subseteq W\times W$ is a preorder relation, and the valuations $v^+,v^-:\mathrm{Prop}\rightarrow 2^W$ are such that $v^+(p)$ and $v^-(p)$ are cones w.r.t. $\leq$ for every $p\in\mathrm{Prop}$, i.e., $w\in v^+(p)$ and $w\leq u$ imply $u\in v^+(p)$, and the same holds for $v^-$. Every logic  $\mathsf{L}=\langle\mathcal{L},\vdash_{\mathsf{L}}\rangle$ under consideration is defined via a class of $\mathsf{L}$-models as follows. For an $\mathsf{L}$-model $\mathcal{M}$,  the support of truth and support of falsity relations $\models^+_{\mathsf{L}}$ and $\models^-_{\mathsf{L}}$ between worlds of $\mathcal{M}$ and $\mathcal{L}$-formulas are defined so that we always have 
	\[ \mathcal{M},w\models^+_{\mathsf{L}} p\  \Leftrightarrow\  w\in v^+(p)\ \ \text{and}\ \ \mathcal{M},w\models^-_{\mathsf{L}} p\ \Leftrightarrow\ w\in v^-(p);\]
	\[ \mathcal{M},w\models^+_{\mathsf{L}} \mathord{\sim}\varphi \ 
	\Leftrightarrow \ \mathcal{M},w\models^-_{\mathsf{L}} \varphi\ \ \text{and}\ \ \mathcal{M},w\models^-_{\mathsf{L}} \mathord{\sim}\varphi \
	\Leftrightarrow \ \mathcal{M},w\models^+_{\mathsf{L}} \varphi.\]
	
	For $\Gamma\cup\{\varphi\}\subseteq\mathrm{Form}_{\mathcal{L}}$, the relation $\Gamma\vdash_{\mathsf{L}}\varphi$ means that for every $\mathsf{L}$-model $\mathcal{M}$ and a world $w$ of $\mathcal{M}$,
	\[ (\mathcal{M},w\models^+_{\mathsf{L}}\psi\ \text{for all}\ \psi\in\Gamma)\ \Rightarrow\ \ \mathcal{M},w\models^+_{\mathsf{L}}\varphi.\]
	In what follows we omit the lower index $-_{\mathsf{L}}$ if the reference to $\mathsf{L}$ is clear from the setting.
	
	\begin{lemma}\label{TwT} Let $\mathsf{L}=\langle\mathcal{L},\vdash_{\mathsf{L}}\rangle$ be a logic, where $\vdash_{\mathsf{L}}$ is defined as a local consequence relation over a class of $\mathsf{L}$-models, and $\varphi,\psi\in\mathrm{Form}_{\mathcal{L}}$. If $\mathsf{L}$ is an sn-implicative logic with DT, then the following equivalences hold:
		\begin{enumerate}
			\item $(\varphi,\psi)\in\tilde{\Omega}_w(\mathsf{L})$ iff for every $\mathsf{L}$-model $\mathcal{M}$ and a world $w$ of $\mathcal{M}$,
			\[ \mathcal{M},w\models^+_{\mathsf{L}}\varphi\  \Leftrightarrow\  \mathcal{M},w\models^+_{\mathsf{L}}\psi;\]
			\item $(\varphi,\psi)\in\tilde{\Omega}(\mathsf{L})$ iff for every $\mathsf{L}$-model $\mathcal{M}$ and a world $w$ of $\mathcal{M}$,
			\[ \mathcal{M},w\models^+_{\mathsf{L}}\varphi\  \Leftrightarrow\  \mathcal{M},w\models^+_{\mathsf{L}}\psi\ \ \text{and}\ \ \mathcal{M},w\models^-_{\mathsf{L}}\varphi\  \Leftrightarrow\  \mathcal{M},w\models^-_{\mathsf{L}}\psi.\]
		\end{enumerate}
	\end{lemma}
	
	\begin{proof} Item~1 follows from the definition of $\vdash_{\mathsf{L}}$ and the fact that $(\varphi,\psi)\in\tilde{\Omega}_w(\mathsf{L})$ iff $\{\varphi\}\vdash_{\mathsf{L}}\psi$ and $\{\psi\}\vdash_{\mathsf{L}}\varphi$ (see Lemma~\ref{WILRR}).
		Item~2 follows from the equivalence of $(\varphi,\psi)\in\tilde{\Omega}(\mathsf{L})$ and $(\varphi,\psi), (\mathord{\sim}\varphi,\mathord{\sim}\psi) \in\tilde{\Omega}_w(\mathsf{L})$ (see Lemma~\ref{WILRR} again).
	\end{proof}
	
	Thus, for logics considered in this section, the weak Tarski congruence is the equivalence argeed with the truth in every world of every model,  the  Tarski congruence is the equivalence argeed with the truth  and the falsity as well.
	
	First we establish the weak definitional equivalence of Nelson's constructive logic $\mathsf{N4}^{\bot}$ \cite{AlmukdadNelson,Odintsov05} and of Wansing's constructive connexive logic $\mathsf{C}^{\bot}$ \cite{Wansing2005, FazOd2024}. Both  logics are defined via the class of all models in the language $\mathcal{L}^{\mathord{\sim}}=\{ \vee,\wedge,\rightarrow,\bot,\mathord{\sim}\}$. For $\mathsf{N4}^{\bot}$, we define $\models^+$ and $\models^-$ as follows:
	
	\begin{itemize}
		
		\item [] $\mathcal{M},w\models^+ \varphi \vee \psi \;\; \Leftrightarrow \;\;
		(\mathcal{M},w\models^+ \varphi\;\; \mbox{or} \;\; \mathcal{M},w\models^+ \psi )$
		
		\item [] $\mathcal{M},w\models^- \varphi \vee \psi \;\; \Leftrightarrow \;\;
		(\mathcal{M},w\models^- \varphi\;\; \mbox{and} \;\; \mathcal{M},w\models^- \psi )$
		
		\item [] $\mathcal{M},w\models^+ \varphi \wedge \psi \;\; \Leftrightarrow
		\;\; (\mathcal{M},w\models^+ \varphi\;\; \mbox{and} \;\; \mathcal{M},w\models^+ \psi )$
		
		\item [] $\mathcal{M},w\models^- \varphi \wedge \psi \;\; \Leftrightarrow \;\;
		(\mathcal{M},w\models^- \varphi\;\; \mbox{or} \;\; \mathcal{M},w\models^- \psi )$
		
		\item [] $\mathcal{M},w\models^+ \varphi \rightarrow \psi \;\;
		\Leftrightarrow \;\; \forall u \geq w\;
		(\mathcal{M},u\models^+ \varphi \Rightarrow \mathcal{M},u\models^+\psi )$
		
		\item [] $\mathcal{M},w\models^- \varphi \rightarrow \psi \;\;
		\Leftrightarrow \;\; 
		(\mathcal{M},w\models^+ \varphi \;\; \mbox{and} \;\; \mathcal{M},w \models^-\psi )$
		
		\item [] $\mathcal{M},w\not\models^+ \bot\ \ \text{and} \ \ \mathcal{M},w\models^- \bot$
		
		
	\end{itemize}
	
	In the case of $\mathsf{C}^{\bot}$ the support of truth is defined as above and the support of falsity also is defined as above except for the case of implication:
	
	\begin{itemize}
		\item [] $\mathcal{M},w\models^- \varphi \rightarrow \psi \;\;
		\Leftrightarrow \;\; \forall u \geq w\;
		(\mathcal{M},u\models^+ \varphi \Rightarrow \mathcal{M},u\models^-\psi )$
	\end{itemize} 
	
	Let us define  weakly structural translations $\theta,\rho:\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}\rightarrow\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ so that they commute with binary connectives, $\theta(\bot)=\bot$, $\rho(\bot)=\bot$, and for negated formulas they are defined as follows:
	\[ \theta(\mathord{\sim}(\varphi\vee\psi))=\theta(\mathord{\sim}\varphi)\wedge\theta(\mathord{\sim}\psi),\ \theta(\mathord{\sim}(\varphi\wedge\psi))=\theta(\mathord{\sim}\varphi)\vee\theta(\mathord{\sim}\psi)\]
	\[ \theta(\mathord{\sim}(\varphi\rightarrow\psi))=\theta(\varphi)\wedge\theta(\mathord{\sim}\psi),\ \theta(\mathord{\sim}\bot)=\mathord{\sim}\bot;\]
	\[ \rho(\mathord{\sim}(\varphi\vee\psi))=\rho(\mathord{\sim}\varphi)\wedge\rho(\mathord{\sim}\psi),\ \rho(\mathord{\sim}(\varphi\wedge\psi))=\rho(\mathord{\sim}\varphi)\vee\rho(\mathord{\sim}\psi)\]
	\[ \rho(\mathord{\sim}(\varphi\rightarrow\psi))=\rho(\varphi)\rightarrow\rho(\mathord{\sim}\psi),\ \rho(\mathord{\sim}\bot)=\mathord{\sim}\bot.\]
	
	\begin{proposition}\label{N4Cwde} Logics $\mathsf{N4}^{\bot}$ and $\mathsf{C}^{\bot}$ are sn-implicative logics with DT. Moreover, $\mathsf{N4}^{\bot}$ and $\mathsf{C}^{\bot}$ are weakly definitionally equivalent via $\theta$ and $\rho$.
	\end{proposition}
	
	\begin{proof} It is routine to check using the semantical definitions of $\vdash_{\mathsf{N4}^{\bot}}$ and $\vdash_{\mathsf{C}^{\bot}}$ that both $\mathsf{N4}^{\bot}$ and $\mathsf{C}^{\bot}$ are sn-implicative logics and that they satisfy DT.
		
		The next lemma can be easily proved by induction on the structure of formulas.
		
		\begin{lemma}\label{N4C}
			For every model $\mathcal{M}=\langle W,\leq,v^+,v^-\rangle$, $w\in W$, and $\varphi\in\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}}$ the following equivalences hold:
			
			\medskip
			\begin{tabular}{lll}
				\smallskip
				$\mathcal{M},w\models^+_{\mathsf{N4}^{\bot}} \varphi$ & iff & $\mathcal{M},w\models^+_{\mathsf{C}^{\bot}} \theta(\varphi)$ \\
				
				\smallskip
				$\mathcal{M},w\models^+_{\mathsf{N4}^{\bot}} \rho(\varphi)$ & iff & $\mathcal{M},w\models^+_{\mathsf{C}^{\bot}} \varphi$.
			\end{tabular}
		\end{lemma}
		
		Applying this lemma	twice for a formula $\varphi$ we obtain that for any $\varphi$,
		
		\medskip
		\begin{tabular}{lll}
			\smallskip
			$\mathcal{M},w\models^+_{\mathsf{N4}^{\bot}} \varphi$ & iff & $\mathcal{M},w\models^+_{\mathsf{N4}^{\bot}} \rho\theta(\varphi)$ \\
			
			\smallskip
			$\mathcal{M},w\models^+_{\mathsf{C}^{\bot}} \varphi$ & iff & $\mathcal{M},w\models^+_{\mathsf{C}^{\bot}} \theta\rho\varphi$.
		\end{tabular}
		
		According to Lemma\ref{TwT} these equivalences mean exactly that 
		\[ (\varphi,\rho\theta(\varphi))\in\tilde{\Omega}_w(\mathsf{N4}^{\bot})\ \ \text{and}\ \ (\varphi,\theta\rho(\varphi))\in\tilde{\Omega}_w(\mathsf{C}^{\bot})\]
		for any $\varphi$.
		
		It remains to check that $\theta$ and $\rho$ embed $\mathsf{N4}^{\bot}$ into $\mathsf{C}^{\bot}$ and, respectively, $\mathsf{C}^{\bot}$ into $\mathsf{N4}^{\bot}$. These facts easily follow from the definition of consequence relations and Lemma~\ref{N4C}.
		
	\end{proof}
	
	Now we add to the language $\mathcal{L}^{\mathord{\sim}}$ constants $\mathsf{b}$ and $\mathsf{n}$, $\mathcal{L}^\mathsf{B}=\mathcal{L}^{\mathord{\sim}}\cup\{\mathsf{b},\mathsf{n}\}$, and define $\mathsf{N4}^{\mathsf{B}}$ and $\mathsf{C}^{\mathsf{B}}$ as expansions of $\mathsf{N4}^{\bot}$ and $\mathsf{C}^{\bot}$, respectively, via the following semantical clauses:
	\begin{equation} \mathcal{M},w\models^+\mathsf{b},\ \mathcal{M},w\models^-\mathsf{b} \ \ \text{and}\ \ \mathcal{M},w\not\models^+\mathsf{n},\ \mathcal{M},w\not\models^-\mathsf{n}.
		\label{tfnb}
	\end{equation}
	These definitions demonstrate the similarity of constants $\mathsf{b}$ and $\mathsf{n}$ to Belnapian truth values $Both$ and $Neither$, respectively.
	
	\begin{proposition}\label{N4Cbl} Logics $\mathsf{N4}^{\mathsf{B}}$ and $\mathsf{C}^{\mathsf{B}}$ are $bl$-logics.
	\end{proposition}
	
	\begin{proof} Let us consider the formula\footnote{This formula was found in \cite{ArieliAvron1996} and used to prove that bilattice connectives $\oplus$ and $\otimes$ are definable via $\vee$, $\wedge$, $\mathsf{b}$, and $\mathsf{n}$:
			\[ p\oplus q := \odot(p\vee q,p\vee q)\ \ \text{and}\ \ p\otimes q := \odot(p\wedge q,p\wedge q).\]} 
		\[ \odot(p,q)=(p\wedge\mathsf{b})\vee(\mathord{\sim} q\wedge\mathsf{n}).\]
		It can be immediately checked that for any $\varphi,\psi\in\mathrm{Form}_{\mathcal{L}^\mathsf{B}}$, any model $\mathcal{M}$, and its world $w$,
		\[ \mathcal{M},w\models^+\odot(\varphi,\psi) \Leftrightarrow \mathcal{M},w\models^+\varphi\ \ \text{and}\ \ \mathcal{M},w\models^-\odot(\varphi,\psi) \Leftrightarrow \mathcal{M},w\models^+\psi.\]
		Applying Lemma~\ref{TwT} we obtain for $\mathsf{L}\in\{ \mathsf{N4}^{\mathsf{B}}, \mathsf{C}^{\mathsf{B}}\}$
		\[(\odot(\varphi,\psi),\varphi)\in\tilde{\Omega}_w(\mathsf{L})\ \ \text{and}\ \ (\mathord{\sim}\odot(\varphi,\psi),\psi)\in\tilde{\Omega}_w(\mathsf{L}).\]
	\end{proof}
	
	\begin{proposition}\label{N4Cde} Logics $\mathsf{N4}^{\mathsf{B}}$ and $\mathsf{C}^{\mathsf{B}}$ are definitionally equivalent. 
	\end{proposition}
	
	\begin{proof} We define the translations $\theta^{\mathsf{B}}$ and $\rho^{\mathsf{B}}$ as expansions of $\theta$ and $\rho$ to the language $\mathcal{L}^\mathsf{B}$ that preserve constants $\mathsf{b}$ and $\mathsf{n}$. Naturally, $\mathsf{N4}^{\mathsf{B}}$ and $\mathsf{C}^{\mathsf{B}}$ are weakly definitionally equivalent via $\theta^{\mathsf{B}}$ and $\rho^{\mathsf{B}}$.  Further, the translations $\theta^{\mathsf{B}}$ and $\rho^{\mathsf{B}}$ are agreed with $\tilde{\Omega}_w(\mathsf{C}^{\mathsf{B}})$ and $\tilde{\Omega}_w(\mathsf{N4}^{\mathsf{B}})$, respectively, because the mappings $\alpha_{\theta}$, $\beta_{\theta}$ and $\alpha_{\rho}$, $\beta_{\rho}$ defining these translations use only $\mathord{\sim}$-free formulas, e.g.,
		\[\beta_{\theta}(\rightarrow)=p_1\wedge q_2\ \text{and}\ \beta_{\rho}(\rightarrow)=p_1\rightarrow q_2.\]
		Therefore, we can apply Theorem~\ref{wde->de} to infer the definitional equivalence of $\mathsf{N4}^{\mathsf{B}}$ and $\mathsf{C}^{\mathsf{B}}$ from Propositions~\ref{N4Cwde} and~\ref{N4Cbl}. 
	\end{proof}
	
	
	
	H.~Wansing \cite{Wansing08} introduced and motivated sixteen logics $(I_i, C_j)$, $i, j \in \{1, 2, 3, 4\}$ extending Heyting-Brouwer logic {\sf HB} (see \cite{Buisman07,Crolard01,Rauszer74,Rauszer77,Wolter98}), with the strong negation connective. We will consider these logics in the language $\mathcal{L}^{\mathord{\sim}}_{\mathsf{HB}} = \mathcal{L}^{\mathord{\sim}}\cup\{ {-\!\Yleft}\,\}$. The new symbol ${-\!\Yleft}\,$ is used to denote the coimplication connective, the operation dual to the intuitionistic implication. In algebraic models of {\sf HB} the coimpication ${-\!\Yleft}\,$ form a residual pair with  $\vee$, where as the implication $\rightarrow$ forms a residual pair with  $\wedge$. The support of truth for this connective is defined as follows.
	
	\begin{itemize}
		
		\item [] $\mathcal{M},w\models^+ \varphi {-\!\Yleft}\, \psi \;\;
		\Leftrightarrow \;\; \exists u\leq w \;\; 
		(\mathcal{M},u\models^+ \varphi \;\; \mbox{and} \;\; \mathcal{M},u\not \models^+\psi )$
		
	\end{itemize}
	
	
	All logics $(I_i, C_j)$, $i, j \in \{1, 2, 3, 4\}$ have the same support of truth $\models^+$ defined for ${-\!\Yleft}\,$ as above and for $\vee$, $\wedge$, $\rightarrow$, and $\bot$ in the same way as for $\mathsf{N4}^{\bot}$. The support of falsity for $\vee$, $\wedge$, $\rightarrow$ also is defined as for $\mathsf{N4}^{\bot}$. In  $(I_i, C_j)$, the support of falsity for implication satisfies the condition $cI_i$ and for coimplication the condition $cC_j$, $i, j \in \{1, 2, 3, 4\}$:
	
	\begin{itemize}
		
		\item[$cI_1$]\ \  ${\mathcal{M}}, w \models^- (\varphi \rightarrow \psi)$  $\; \Leftrightarrow \;$  $({\mathcal{M}}, w \models^+ \varphi \mbox{ and } {\mathcal{M}}, w \models^- \psi )$
		
		\item[$cI_2$]\ \  ${\mathcal{M}}, w \models^- (\varphi \rightarrow \psi)$ $\; \Leftrightarrow \;$
		$\forall u \geq w  ({\mathcal{M}}, u \not  \models^+ \varphi \mbox{ or } {\mathcal{M}}, u \models^- \psi )$
		
		\item[$cI_3$]\ \  ${\mathcal{M}}, w \models^- (\varphi \rightarrow \psi)$  $\; \Leftrightarrow \;$   $\exists u \leq w ({\mathcal{M}}, u \models^+ \varphi  \mbox{ and } {\mathcal{M}}, u \not  \models^+ \psi )$
		
		\item[$cI_4$]\ \  ${\mathcal{M}}, w \models^- (\varphi \rightarrow \psi)$  $\; \Leftrightarrow \;$
		$\exists u\leq w ({\mathcal{M}}, u \not  \models^- \varphi \mbox{ and } {\mathcal{M}}, u\models^- \psi )$
		
		\item[$cC_1$]\ \  ${\mathcal{M}}, w \models^- (\varphi {-\!\Yleft}\, \psi)$  $\; \Leftrightarrow \;$    $({\mathcal{M}}, w \models^- \varphi \mbox{ or } {\mathcal{M}}, w \models^+ \psi )$
		
		\item[$cC_2$]\ \ ${\mathcal{M}}, w \models^- (\varphi {-\!\Yleft}\, \psi)$  $\; \Leftrightarrow \;$    $\exists u\leq w  ({\mathcal{M}}, u \models^- \varphi \mbox{ and } {\mathcal{M}}, u \not \models^+ \psi )$
		
		\item[$cC_3$]\ \  ${\mathcal{M}}, w \models^- (\varphi {-\!\Yleft}\, \psi)$  $\; \Leftrightarrow \;$    $\forall u \geq w ({\mathcal{M}}, u \not  \models^+ \varphi \mbox{ or } {\mathcal{M}}, u
		\models^+ \psi )$
		
		\item[$cC_4$]\ \  ${\mathcal{M}}, w \models^- (\varphi {-\!\Yleft}\, \psi)$  $\; \Leftrightarrow \;$    $\forall u \geq w ({\mathcal{M}}, u \models^- \varphi \mbox{ or } {\mathcal{M}}, u \not  \models^- \psi )$
	\end{itemize}
	
	
	Now we define a weakly structural translation $\theta^{i,j}:\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}_{\mathsf{HB}}}\rightarrow\mathrm{Form}_{\mathcal{L}^{\mathord{\sim}}_{\mathsf{HB}}}$ that embeds logic $(I_i, C_j)$ into any other logic $(I_k, C_l)$, $k, l$ $\in$ $\{1, 2, 3, 4\}$.  The translation $\theta^{i,j}$ preserves propositional variables, formulas $\bot$ and $\mathord{\sim}\bot$, and commutes with binary connectives. For negated $\vee$ and $\wedge$ we have:
	
	\begin{center}
		\begin{tabular}{rcl}
			
			
			$\theta^{i,j}(\mathord{\sim} (\varphi\vee\psi))$ & $=$ & $\theta^{i,j}(\mathord{\sim}\varphi)\wedge \theta^{i,j}(\sim \psi)$ \vspace{1mm} \\
			
			$\theta^{i,j}(\mathord{\sim} (\varphi\wedge\psi))$ & $=$ & $\theta^{i,j}(\mathord{\sim}\varphi) \vee \theta^{i,j}(\sim \psi)$ 
			
		\end{tabular}
	\end{center}
	
	The most essential parts of our definition are the translation clauses for negated implication and negated coimplication. They depends on $i$ and $j$ as follows:
	
	\begin{center}
		\begin{tabular}{lcl}
			
			
			$\theta^{1,j}(\mathord{\sim} (\varphi\rightarrow\psi))$ & $=$ & $\theta^{1,j}(\varphi)\wedge \theta^{I1,Cj}(\sim \psi)$ \vspace{1mm} \\
			
			$\theta^{2,j}(\mathord{\sim} (\varphi\rightarrow\psi))$ & $=$ & $\theta^{2,j}(\varphi) \rightarrow \theta^{2,j}(\sim \psi)$ \vspace{1mm} \\
			
			$\theta^{3,j}(\mathord{\sim} (\varphi\rightarrow\psi))$ & $=$ & $\theta^{3,j}(\varphi){-\!\Yleft}\, \theta^{3,j}(\psi)$ \vspace{1mm} \\
			
			$\theta^{4,j}(\mathord{\sim} (\varphi\rightarrow\psi))$ & $=$ & $\theta^{I4,Cj}(\mathord{\sim} \psi) {-\!\Yleft}\, \theta^{4,j}(\mathord{\sim} \varphi)$ \vspace{1mm} \\
			
			
			
			$\theta^{i,1}(\mathord{\sim} (\varphi{-\!\Yleft}\, \psi))$ & $=$ & $ \theta^{i,1}(\mathord{\sim} \varphi)\vee \theta^{i,1}(\psi)$ \vspace{1mm} \\
			
			$\theta^{i,2}(\mathord{\sim} (\varphi{-\!\Yleft}\, \psi))$ & $=$ & $\theta^{i,2}(\sim \varphi)\wedge \theta^{i,2}(\psi)$ \vspace{1mm} \\
			
			$\theta^{i,3}(\mathord{\sim} (\varphi{-\!\Yleft}\, \psi))$ & $=$ & $\theta^{i,3}(\varphi) \rightarrow \theta^{i,3}(\psi)$ \vspace{1mm} \\
			
			$\theta^{i,4}(\mathord{\sim} (\varphi{-\!\Yleft}\, \psi))$ & $=$ & $\theta^{i,4}(\sim \psi)\rightarrow \theta^{i,4}(\sim \varphi)$ \\
			
		\end{tabular}
	\end{center}
	
	\begin{proposition}\label{IiCjwde} Logics $(I_i, C_j)$, $i, j \in \{1, 2, 3, 4\}$, are sn-implicative logics with DT. Moreover, $(I_i, C_j)$ and $(I_k, C_l)$ are weakly definitionally equivalent via $\theta^{i,j}$ and $\theta^{k,l}$.
	\end{proposition}
	
	\begin{proof} This statement can be proved via a natural modification of the proof of Proposition~\ref{N4Cwde}. 
	\end{proof}
	
	As above we add to the language $\mathcal{L}^{\mathord{\sim}}_{\mathsf{HB}}$ constants $\mathsf{b}$ and $\mathsf{n}$ and define the expansion $(I_i,C_j)^\mathsf{B}$  of $(I_i,C_j)$, $i,j$ $\in$ $\{ 1,2,3,4\}$, to the language $\mathcal{L}^{\mathord{\sim}}_{\mathsf{HB}}\cup\{\mathsf{b},\mathsf{n}\}$ via the  semantical clauses~\eqref{tfnb}.
	
	Similarly to $\mathsf{N4}^{\mathsf{B}}$ and $\mathsf{C}^{\mathsf{B}}$ the obtained logics are $bl$-logics.
	
	\begin{proposition}\label{IiCjbl} Logics $(I_i,C_j)^\mathsf{B}$, $i,j$ $\in$ $\{ 1,2,3,4\}$, are $bl$-logics.
	\end{proposition}
	
	Finally, analogously to Proposition~\ref{N4Cde} we obtain.
	
	\begin{proposition} Logics $(I_i,C_j)^\mathsf{B}$, $i,j$ $\in$ $\{ 1,2,3,4\}$, are definitionally equivalent. 
	\end{proposition}
		
	\section{Beth property in implicative logics with strong negation}
	In this section we pass from the mutual definability of logics to the definability of parameters in different logics. In 1953 \cite{Beth53}, W.E.~Beth proved that in classical predicate logic the implicit definability of a predicate by a theory implies that this theory defines the predicate expicitly too. Since that studying interrelations between different forms of definability became  an important branch of investigations in non-classical logics.
	
	\begin{definition} Let  $\mathsf{L}=\langle\mathcal{L},\vdash_{\mathsf{L}}\rangle$ be a logic such that $\rightarrow\in\mathcal{L}$. We say that $\mathsf{L}$ has the {\em Beth property}
		{\em (\textbf{B2})} if the following holds. For every $\mathcal{L}$-formula ${\varphi (\bar{p},q)} ={\varphi (p_1, \ldots, p_n, q)}$ if 
		\begin{equation} \{ \varphi \left( \bar{p}, q
				\right), \varphi \left( \bar{p}, q' \right) \} \vdash_{\mathsf{L}}  q
				\leftrightarrow q',
			\label{imdef}
		\end{equation} then there is an $\mathcal{L}$-formula $\psi
		(\bar{p})$ such that  \begin{equation} \{\varphi \left( \bar{p}, q \right)\} \vdash_{\mathsf{L}}
				 q \leftrightarrow \psi \left( \bar{p} \right).
			\label{exdef}	
	\end{equation} \end{definition}

	The premiss~\eqref{imdef} of {\bf B2} means that formula $\varphi (\bar{p},q)$ implicitly defines the variable $q$, i.e., it uniquely determines the truth of $q$. The conclusion~\eqref{exdef} of {\bf B2} means that the truth of $q$ is explicitly defined by formula $\psi(\bar{p})$. There is also an implicative form  {\bf B1} of Beth property, where the inference relations \eqref{imdef} and \eqref{exdef} are replaced by statements that that the implications 
	\[ (\varphi \left( \bar{p}, q
	\right) \wedge \varphi \left( \bar{p}, q' \right) ) \rightarrow ( q
	\leftrightarrow q')\ \ \text{and}\ \ \varphi \left( \bar{p}, q \right)\rightarrow (q \leftrightarrow \psi \left( \bar{p} \right))\] are {\sf L}-theorems. For logics with DT the properties {\bf B1} and {\bf B2} are obviously equivalent.  The projective Beth property {\bf PBP} assumes that $\varphi$ also contains parameters different from $\bar{p}$ and $q$. We will not consider {\bf PBP}.
	
	In 1960 \cite{Kreisel1960}, G.~Kreisel proved that every superintuintionistic logic $L$ possesses the  property \textbf{B1} (equivalent to \textbf{B2} in superintuitionistic logics).  The short proof of this theorem can be easily generalized to an arbitrary implicative logic with DT.
	
	
	
	
	\begin{theorem} Every implicative logic with DT possesses {\bf B2}. 
	\end{theorem}
	
	\begin{proof} Recall that $\{\varphi \left( \bar{p}, q
		\right),\ \varphi \left( \bar{p}, q' \right) \} \vdash_{\mathsf{L}}  q
		\leftrightarrow q'$ means that $q\rightarrow q'$ and $q'\rightarrow q$ are inferable from the set of premisses. From $\{\varphi \left( \bar{p}, q \right),\ \varphi \left( \bar{p}, q' \right) \} \vdash_{\mathsf{L}}  q
		\rightarrow q'$ by DT we obtain $\{\varphi \left( \bar{p}, q
		\right) \} \vdash_{\mathsf{L}}  \varphi \left( \bar{p}, q' \right)\rightarrow(q' \rightarrow q)$.
		Further, substituting $\top$ for $q'$ ($\top:=p_0\rightarrow p_0$) yields
		\[ \{\varphi \left( \bar{p}, q
		\right) \} \vdash_{\mathsf{L}}  \varphi \left( \bar{p}, \top \right)\rightarrow(\top \rightarrow q).\]
		From (IL1) and (IL4) we obtain  $\{\top\rightarrow q\}\vdash_{\mathsf{L}} q$. By DT, $(\top\rightarrow q)\rightarrow q\in\mathrm{Thm}(\mathsf{L})$. By (IL2) and the transitivity of inference
		\[ \{\varphi \left( \bar{p}, q
		\right) \} \vdash_{\mathsf{L}}  \varphi \left( \bar{p}, \top \right)\rightarrow q.\]
		On the other hand, from (IL3) we have $\{ q\leftrightarrow q'\}\vdash_{\mathsf{L}} \varphi \left( \bar{p}, q
		\right)\rightarrow\varphi \left( \bar{p}, q' \right)$, in particular,
		\[\{ q\leftrightarrow \top\}\vdash_{\mathsf{L}} \varphi \left( \bar{p}, q
		\right)\rightarrow\varphi \left( \bar{p},\top
		\right),\]
		From (IL5) we have $\{ q\}\vdash_{\mathsf{L}} \top\rightarrow q$ and $q\rightarrow\top\in\mathrm{Thm}(\mathsf{L})$. By monotonicity $\{ q\}\vdash_{\mathsf{L}} q\rightarrow\top$. Whence  $\{ q\}\vdash_L \varphi \left( \bar{p}, q
		\right)\rightarrow\varphi \left( \bar{p},\top
		\right)$ by transitivity of inference. Applying DT twice we obtain
		\[  \{\varphi \left( \bar{p}, q
		\right)\} \vdash_L q \rightarrow\varphi \left( \bar{p},\top
		\right).\]
	\end{proof}
	
	We say that an sn-implicative logic $\mathsf{L}$ is {\em explosive} if 
	\[ \{ p,\mathord{\sim} p\}\vdash_{\mathsf{L}} q.\]
	Now we adopt the Beth property for sn-implicative logics. Since the truth and the falsity are to some extent independent in sn-implicative logics, we replace the conclusion of~\eqref{imdef} by $q\Leftrightarrow q'$. The conclusion~\eqref{exdef} of {\bf B2} means that the truth of $q$ is explicitly defined by formula $\psi(\bar{p})$. In the case of sn-implicative logics it would be natural to replace $\psi(\bar{p})$ by a pair of formulas, one of these formulas will explicitly define the truth of $q$, while the other --- the falsity of $q$.
	
	\begin{theorem} Let  $\mathsf{L}=\langle\mathcal{L},\vdash_{\mathsf{L}}\rangle$  be an explosive sn-implicative logic with DT. For every  ${\varphi (\bar{p},q)} ={\varphi (p_1,\ldots, p_n, q)}\in\mathrm{Form}_{\mathcal{L}}$, the following holds. If \[ \{\varphi \left( \bar{p}, q
		\right),\ \varphi \left( \bar{p}, q' \right) \} \vdash_{\mathsf{L}}  q
		\Leftrightarrow q',\] then there are $\psi^+(\bar{p}),\psi^-(\bar{p})\in\mathrm{Form}_{\mathcal{L}}$ such that  
		\[ \{\varphi \left( \bar{p}, q \right)\}  \vdash_{\mathsf{L}}  q \leftrightarrow \psi^+ \left( \bar{p} \right)\ \text{and}\ \{\varphi \left( \bar{p}, q \right)\}  \vdash_{\mathsf{L}} \mathord{\sim} q \leftrightarrow \psi^- \left( \bar{p} \right).\] 
	\end{theorem}
	
	\begin{proof} For $\psi^+(\bar{p}):=\varphi(\bar{p},\top)$, we repeat the arguments from the previous proof to obtain
		\[\{\varphi \left( \bar{p}, q \right)\}  \vdash_{\mathsf{L}}  \psi^+ \left( \bar{p} \right)\rightarrow q.\] 
		Let us prove that the inverse implication is inferable from $\{\varphi \left( \bar{p}, q \right)\}$ too. By Proposition~\ref{WILRR} the weak replacement rule (WR) is derivable in $\mathsf{L}$, so we have 
		\[\{ q\Leftrightarrow q'\}\vdash_{\mathsf{L}} \varphi \left( \bar{p}, q \right)\rightarrow\varphi \left( \bar{p}, q'
		\right), \]
		in particular, $\{ q\Leftrightarrow \top\}\vdash_{\mathsf{L}} \varphi \left( \bar{p}, q \right)\rightarrow\varphi \left( \bar{p}, \top
		\right)$, i.e.,
		\[\{ q\rightarrow \top\,,\; \top \rightarrow q\,,\;\mathord{\sim} q\rightarrow \mathord{\sim}\top\,,\; \mathord{\sim}\top\rightarrow \mathord{\sim} q\}\vdash_{\mathsf{L}} \varphi \left( \bar{p}, q
		\right)\rightarrow\varphi \left( \bar{p}, \top
		\right), \]
		We just noticed that $q\rightarrow\top\in\mathrm{Thm}(\mathsf{L})$. Since $\mathsf{L}$ is explosive $\{\top,\mathord{\sim}\top\}\vdash_{\mathsf{L}}\mathord{\sim} q$ and by DT we obtain $\mathord{\sim}\top\rightarrow\mathord{\sim} q\in\mathrm{Thm}(\mathsf{L})$. In a similar way, $\{ q\}\vdash_{\mathsf{L}}\mathord{\sim} q\rightarrow \mathord{\sim}\top$.  Finally, $\{ q\}\vdash_{\mathsf{L}} \top\rightarrow q$ by (SN5). Thus, we obtain 
		\[ \{ q\}\vdash_{\mathsf{L}} \varphi \left( \bar{p}, q
		\right)\rightarrow\psi^+ \left( \bar{p} \right). \]
		Applying  DT twice we conclude that $\{\varphi \left( \bar{p}, q \right)\}  \vdash_{\mathsf{L}}  q\rightarrow\psi^+ \left( \bar{p} \right)$. 
		
		Recall that $\{\varphi \left( \bar{p}, q \right),\ \varphi \left( \bar{p}, q' \right) \} \vdash_{\mathsf{L}}  q\Leftrightarrow q'$ abbreviates four inferences, one of which is $\{\varphi \left( \bar{p}, q
		\right),\ \varphi \left( \bar{p}, q' \right) \} \vdash_{\mathsf{L}}  \mathord{\sim} q'
		\rightarrow \mathord{\sim} q$. Substituting $\mathord{\sim}\top$ for $q'$ we obtain 
		\[ \{\varphi \left( \bar{p}, q
		\right)\, ,\; \varphi \left( \bar{p}, \mathord{\sim}\top \right) \} \vdash_{\mathsf{L}}   \mathord{\sim}\mathord{\sim}\top \rightarrow\mathord{\sim} q.\]
		Since $\mathord{\sim}\mathord{\sim}\top\in\mathrm{Thm}( L)$, the application of (SN4) and DT yields
		\[ \{\varphi \left( \bar{p}, q
		\right) \} \vdash_{\mathsf{L}}    \varphi \left( \bar{p}, \mathord{\sim}\top \right) \rightarrow\mathord{\sim} q.\]
		Let us substitute $\mathord{\sim}\top$ for $q'$ in 
		$\{ q\Leftrightarrow q'\}\vdash_L \varphi \left( \bar{p}, q
		\right)\rightarrow\varphi \left( \bar{p}, q'
		\right)$. As a result we have
		\[\{ q\rightarrow \mathord{\sim}\top\,,\; \mathord{\sim}\top \rightarrow q\,,\;\mathord{\sim} q\rightarrow \mathord{\sim}\mathord{\sim}\top\,,\; \mathord{\sim}\mathord{\sim}\top\rightarrow \mathord{\sim} q\}\vdash_L \varphi \left( \bar{p}, q
		\right)\rightarrow\varphi \left( \bar{p}, \mathord{\sim}\top
		\right), \]
		From the assumption that $\mathsf{L}$ is explosive we obtain $\{  \mathord{\sim}\top\rightarrow q\,,\; \mathord{\sim} q\rightarrow \mathord{\sim}\mathord{\sim}\top) \}\subseteq\mathrm{Thm}( L)$ and  $\{\mathord{\sim} q\} \vdash_{\mathsf{L}} q\rightarrow \mathord{\sim}\top$. By (SN5) we have $\{ \mathord{\sim} q\}\vdash_{\mathsf{L}} \mathord{\sim}\mathord{\sim}\top\rightarrow \mathord{\sim} q$. In this way,
		\[ \{ \mathord{\sim} q\}\vdash_L \varphi \left( \bar{p}, q
		\right)\rightarrow\varphi \left( \bar{p}, \mathord{\sim}\top
		\right). \]
		The double application of DT yields $\{\varphi \left( \bar{p}, q \right)\}  \vdash_L  \mathord{\sim} q\rightarrow\varphi \left( \bar{p},\mathord{\sim}\top \right)$. Thus, one can choose $\varphi \left( \bar{p},\mathord{\sim}\top \right)$ as $\psi^-(\bar{p})$ .
		
	\end{proof}
	
	The explosive extension $\mathsf{N3}^{\bot}$ of Nelson's logic $\mathsf{N4}^{\bot}$ can be defined via the class of $\mathsf{N3}^{\bot}$-models $\langle W,\leq,v^+,v^-\rangle$ satisfying the condition 
	\[ v^+(p)\cap v^-(p)=\varnothing\ \text{for all}\ p\in\mathrm{Prop}.\]
	The support of truth and support of falsity relations, $\models^+$ and $\models^-$ are defined in the same way as for $\mathsf{N4}^{\bot}$. As in Proposition~\ref{N4Cwde} one can proof that $\mathsf{N3}^{\bot}$ is 
	an explosive sn-implicative logic with DT. So we can apply the previous theorem to $\mathsf{N3}^{\bot}$ as well as to every its axiomatic extension.
	
	\begin{corollary} Every axiomatic extension of the explosive Nelson's logic $\mathsf{N3}^{\bot}$ satisfies Theorem~16.
	\end{corollary}
	
	\section{Conclusion}
	
	We just started the investigation of sn-implicative logics, so there is a sense to mention some  questions for subsequent studies.  The first group of questions concerns the algebraizability of sn-implicative logics.
	
	\begin{itemize}
		\item Is it possible given an sn-implicative logic $L$ to define a class of algebras $\mathcal{K}$ such that $ L$ is algebraizable with respect to $\mathcal{K}$ with the equivalence formulas $\{ p\Leftrightarrow q\}$ and the defining identity $p\rightarrow p= p$?
		
		\item Is it possible to obtain a sort of twist-structure presentation (see \cite{Odintsov04}) for algebraic models of sn-implicative logics?
		
		\item In \cite{OdSp2020}, it was proved that the lattice of axiomatic extensions of $\mathsf{N4^B}$ is isomorphic to the lattice of superintuitionistic logics. Is it possible to prove an analog of this statement for arbitrary $bl$-logics?
	\end{itemize}
	
	Naturally, one can formulate numerous questions concering the investigation of different versions of definability and interpolation in sn-implicative logics. We mention only two of them.				
	
	\begin{itemize}
		
		\item To which extend one can weaken the assumption of Theorem~16 preserving the truth of its conclusion?
		
		\item Classical regular logics defined in \cite[Sec.~7.1]{GabbayMaximova2005} have a remarkable property: the Craig interpolation property and the Beth property {\bf B1} are equivalent in this class of logics. Is it possible to define a version of classical regular logics with strong negation so that the Craig interpolation property and the Beth property {\bf B1} (or some natural analogs of these properties) are equivalent for such logics?
		
	\end{itemize}
	
	
		
	
	
	
	\bigskip
	\begin{thebibliography}{99} % Ссылки на литературу приводятся только на английском языке (даже если у источника нет англоязычной версии).
		
		
		\bibitem{AlmukdadNelson}
		A.~Almukdad, D.~Nelson, \href{https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/constructible-falsity-and-inexact-predicates/DC5A36D5D9E46F77472087F2C837BBC6}{\em Constructible falsity and inexact predicates}, Journal of Symbolic Logic, \textbf{49} (1984), 231--233.
		
		\bibitem{ArieliAvron1996} %
		O.~Arieli, A.~Avron, \href{https://www.jstor.org/stable/40180088}{\em Reasoning with logical bilattices}, Journal of Logic, Language and Information, \textbf{5}:1 (1996), 25--63.
		
		\bibitem{Beth53}
		W.E.~Beth, \href{https://www.sciencedirect.com/science/article/abs/pii/S1385725853500423}{\em On Padoa's method in the theory of definition}, Indagationes Mathematicae, \textbf{15} (1953), 330--339.
		
		\bibitem{BlokPigozzi}
		W.J.~Blok,  D.~Pigozzi, {\em Algebraizable logics}, Providence: A.M.S., 1989.
		
		\bibitem{Buisman07}
		L.~Buisman, R.~Gor\'e, \href{https://link.springer.com/chapter/10.1007/978-3-540-73099-6_9}{\em A Cut-Free Sequent Calculus for Bi-intuitionistic Logic}, N.~Olivetti (ed.) {\em TABLEAUX 2007}, LNAI 4548, Springer-Verlag, Berlin, 2007, 90--106.
		
		\bibitem{burris1981course}
		S.~Burris,  H.P.~Sankappanavar, \href{https://link.springer.com/book/9781461381327}{\em A course in universal algebra}, Springer-Verlag, 1981.
		
		
		\bibitem{Crolard01}
		V.~Crolard, \href{https://www.sciencedirect.com/science/article/pii/S0304397599001243}{\em Subtractive logic}, Theoretical Computer Science, \textbf{254} (2001), 151--185.
		
		\bibitem{FazOd2024}
		D.~Fazio, S.P.~Odintsov, \href{https://link.springer.com/article/10.1007/s11225-023-10057-2}{\em An Algebraic Investigation of the Connexive Logic $\mathsf{C}$}, Studia Logica, \textbf{112} (2024), 37--67.
		
		\bibitem{Font16}
		J.~Font, \href{https://www.collegepublications.co.uk/logic/mlf/?00026}{\em Abstract Algebraic Logic: An Introductory Textbook}, College Publications, 2016.
		
		\bibitem{GabbayMaximova2005}
		D.~Gabbay,  L.~Maksimova, \href{https://global.oup.com/academic/product/interpolation-and-definability-9780198511748?cc=ru&lang=en&}{\em Interpolation and Definability}, Oxford Science Publication, Oxford, 2005.
		
		\bibitem{Gyuris99} %
		V.~Gyuris,  {\em Variations of Algebraizability},  PhD thesis, The University of Illinois at Chicago, 1999.
		
		\bibitem{Kreisel1960}
		G.~Kreisel,  {\em Explicit definability in intuitionistic logic}, The Journal of Symbolic Logic, \textbf{25} (1960), 389--390.
		
				
		\bibitem{McKenMcNulTayl87}
		R.N.~McKenzie, G.F.~McNulty, W.F.~Taylor, {\em Algebras, Lattices, Varieties, vol. 1}, Wadsworth \& Brooks/Cole, Monterey, California, 1987.
		
		\bibitem{Nelson49} 
		D.~Nelson, \href{https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/constructible-falsity/3FACF8D0777593E0B3516678E65BAB55}{\em Constructible falsity}, Journal of Symbolic Logic, \textbf{14} (1949), 16--26.
		
			
		\bibitem{Odintsov04} 
		S.P.~Odintsov, \href{https://link.springer.com/article/10.1023/B:STUD.0000032104.14199.08}{\em On the representation of {\bf N4}-lattices}, Studia Logica, \textbf{76}:3 (2004), 385--405.
		
		\bibitem{Odintsov05} 
		S.P.~Odintsov, \href{https://link.springer.com/article/10.1007/s11225-005-8472-9}{\em The class of extensions of Nelson's paraconsistent logic}, Studia Logica, \textbf{80}:2--3 (2005), 291--320.
				
		\bibitem{OdSkWans19} 		
		S.~Odintsov, D.~Skurt,  H.~Wansing, \href{https://apcz.umk.pl/LLP/article/view/LLP.2019.010}{\em On Definability of Connectives and Modal Logics over {\sf FDE}}, Logic and Logical Philosophy, \textbf{28} (2019), 631--659.
		
		\bibitem{OdSp2020}
		S.P.~Odintsov,  S.O.~Speranski, \href{https://www.cambridge.org/core/journals/review-of-symbolic-logic/article/belnapdunn-modal-logics-truth-constants-vs-truth-values/B67AEA04085BDCCD8F90ABC859645813}{\em Belnap-Dunn modal logics: thruth constants versus truth values}, The Review of Symbolic Logic, \textbf{13}:2 (2020), 416--435. 
		
		\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 {\sf FDE}-based Paraconsistent Modal Logics}, Studia Logica,  \textbf{105}:6 (2017), 1221–-1254.
			
		
		\bibitem{Rasiowa}
		H.~Rasiowa, \href{https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/78/suppl/C}{\em An Algebraic Approach to Non-Classical Logics}, Amsterdam, Netherlands: Warszawa, PWN - Polish Scientific Publishers, 1974.
		
		\bibitem{Rauszer74}
		C.~Rauszer, \href{https://link.springer.com/article/10.1007/BF02120864}{\em A formalization of the propositional calculus of H-B logic}, Studia Logica, \textbf{33} (1974), 23--34.
		
		
		\bibitem{Rauszer77} 
		C.~Rauszer, \href{https://link.springer.com/article/10.1007/BF02121115}{\em Applications of Kripke models to Heyting-Brouwer logic}, Studia Logica, \textbf{36} (1977), 61--72.
		
		\bibitem{RJJ}
		U.~Rivieccio, A.~Jung,   R.~Jansana, \href{https://academic.oup.com/logcom/article-lookup/doi/10.1093/logcom/exv038?__cf_chl_rt_tk=xn1cBXIO8sYZL_cEiCZotSe7ZzvU.Mt5X4y8rjrZHxs-1770624973-1.0.1.1-n.qAWFmO0W6xt4k20Qf6MrPTO.FgXkhkk_WJiHONjCM}{\em Four-valued modal logic: Kripke semantics and duality}, Journal of Logic and Computation, \textbf{27}:1 (2017), 155--199.
		
			
		\bibitem{SpVer08} 
		M.~Spinks,  R.~Veroff, \href{https://link.springer.com/article/10.1007/s11225-008-9138-1}{\em Constructive logic with strong negation is a substructural logic. II}, Studia Logica, \textbf{89} (2008), 401–-425.
		
		\bibitem{SpV16}  
		M.~Spinks,  R.~Veroff, \href{https://link.springer.com/chapter/10.1007/978-3-319-74772-9_13}{\em Paraconsistent constructive logic with strong negation is a contraction-free relevant logic}, J. Czelakowski (ed.), Don Pigozzi on abstract
			algebraic logic and universal algebra, Springer, Dordrecht, 2018, 323--379.
		
		\bibitem{Wansing2005}
		H.~Wansing, {\em Connexive Modal Logic}, R. Schmidt \emph{et al.}~(eds.), Advances in Modal Logic. V.~5, King's College Publications, 2005, 367--383.
		
		\bibitem{Wansing08}
		H.~Wansing, \href{https://www.tandfonline.com/doi/abs/10.3166/jancl.18.341-364}{\em Constructive negation, implication, and co-implication}, Journal of Applied Non-Classical Logics, \textbf{18} (2008), 341--364.
		
		\bibitem{Wolter98}
		F.~Wolter, \href{https://link.springer.com/article/10.1023/A:1004218110879}{\em On Logics with Coimplication}, Journal of Philosophical Logic, \textbf{27} (1998), 353--387.
		
	
		
	\end{thebibliography}
\end{document}

