\documentclass[10pt,a4paper]{amsart}

%Russian-specific packages
%--------------------------------------
\usepackage[T2A]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
%--------------------------------------

%Math packages
%--------------------------------------
\usepackage{hyperref}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{array} %for hilbert-style derivations
\usepackage{bussproofs} %for proofs
\usepackage{color}
\usepackage{float} %for positioning tables
\usepackage{mathrsfs}  %for \mathscr{...}
%--------------------------------------

%Theorems, definitions, etc.
%--------------------------------------
\newtheorem{Prop}{Proposition}[section]
\newtheorem{Lemm}[Prop]{Lemma}
\newtheorem{Theo}[Prop]{Theorem}
\newtheorem{Coro}[Prop]{Corollary}
\newtheorem{Folk}[Prop]{Folklore}

\theoremstyle{definition}
\newtheorem{Rem}[Prop]{Remark}
%--------------------------------------

%Commands
%--------------------------------------
\newcommand{\F}{\mathrm{Form}}
\newcommand{\R}{\mathrel{R}}
%--------------------------------------
%--- redefining enumi
\newcommand{\enumialph}{\renewcommand{\theenumi}{\alph{enumi}}}
\newcommand{\enumiAlph}{\renewcommand{\theenumi}{\Alph{enumi}}}
\newcommand{\enumiroman}{\renewcommand{\theenumi}{\roman{enumi}}}
\newcommand{\enumiRoman}{\renewcommand{\theenumi}{\Roman{enumi}}}
%---
%--------------------------------------
%--- hilbert-style derivations
\newcounter{rowcount}
\newcolumntype{T}{>{\small \ttfamily}l}
\newenvironment{hilbert}{ \setcounter{rowcount}{0}%
  \begin{center}
    \begin{tabular}{@{\stepcounter{rowcount} \makebox[3em][r]{\small \ttfamily \therowcount}\hspace*{\tabcolsep}}|l|T} %\hspace*{\tabcolsep}
 }
{\end{tabular} \end{center}}
%---
%--------------------------------------

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

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

\def\semrtop
     {
  \vbox{
     \noindent\logo
     \hspace{80mm}\raisebox{1ex}{ISSN 1813-3304 }

     \vspace{5mm}

     \begin{center}
     {\huge СИБИРСКИЕ \ ЭЛЕКТРОННЫЕ} \\[2mm]  %Headings in Russian
     {\huge МАТЕМАТИЧЕСКИЕ ИЗВЕСТИЯ} \\[2mm]
     {\large Siberian Electronic Mathematical Reports} \\[1mm]
     {\LARGE\tt{http://semr.math.nsc.ru}}\\[0.5mm]
%     {\small Институт математики им. С.Л.Соболева СО РАН}\\[-1mm]
%     {\small Sobolev Institute of Mathematics SB RAS}
     \end{center}
     \vspace{-3mm}
     \noindent
     \begin{tabular}{c}
     \hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} \\
     \hline\hline
     \end{tabular}

     \vspace{1mm}
     {\flushleft\it Том 19, стр.\ 1--15 (2022) \hspace{65mm}{\rm\small УДК \udcs}} %Volume, pages in Russian,
                                                                                    %filled by Editorial board
     \newline
         {\rm\small DOI~10.33048/semi.2022.19.xxx}\hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa}{\rm\small MSC\ \ \mscs}
  }%\vbox
}
%--------------------------------------

%%%

\begin{document}
\renewcommand{\refname}{References}
\renewcommand{\proofname}{Proof.}
%\renewcommand{\figurename}{Fig.}
\renewcommand{\tablename}{Table}

\thispagestyle{empty}

%

\title[Some remarks on Do\v{s}en's logic $\mathsf{N}$ and its extensions]{Some remarks on Do\v{s}en's logic $\mathsf{N}$\linebreak and its extensions}
\author{{S.\,O.\ Speranski}}%
\address{Stanislav O.\ Speranski
\newline\hphantom{iii} Steklov Mathematical Institute of Russian Academy of Sciences,
\newline\hphantom{iii} 8, Gubkina St.,
\newline\hphantom{iii} Moscow, 119991, Russia}%
\email{katze.tail@gmail.com}%

\thanks{\sc Speranski, S.\,O.,
Some remarks on Do\v{s}en's logic $\mathsf{N}$ and its extensions}
\thanks{\copyright \ 2022 Speranski S.\,O}
\thanks{\rm This work was supported by the Russian Science Foundation under grant no.\ 21-11-00318.}
\thanks{\it Received  March, 20, 2022, published  July, 11,  2022.}%

\semrtop \vspace{1cm}
\maketitle {\small
\begin{quote}
\noindent{\sc Abstract.} This paper collects some observations about Do\v{s}en's logic $\mathsf{N}$, where negation is treated as a modal operator, and its extensions. We shall see what happens when we add the~contraposition axiom to several important extensions of $\mathsf{N}$, show that certain extensions of $\mathsf{N}$ are canonical, and also revisit the method of filtration.\medskip

\noindent{\bf Keywords:} modal negation, intuitionistic modal logic, Heyting--Ockham logic, Hype, Routley star.
 \end{quote}
}

%

%\tableofcontents

%%%

\section{Introduction}

Do\v{s}en's logic $\mathsf{N}$, proposed in \cite{Dosen-1986}, enriches the positive fragment of intuitionistic logic by adding a negative modality, which is weaker than the negation of Jo\-hans\-son's minimal logic. (For information about quantified versions of logics containing $\mathsf{N}$, the reader may consult \cite{Speranski-2020}.)
Among the interesting extensions of $\mathsf{N}$ are the logics $\mathsf{N}^\ast$ and $\mathsf{Hype}$. The former was introduced in \cite{Cabalar-Odintsov-Pearse-2006} in the course of developing a framework for the study of logic programs with negation. The latter has been advocated in \cite{Leitgeb-2019} as a system suitable for dealing with `hy\-per\-in\-ten\-si\-o\-nal' contexts, but was first described in \cite{Moisil-1942}; the reader may consult \cite{Odintsov-Wansing-2021} for further discussion. Following \cite{Speranski-2020}, we shall write $\mathsf{N}^\bullet$ instead of $\mathsf{Hype}$. Note that $\mathsf{N}^\bullet$ extends $\mathsf{N}^\ast$.

While the system for $\mathsf{N}$ employs the contraposition rule, the corresponding scheme
\[
\left( \phi \rightarrow \psi \right) \rightarrow \left( {\neg \psi} \rightarrow {\neg \phi} \right)
\] \pagebreak
cannot be derived even in $\mathsf{N}^\bullet$. In Section~\ref{section:contra} we shall see what happens when we add the above scheme to some important extensions of $\mathsf{N}$.\footnote{The writing of this section has been partially motivated by a question of Dick de Jongh~(pri\-va\-te com\-mu\-ni\-cation): he asked about extending $\mathsf{N}$ by adding the scheme
\begin{equation*}
{\left( \phi \leftrightarrow \psi \right) \rightarrow \left( {\neg \phi} \leftrightarrow {\neg \psi} \right)}
\tag{$\star$} \label{scheme:E}
\end{equation*}
--- which is the same as adding ${{\neg \phi} \wedge {\neg \psi}} \rightarrow {\neg \left( \phi \vee \psi \right)}$ to the system of `subminimal logic' studied in \cite{Bezhanishvili-Colacito-de-Jongh-2019} (see also \cite{Hazen-1995}). Among other things, we shall derive the contraposition scheme from (\ref{scheme:E}) over $\mathsf{N}$.}
In Section~\ref{section:canonical} we shall prove that certain extensions of $\mathsf{N}$~--- which are obtained by adding various schemes involved in the definitions of $\mathsf{N}^\ast$ and $\mathsf{N}^\bullet$ --- are canonical. In Section~\ref{section:filtration} we shall revisit the method of filtration, which was used in \cite{Drobyshevich-Odintsov-2013} to establish the decidability of $\mathsf{N}$ and $\mathsf{N}^\ast$. This will lead to further decidability results.

It should be noted that these remarks are
inspired %largely
by the work of K.\ Do\v{s}en and that of S.\ Odintsov, and are intended to~complement \cite{Dosen-1986}, \cite{Odintsov-2010}, \cite{Drobyshevich-Odintsov-2013} and \cite{Odintsov-Wansing-2021}. {The technique used in the paper is quite simple, but the results may be of interest to those working in~non-classical logics.}

%%%

%\pagebreak
\section{Preliminaries}

Fix once and for all a countable set $\mathrm{Prop}$ of \emph{propositional variables}. The syntax of $\mathsf{N}$ is exactly the same as that of intuitionistic logic; so the \emph{connective symbols} are $\rightarrow$, $\wedge$, $\vee$ and $\neg$. However, one should bear in mind that
\begin{quote}
{\slshape in the semantics of $\mathsf{N}$, $\neg$ will be interpreted as a negative modal operator, and thus many intuitionistic principles involving $\neg$ will not be valid.}
\end{quote}
Denote by $\F$ the collection of all formulas~--- i.e.\ the set of all expressions that can be built up from $\mathrm{Prop}$ using the connective symbols. We treat $\leftrightarrow$ as defined in the obvious way, viz.
\[
{\phi \leftrightarrow \psi}\ :=\
{\left( \phi \rightarrow \psi \right) \wedge \left( \phi \rightarrow \psi \right)} .
\]
For convenience, when concerned only with non-empty sets of formulas, we shall abbreviate the condition `$\Delta \ne \varnothing$ and $\Delta \subseteq \F$' as $\Delta \sqsubseteq \F$.

%%

%\pagebreak
\subsection{The logics $\mathsf{N}$, $\mathsf{N}^\circ$, $\mathsf{N}^\ast$ and $\mathsf{N}^\bullet$}

The Hilbert-type system for $\mathsf{N}$ was described in \cite{Dosen-1986}. It employs the following axiom schemes:
\begin{itemize}

\item[$\mathtt{I1}$.]
$\phi \rightarrow \left( \psi \rightarrow \phi \right)$;

\item[$\mathtt{I2}$.]
$\left( \phi \rightarrow \left( \psi \rightarrow \theta \right) \right) \rightarrow
\left( \left( \phi \rightarrow \psi \right) \rightarrow \left( \phi \rightarrow \theta \right) \right)$;

\item[$\mathtt{C1}$.]
$\phi \wedge \psi \rightarrow \phi$;

\item[$\mathtt{C2}$.]
$\phi \wedge \psi \rightarrow \psi$;

\item[$\mathtt{C3}$.]
$\phi \rightarrow \left( \psi \rightarrow {\phi \wedge \psi} \right)$;

\item[$\mathtt{D1}$.]
$\phi \rightarrow \phi \vee \psi$;

\item[$\mathtt{D2}$.]
$\psi \rightarrow \phi \vee \psi$;

\item[$\mathtt{D3}$.]
$\left( \phi \rightarrow \theta \right) \rightarrow
\left( \left( \psi \rightarrow \theta \right) \rightarrow \left( {\phi \vee \psi} \rightarrow \theta \right) \right)$;

\item[$\mathtt{N}$.]
${{\neg \phi} \wedge {\neg \psi}} \rightarrow {\neg \left( \phi \vee \psi \right)}$.

\end{itemize}
Thus we have the `positive' axioms of intuitionistic logic plus all instances of $\mathtt{N}$. It also employs two inference rules:
\begin{itemize}

\item[$\mathtt{MP}$.] \emph{modus ponens}, i.e.\
\begin{prooftree}
\def\fCenter{\rightarrow}
\AxiomC{$\phi$}
\AxiomC{$\phi \rightarrow \psi$}
\RightLabel{;}
\BinaryInfC{$\psi$}
\end{prooftree}

\item[$\mathtt{CR}$.] the \emph{contraposition rule}, which is rendered as
\begin{prooftree}
\def\fCenter{\rightarrow}
\Axiom$\phi \fCenter \psi$
\RightLabel{.}
\UnaryInf${\neg \psi} \fCenter {\neg \phi}$
\end{prooftree}

\end{itemize}
Note that if we think of $\neg$ as an impossibility operator, then $\mathtt{CR}$ can be viewed as a modal rule. Clearly, $\neg$ is weaker than intuitionistic negation, and even minimal negation.

Now let $\mathsf{N}$ denote the least set of formulas containing the axioms of our calculus and closed under its rules of inference. For each $\Gamma \subseteq \F$, take
\[
{\mathrm{Disj} \left( \Gamma \right)}\ :=\
{\left\{
{\phi_0 \vee \ldots \vee \phi_n} \mid
{n \in \mathbb{N}} ~ \text{and} ~ \phi_0, \ldots, \phi_n \in  \Gamma
\right\}} .\footnotemark
\]
Given $\Gamma \subseteq \F$ and $\Delta \sqsubseteq \F$, we write $\Gamma \vdash \Delta$ iff some element of $\mathrm{Disj} \left( \Delta \right)$ can be obtained from elements of $\Gamma \cup \mathsf{N}$ by means of $\mathtt{MP}$. As may be expected, $\phi \vdash \Delta$ and \mbox{$\Gamma \vdash \phi$} abbreviate $\left\{ \phi \right\} \vdash \Delta$ and $\Gamma \vdash \left\{ \psi \right\}$ respectively. Exactly as in in\-tu\-i\-ti\-o\-n\-is\-tic logic, one can prove:

\footnotetext{When
$n = 0$, we have $\phi_0 \vee \ldots \vee \phi_n = \phi_0$. Thus $\mathrm{Disj} \left( \Gamma \right)$ contains non-empty disjunctions only.}

%

\begin{Theo}[see \cite{Dosen-1986}] \label{Deduction_Theorem} %Deduction Theorem
For any $\Gamma \subseteq \F$ and $\phi, \psi
\in \F$,
\[
{\Gamma \cup \left\{ \phi \right\} \vdash \psi}
\quad \Longleftrightarrow \quad
{\Gamma \vdash \phi \rightarrow \psi} .
\]
\end{Theo}

%

Here is another simple but useful observation.

\begin{Theo}[see \cite{Dosen-1986}] \label{Replacement} %Replacement
Let $\left\{ \phi, \psi, \psi' \right\} \subseteq \F$, and suppose that $\phi'$ is obtained from $\phi$ by replacing some occurrence of $\psi$ by $\psi'$. Then $\vdash \psi \leftrightarrow \psi'$ implies $\vdash \phi \leftrightarrow \phi'$.
\end{Theo}

\begin{proof}
By induction on the complexity of $\phi$.

The case where $\phi \in \mathrm{Prop}$ is trivial. %In case $\phi$ is in $\mathrm{Prop}$ the result is immediate.

Suppose $\phi = \neg \theta$. The result then follows by the inductive hypothesis and $\mathtt{CR}$.

The other cases can be handled as in intuitionistic logic.
\end{proof}

%

Evidently, for any $\phi, \psi \in \F$ we have $\vdash \left( \phi \rightarrow \phi \right) \leftrightarrow \left( \psi \rightarrow \psi \right)$; thus by The\-o\-rem~\ref{Replacement}, $\phi \rightarrow \phi$ and $\psi \rightarrow \psi$ are practically interchangeable. Denote
\[
\top\ :=\ {\phi_\circ \rightarrow \phi_\circ}
\quad \text{and} \quad
\bot\ :=\ {\neg \top}
\]
where $\phi_\circ$ is a fixed formula. We shall occasionally abbreviate $\phi \rightarrow \bot$ to
$- \phi$. One may think of $-$ as intuitionistic negation provided that $\bot$ behaves as the falsum.

%

In this article by a (\emph{normal})
\emph{logic} we mean a superset of $\mathsf{N}$ closed under $\mathtt{MP}$, $\mathtt{CR}$ and substitutions. Given a logic $L$, we define
\[
{\Gamma \vdash_L \Delta}
\quad : \Longleftrightarrow \quad
{L \cup \Gamma \vdash \Delta} .
\]
Thus Theorems~\ref{Deduction_Theorem} and \ref{Replacement} %as well as many results below
generalise readily to extensions of $\mathsf{N}$. If $L$ is a logic and $\mathtt{S}_1$, \ldots, $\mathtt{S}_n$ are formula schemes, we write $L + \left\{ \mathtt{S}_1, \ldots \mathtt{S}_n \right\}$ for the least logic containing $L$ and all instances of $\mathtt{S}_1$, \ldots, $\mathtt{S}_n$. Here are examples of extra schemes:
\begin{itemize}

\item[$\mathtt{N1}^\circ$.]
${\neg \left( \phi \rightarrow \phi \right)} \rightarrow \psi$;

\item[$\mathtt{N2}^\circ$.]
$\neg {\neg \left( \phi \rightarrow \phi \right)}$;
%instead of $\neg \left( \left( \phi \rightarrow \phi \right) \rightarrow {\neg \left( \psi \rightarrow \psi \right)} \right)$

\item[$\mathtt{N}^\ast$.]
$\neg \left( \phi \wedge \psi \right) \rightarrow {\neg \phi} \vee {\neg \psi}$;

\item[$\mathtt{N1}^\bullet$.]
$\phi \rightarrow {\neg \neg \phi}$;

\item[$\mathtt{N2}^\bullet$.]
${\neg \neg \phi} \rightarrow \phi$.

\end{itemize}
They can be used to define three important extensions of $\mathsf{N}$:
\begin{align*}
\mathsf{N}^\circ\
&:=\ {\mathsf{N} + \left\{ \mathtt{N1}^\circ, \mathtt{N2}^\circ \right\}} ;\\
\mathsf{N}^\ast\
&:=\ {\mathsf{N}^\circ + \left\{ \mathtt{N}^\ast \right\}} ;\\
\mathsf{N}^\bullet\
&:=\ {\mathsf{N}^\ast + \left\{ \mathtt{N1}^\bullet, \mathtt{N2}^\bullet \right\}} .
\end{align*}
It is known that $\mathsf{N}^\circ$ is the least logic in which $\bot$ behaves as the falsum; see \cite{Speranski-2020}. Next, $\mathsf{N}^\ast$ was introduced in \cite{Cabalar-Odintsov-Pearse-2006} and studied further in \cite{Odintsov-2010,Drobyshevich-Odintsov-2013}. Finally, $\mathsf{N}^\bullet$ has been advocated in \cite{Leitgeb-2019}, but it was first described in \cite{Moisil-1942}; consult \cite{Odintsov-Wansing-2021} for discussion.\footnote{In
\cite{Leitgeb-2019}, $\mathsf{N}^\bullet$ was presented in a slightly different language: $\top$ was treated as primitive, rather than defined. So formally speaking, the system for $\mathsf{N}^\bullet$ as given above is a definitional variant of that in \cite{Leitgeb-2019}.}
Here are a few useful observations:
\begin{itemize}

\item the converses to $\mathtt{N}$ and $\mathtt{N}^\ast$ are derivable in $\mathsf{N}$, even without $\mathtt{N}$;

\item $\mathtt{N}$, $\mathtt{N1}^\circ$, $\mathtt{N2}^\circ$ and $\mathtt{N}^\ast$ are redundant~--- i.e.\ derivable from the other axioms~--- in $\mathsf{N}^\bullet$.

\end{itemize}
See \cite{Speranski-2020} for the details.

%

While the rule $\mathtt{CR}$ is obviously admissible in each extension of $\mathsf{N}$, it is~not de\-ri\-v\-a\-ble even in $\mathsf{N}^\bullet$, let alone $\mathsf{N}$ and $\mathsf{N}^\ast$~--- this can be shown using the corresponding pos\-si\-b\-le world semantics; see \cite{Odintsov-2010}. The same applies to the rule
\begin{prooftree}
\def\fCenter{\leftrightarrow}
\Axiom$\phi \fCenter \psi$
\RightLabel{.}
\UnaryInf${\neg \psi} \fCenter {\neg \phi}$
\end{prooftree}
In other words, the following schemes are not derivable in $\mathsf{N}^\bullet$:
\begin{itemize}

\item[$\mathtt{C}$.] $\left( \phi \rightarrow \psi \right) \rightarrow \left( {\neg \psi} \rightarrow {\neg \phi} \right)$;

\item[$\mathtt{E}$.] $\left( \phi \leftrightarrow \psi \right) \rightarrow \left( {\neg \psi} \leftrightarrow {\neg \phi} \right)$.

\end{itemize}
Interestingly enough, $\mathtt{C}$ and $\mathtt{E}$ turn out to be equivalent, i.e.\ derivable from each other over the basic logic $\mathsf{N}$.

\begin{Prop} \label{Prop-Repl}
Let $L$ be a logic. Then $L + \left\{ \mathtt{C} \right\}$ coincides with $L + \left\{ \mathtt{E} \right\}$.
\end{Prop}

\begin{proof}
Clearly, it suffices to show that $\mathtt{C}$ is derivable in $\mathsf{N} + \left\{ \mathtt{E} \right\}$. For convenience, let $\mathsf{L}$ denote $\mathsf{N} + \left\{ \mathtt{E} \right\}$. Observe that ${\phi \rightarrow \psi} \vdash_{\mathsf{L}} {\neg \psi} \rightarrow {\neg \phi}$:
\begin{hilbert}
$\phi \rightarrow \psi$
&{hypothesis}\\
$\left( \phi \rightarrow \psi \right) \rightarrow \left( \left( \phi \vee \psi \right) \leftrightarrow \psi \right)$
&{positive intuitionistic logic}\\
$\left( \phi \vee \psi \right) \leftrightarrow \psi$
&from 1, 2\\
$\left( \left( \phi \vee \psi \right) \leftrightarrow \psi \right) \rightarrow \left( {\neg \left( \phi \vee \psi \right)} \leftrightarrow {\neg \psi} \right)$
&$\mathtt{E}$\\
${\neg \left( \phi \vee \psi \right)} \leftrightarrow {\neg \psi}$
&from 3, 4\\
$\left( {\neg \phi} \wedge {\neg \psi} \right) \leftrightarrow {\neg \left( \phi \vee \psi \right)}$
&$\mathsf{N}$\\
$\left( {\neg \phi} \wedge {\neg \psi} \right) \leftrightarrow {\neg \psi}$
&from 6, 5\\
$\left( \left( {\neg \phi} \wedge {\neg \psi} \right) \leftrightarrow {\neg \psi} \right) \rightarrow
\left( {\neg \psi} \rightarrow {\neg \phi} \right)$
&{positive intuitionistic logic}\\
${\neg \psi} \rightarrow {\neg \phi}$
&from 7, 8.
\end{hilbert}
By the deduction theorem for $\mathsf{L}$, this gives us $\mathtt{C}$.
\end{proof}

One may wonder what happens if we add $\mathtt{C}$ to a given logic. Some natural ex\-am\-p\-les will be discussed in Section~\ref{section:contra}.

%%%

%\pagebreak
\subsection{Do\v{s}en-style semantics} %Routley-style
\label{subsection-ds-semantics}

As in \cite{Dosen-1986}, by a \emph{frame} we mean a triple $\mathcal{W} = \langle W, \leqslant,\linebreak \R \rangle$ where $W$ is a non-empty set, $\leqslant$ is a pre\-or\-de\-r\-ing on $W$, and $R$ is a binary re\-la\-ti\-on on $W$ such that
\[
{{\leqslant \circ \R}}\ \subseteq\ {{\R \circ \leqslant^{-1}}} .\footnotemark
\]
Given $\mathcal{W}$, we call $\xi: \mathrm{Prop} \rightarrow \mathcal{P} \left( W \right)$ a \emph{valuation in $\mathcal{W}$} iff for any $p \in \mathrm{Prop}$ and $x, y \in W$, \footnotetext{Here $\circ$ and ${\,\cdot\,}^{-1}$ denote the composition operation and the inverse operation respectively.}
\[
x\ \in\ {\xi \left( p \right)}
\quad \text{and} \quad
x\ \leqslant\ y
\quad \Longrightarrow \quad
y\ \in\ {\xi \left( p \right)} ,
\]
i.e.\ the $\xi \left( p \right)$'s are upward closed. By a \emph{model} we mean a pair $\mathcal{M} = \langle \mathcal{W}, \xi \rangle$ where $\mathcal{W}$ is a frame and $\xi$ is a valuation in $\mathcal{W}$. Now $\mathcal{M}, x \Vdash \phi$ is defined exactly as in intuitionistic logic, except for the negation clause:
\[
\mathcal{M}, x \Vdash {\neg \psi}
\quad :\Longleftrightarrow \quad
\mathcal{M}, y \nVdash \psi \quad \text{for all} \enskip {y \in R \left( x \right)} .\footnotemark
\]
When there is no ambiguity, we shall drop $\mathcal{M}$ and write $x \Vdash \phi$ instead of $\mathcal{M}, x \Vdash \phi$. Naturally, $\mathcal{M}, x \Vdash \phi$ is read \emph{$\phi$ is true at $x$ in $\mathcal{M}$}. Also define: \footnotetext{Here $R \left( u \right)$ denotes the image of $\left\{ u \right\}$ under $R$, i.e.\ $\left\{ v \in W \mid  u R v \right\}$.}
\begin{itemize}

\item $\mathcal{M} \Vdash \phi$ iff $\mathcal{M}, x \Vdash \phi$ for all $x \in W$;

\item $\mathcal{W} \Vdash \phi$ iff $\mathcal{M} \Vdash \phi$ for all models $\mathcal{M}$ based on $\mathcal{W}$.

\end{itemize}
These %notations
are read \emph{$\phi$ is true in $\mathcal{M}$} and \emph{$\phi$ is valid in $\mathcal{W}$} respectively.

%

\begin{Lemm}[see \cite{Dosen-1986}] \label{Lemm-heredity}
Let $\mathcal{M}$ be a model. Then for any $\phi \in \F$ and $x, y \in W$,
\[
\mathcal{M}, x \Vdash \phi
\quad \text{and} \quad
x \leqslant y
\quad \Longrightarrow \quad
\mathcal{M}, y \Vdash \phi .
\]
More informally, it means that $\Vdash$ is intuitionistically hereditary.
\end{Lemm}

%

As in modal logic, some of the formulas correspond to frame properties. For in\-stan\-ce, $\bot$ is valid in $\mathcal{W}$ iff $R = \varnothing$. For a more interesting example, consider the principle of weak excluded middle, which can be represented as the formula scheme
\begin{itemize}

\item[$\mathtt{WEM}$.]
${\neg \phi} \vee {\neg {\neg \phi}}$.

\end{itemize}
As was shown in \cite{Dosen-1986}, it corresponds to a rather complicated property:
\begin{multline*}
\qquad
\mathcal{W} \Vdash {{\neg p} \vee {\neg {\neg p}}}
\quad \Longleftrightarrow \quad\\
{\forall x}\, {\forall y}\, {\forall z}\, {\left( {R \left( x, y \right)} ~ \& ~ {R \left( x, z \right)} \Rightarrow {\exists u}\, {\left( {R \left( y, u \right)} ~ \& ~ {z \leqslant u} \right)} \right)} .
\qquad
\end{multline*}
Here is yet another example.

%

\begin{Prop}
For every frame $\mathcal{W}$,
\begin{multline*}
\qquad
\mathcal{W} \Vdash {\neg \left( p \wedge q \right) \rightarrow {\neg p} \vee {\neg q}}
\quad \Longleftrightarrow \quad\\
{\forall x}\, {\forall y}\, {\forall z}\, {\left( {R \left( x, y \right)} ~ \& ~ {R \left( x, z \right)} \Rightarrow {\exists u}\, {\left( {R \left( x, u \right)} ~ \& ~ {y \leqslant u} ~ \& ~ {z \leqslant u} \right)} \right)} .
\qquad
\end{multline*}
Thus the scheme $\mathtt{N}^\ast$ corresponds to the property on the right-hand side.
\end{Prop}

\begin{proof}
For convenience, denote by ($\star$) the property on the right-hand side.

\fbox{$\Longleftarrow$}~\,Assume ($\star$) holds. Let $\mathcal{M}$ be a model based on $\mathcal{W}$. It suffices to show that for every $x \in W$,
\[
\mathcal{M}, x \Vdash {\neg \left( p \wedge q \right)}
\quad \Longrightarrow \quad
\mathcal{M}, x \Vdash {\neg p}
\quad \text{or} \quad
\mathcal{M}, x \Vdash {\neg q} .
\]
Suppose $x \nVdash \neg p$ and $x \nVdash \neg q$. So there exist $y, z \in R \left( x \right)$ such that
\[
y \Vdash p
\quad \text{and} \quad
z \Vdash q
\]
Then by ($\star$), there exists $u \in R \left( x \right)$ such that $y \leqslant u$ and $z \leqslant u$. Consequently, $u \Vdash p$ and $u \Vdash q$, i.e.\ $u \Vdash p \wedge q$. Hence $x \nVdash \neg \left( p \wedge q \right)$.

\fbox{$\Longrightarrow$}~\,Assume ($\star$) fails. So there exist $x \in W$ and $y, z \in R \left( x \right)$ such that for every $u \in R \left( x \right)$ we have $y \not \leqslant u$ or $z \not \leqslant u$. Consider a model $\mathcal{M}$ based on $\mathcal{W}$ such that
\[
{\xi \left( p \right)}\ :=\
{\left\{ u \in W \mid y \leqslant u \right\}}
\quad \text{and} \quad
{\xi \left( q \right)}\ :=\
{\left\{ u \in W \mid z \leqslant u \right\}} .
\]
It is straightforward to check that
$\mathcal{M}, x \Vdash \neg \left( p \wedge q \right)$ but $\mathcal{M}, x \nVdash \neg p$ and $\mathcal{M}, x \nVdash \neg q$.
\end{proof}

%

For more examples, see the table below.
\begin{table}[H]
\centering
\begin{tabular}{|l|c|c|}
\hline
{\bfseries Property} & {\bfseries Scheme} & {\bfseries Reference}\\ \hline
${\forall x}\, {\exists y}\, {R \left( x, y \right)}$
&$\mathtt{N1}^\circ$
&\cite{Dosen-1986}\\
${\forall x}\, {\left( {\exists y}\, {R \left( y, x \right)} \Rightarrow {\exists z}\, {R \left( x, z \right)} \right)}$ %a weak form of seriality
&$\mathtt{N2}^\circ$
&\cite{Dosen-1986}\\
${\forall x}\, {\forall y}\, {\forall z}\, {\left( {R \left( x, y \right)} ~ \& ~ {R \left( x, z \right)} \Rightarrow {\exists u}\, {\left( {R \left( x, u \right)} ~ \& ~ {y \leqslant u} ~ \& ~ {z \leqslant u} \right)} \right)}$
&$\mathtt{N}^\ast$
&{This article}\\
${\forall x}\, {\forall y}\, {\left( {\exists u}\, {\left( {R \left( x, u \right)} ~ \& ~ {y \leqslant u} \right)} \Rightarrow {\exists u}\, {\left( {R \left( y, u \right)} ~ \& ~ {x \leqslant u} \right)} \right)}$ %i.e.\ $R \,\circ \leqslant^{-1}$ is symmetric
&$\mathtt{N1}^\bullet$
&\cite{Dosen-1986}\\
${\forall x}\, {\exists y}\, {\left( {R \left( x, y \right)} ~ \& ~ {\forall z}\, {\left( {R \left( y, z \right)} \rightarrow {z \leqslant x} \right)} \right)}$
&$\mathtt{N2}^\bullet$
&\cite{Dosen-1986}\\
${\forall x}\, {\forall y}\, {\left( {R \left( x, y \right)} \Rightarrow {\exists z}\, {\left( {R \left( x, z \right)} ~ \& ~ {x \leqslant z} ~ \& ~ {y \leqslant z} \right)} \right)}$
&$\mathtt{C}$
&\cite{Dosen-1986}\\
%${\forall x}\, {\forall y}\, {\forall z}\, {\left( {R \left( x, y \right)} ~ \& ~ {R \left( x, z \right)} \Rightarrow {\exists u}\, {\left( {R \left( y, u \right)} ~ \& ~ {z \leqslant u} \right)} \right)}$
%&$\mathtt{WEM}$
%&\cite{Dosen-1986}\\
\hline
\end{tabular}
\caption{\label{table:properties}Properties vs.\ Schemes.}
\end{table}

%

As was shown in \cite{Dosen-1986}, the canonical model method can be adapted to $\mathsf{N}$ and its extensions. Let $L$ be a logic. Call $\Gamma \subseteq \F$ a \emph{prime $L$-theory} iff: \enumiroman
\begin{enumerate}
    
\item $\left\{ \phi \in \F \mid \Gamma \vdash_L \phi \right\} \subseteq  \Gamma$;
    
% \item for every $\phi \in \F$, if $\Gamma \vdash_L \phi$, then $\phi \in \Gamma$;

\item for every $\phi \vee \psi \in \Gamma$ we have $\phi \in \Gamma$ or $\psi \in \Gamma$.

\end{enumerate}
Thus (i) and (ii) say that $\Gamma$ is closed under $\vdash_L$ and has the disjunction property. The following is proved in the usual way.

%

\begin{Lemm}[see \cite{Dosen-1986}] \label{Extension_Lemma} %Extension Lemma
Let $L$ be a logic. Suppose $\Gamma \subseteq \F$ and $\Delta \sqsubseteq \F$ are such that $\Gamma \nvdash_L \Delta$. Then there exists a prime $L$-theory $\Gamma' \supseteq \Gamma$ such that $\Gamma' \nvdash_L \Delta$.
\end{Lemm}

%

Given $\Gamma \subseteq \F$, we write $\underline{\Gamma}$ for $\left\{ \phi \mid {\neg \phi} \in \Gamma \right\}$.

\begin{Prop}[see \cite{Dosen-1986,Speranski-2020}] \label{Negation_Observations}
Let $\Gamma \subseteq \F$ be such that $\left\{ \phi \in \F \mid \Gamma \vdash \phi \right\} \subseteq \Gamma$
and $\underline{\Gamma} \ne \varnothing$. Then: \enumiroman
\begin{enumerate}

\item $\left\{ \phi \in \F \mid \phi \vdash \underline{\Gamma} \right\} \subseteq \underline{\Gamma}$;

\item for any $\phi, \psi\in \underline{\Gamma}$ we have $\phi \vee \psi \in \underline{\Gamma}$.

\end{enumerate}
\end{Prop}

%

Now take $W^L$ to be the collection of all prime $L$-theories. By the \emph{canonical fra\-me for $L$} we mean the triple $\mathcal{W}^L = \langle W^L, \leqslant^L, R^L \rangle$ where
\begin{align*}
\leqslant^L\ &:=\
{\left\{ \left( \Gamma, \Delta \right) \in W^L \times W^L \mid
\Gamma \subseteq \Delta \right\}} \quad \text{and}\\
R^L\ &:=\
{\left\{ \left( \Gamma, \Delta \right) \in W^L \times W^L \mid
\underline{\Gamma} \cap \Delta = \varnothing \right\}} .
\end{align*}
By the \emph{canonical model for $L$} we mean the pair $\mathcal{M}^L = \langle \mathcal{W}^L, \xi^L \rangle$ where $\xi^L$ is given by
\[
{\xi^L \left( p \right)}\ :=\
{\left\{
\Gamma \in W^L \mid
p \in \Gamma
\right\}} .
\]
One readily verifies that $\mathcal{W}^L$ is a frame, and $\mathcal{M}^L$ is a model. Moreover,
\[
\leqslant^L \circ \mathrel{R}^L \circ \leqslant^{-1}\ \subseteq\
R^L .
\]
Hence $\mathcal{W}^L$ is \emph{strictily condensed}, in the terminology of \cite{Dosen-1986}.\footnote{There
are several different but equivalent ways of defining this notion; see Definition~6 in \cite{Dosen-1986} together with the comments after it. In particular, for every frame $\mathcal{W}$,
\[
\leqslant \circ \mathrel{R} \circ \leqslant^{-1}\ \subseteq\
R
\quad \Longleftrightarrow \quad \mathrel{R} \circ \leqslant^{-1}\ \subseteq\ R .
\]
}
In fact, we might limit ourselves to strictly condensed frames if needed.

%

\begin{Lemm}[see \cite{Dosen-1986}] \label{Canonical_Model_Lemma} %Canonical Model Lemma; see also \cite{Speranski-2020}
Let $L$ be a logic. Then for any $\Gamma \in W^L$ and $\phi \in \mathrm{Form}$,
\[
\mathcal{M}^L, \Gamma \Vdash \phi
\quad \Longleftrightarrow \quad
\phi\ \in\ \Gamma .
\]
\end{Lemm}

Given $\Gamma \subseteq \F$ and $\Delta \sqsubseteq \F$, we write $\Gamma \vDash \Delta$ iff for any model $\mathcal{M}$ and $w \in W$,
\[
{\mathcal{M}, w \Vdash \phi} \quad \text{for all} \enskip {\phi \in \Gamma}
\quad \Longrightarrow \quad
{\mathcal{M}, w \Vdash \psi} \quad \text{for some} \enskip {\psi \in \Delta} .
\]
For each logic $L$, denote by $\vDash_L$ the relativization of $\vDash$ to $\left\{ \mathcal{W} \mid \mathcal{W} \Vdash L \right\}$.\footnote{Here $\mathcal{W} \Vdash L$ means that $\mathcal{W} \Vdash \phi$ for all $\phi \in L$.}
Further, call a logic $L$ \emph{canonical} iff $\mathcal{W}^L \Vdash L$.

\begin{Theo}[see \cite{Dosen-1986}] %Strong Completeness; see also \cite{Speranski-2020}
\label{Theorem_Completeness}
Let $L$ be a canonical logic. Then for any $\Gamma \subseteq \F$ and $\Delta \sqsubseteq \F$,
\[
{\Gamma \vdash_L \Delta}
\quad \Longleftrightarrow \quad
{\Gamma \vDash_L \Delta} .
\]
In particular, since $\mathsf{N}$ is canonical, $\vdash$ coincides with $\vDash$.
\end{Theo}

%

We conclude with two technical remarks. \enumiRoman
\begin{enumerate}

\item In \cite{Dosen-1986}, Do\v{s}en employed single-succedent derivability and semantical con\-se\-quen\-ce relations --- this, in a sense, forced him to utilize Zorn's lemma for the canonical model lemma. As has been shown in \cite{Speranski-2020}, this is not essential.

\item Do\v{s}en emphasized that $\F$ should be treated as a prime theory in his ca\-no\-ni\-cal model
construction. In most cases this is not necessary; see \cite{Speranski-2020}. In particular, if $L$ contains at least one~ne\-ga\-ted formula, we may assume that all prime $L$-theories are non-trivial.

\end{enumerate}
In view of (II), we shall adopt the convention that $\mathrm{Form}$ is a prime $L$-theory iff no negated~formula~belongs to $L$. So if $L$ contains some negated formulas, then each element of $W_L$ must be non-trivial; otherwise $\mathrm{Form}$ is also an element of $W_L$.

Next we turn to a more elegant semantics appropriate for logics containing $\mathsf{N}^\ast$.

%%%

%\pagebreak
\subsection{Routley-style semantics}

Following
\cite{Odintsov-2010}, by a \emph{Routley frame} we mean a tri\-p\-le $\mathbf{W} = \langle W, \leqslant, \ast \rangle$ where $W$ is a non-empty set, $\leqslant$ is a preordering on $W$, and $\ast$ is an anti-monotone function from $W$ to $W$. Obviously, $\ast$ may be viewed as a binary relation on $W$, and moreover, it is easy to verify that
\[
{\leqslant \circ \mathrel{\ast}}\ \subseteq\ {\mathrel{\ast} \circ \leqslant^{-1}} .
\]
So Routley frames are frames.\footnote{Semantically, the class of Routley frames plays the same role as the class of all frames $\mathcal{W}$ such that for each $w \in W$, $R \left( w \right)$ has a greatest element with respect to $\leqslant$; cf.\ \cite{Odintsov-2010}.}
Models based on Routley frames are called \emph{Routley models}. By definition, for any Routley model $\mathbf{M}$, $w \in W$ and $\psi \in \F$,
\[
\mathbf{M}, x \Vdash {\neg \psi}
\quad \Longleftrightarrow \quad
\mathbf{M}, x^\ast \nVdash \psi
\]
where $x^\ast$ stands for $\ast \left( x \right)$. This kind of semantics is suitable for $\mathsf{N}^\ast$ and its ex\-ten\-si\-ons.

%

Given $\Gamma \subseteq \F$, denote $\F \setminus \underline{\Gamma}$~--- i.e.\ $\left\{ \phi \in \F \mid {\neg \phi} \not \in \Gamma \right\}$~--- by $\Gamma^\ast$. Notice that if $L$ is an extension of $\mathsf{N}^\ast$, then it contains some negated formulas, and hence all prime $L$-theories are non-trivial by the above convention. The following is straightforward.

\begin{Prop}[see \cite{Odintsov-2010}]
Let $\Gamma$ be a prime $L$-theory, where $L$ is an extension of $\mathsf{N}^\ast$. Then $\Gamma^\ast$ is also a prime $L$-theory.
\end{Prop}

%

Let $L$ be an extension of $\mathsf{N}^\ast$. Observe that for every $\Gamma \in W^L$,
\[
\Gamma^\ast\ =\
\text{the greatest element of} ~ {\{ \Delta \in W^L \mid \underline{\Gamma} \cap \Delta = \varnothing \}}
\]
(with respect to inclusion). By the \emph{canonical Routley frame for $L$} we mean
\[
\mathbf{W}^L\ =\
\langle W^L, \leqslant^L, \ast^L \rangle
\]
where $W^L$ and $\leqslant^L$ are as before, and $\ast^L$ maps each $\Gamma$ in $W^L$ to $\Gamma^\ast$. By the \emph{ca\-no\-ni\-cal~Routley model for $L$} we mean 
\[
\mathbf{M}^L\ =\
\langle \mathbf{W}^L, \xi^L \rangle
\]
where $\xi^L$ is defined in the usual way. Clearly, $\mathbf{W}^L$ and $\mathbf{M}^L$ are a Routley frame and a Routley model respectively.

%

\begin{Lemm}[see \cite{Odintsov-2010}] %Canonical Model Lemma
Let $L$ be an extension of $\mathsf{N}^\ast$. Then for any $\Gamma \in W^L$ and $\phi \in \mathrm{Form}$,
\[
\mathbf{M}^L, \Gamma \Vdash \phi
\quad \Longleftrightarrow \quad
\phi\ \in\ \Gamma .
\]
\end{Lemm}

%

For each extension $L$ of $\mathsf{N}^\ast$, define $\vDash_L^\ast$ exactly as $\vDash_L$ but with `frames' replaced by `Routley frames'.
Further, we call an extension $L$ of $\mathsf{N}^\ast$ \emph{Routley canonical} iff $\mathbf{W}^L \Vdash L$.

\begin{Theo}[see \cite{Odintsov-2010}] %Strong Completeness
Let $L$ be a Routley canonical extension of $\mathsf{N}^\ast$. Then for any $\Gamma \subseteq \F$ and $\Delta \sqsubseteq \F$,
\[
{\Gamma \vdash_L \Delta}
\quad \Longleftrightarrow \quad
{\Gamma \vDash_L^\ast \Delta} .
\]
In particular, since $\mathsf{N}^\ast$ is Routley canonical, $\vdash_{\mathsf{N}^\ast}$ coincides with $\vDash_{\mathsf{N}^\ast}^\ast$.
\end{Theo}

%%%

%\pagebreak
\section{Adding the contraposition axiom} \label{section:contra}

Naturally, one may wonder what happens when we add the scheme $\mathtt{C}$~--- which is equivalent to $\mathtt{E}$ by Proposition~\ref{Prop-Repl}~--- to a given logic, e.g.\ $\mathsf{N}^\circ$, $\mathsf{N}^\ast$ or $\mathsf{N}^\bullet$. Here we focus on logics containing at least one negated formula. As will become clear from what follows, this leads us to consider logics that include $\mathtt{N2}^\circ$.\footnote{In
particular, $\mathsf{N} + \left\{ \mathtt{E} \right\}$ will not be considered because of Proposition~\ref{Prop:no_negations} below.}
Note that
$\mathtt{N2}^\circ$ is semantically weaker than $\mathtt{N1}^\circ$; see Table~\ref{table:properties}. We shall write $\mathsf{CL}$ for classical logic, $\mathsf{IL}$ for intuitionistic logic, and $\mathsf{JL}$ for Johansson's minimal logic.

%

\begin{Lemm} \label{Lemm:NE}
$\mathsf{N} + \left\{ \mathtt{N2}^\circ, \mathtt{E} \right\}$ coincides with $\mathsf{JL}$, and hence includes $\mathtt{N1}^\bullet$.\footnote{In \cite{Dosen-1986}, Do\v{s}en notes that $\mathsf{JL}$ coincides with $\mathsf{N} + \left\{ \mathsf{N1}^\bullet, \mathtt{C} \right\}$.}
\end{Lemm}

\begin{proof}
For convenience, let $L$ denote $\mathsf{N} + \left\{ \mathtt{N2}^\circ, \mathtt{E} \right\}$.
Clearly, $L \subseteq \mathsf{JL}$. For the other inclusion, it suffices to show that
\[
{\neg \phi} \leftrightarrow \underbrace{\left( \phi \rightarrow {\neg \left( \phi \rightarrow \phi \right)} \right)}_{- \phi}
\]
is derivable in $L$. The implication from left to right can be obtained as follows:
\begin{hilbert}
$\phi \rightarrow \left( \left( \phi \rightarrow \phi \right) \rightarrow \phi \right)$
&\\ %positive intuitionistic logic
$\left( \left( \phi \rightarrow \phi \right) \rightarrow \phi \right) \rightarrow \left( {\neg \phi} \rightarrow {\neg \left( \phi \rightarrow \phi \right)} \right)$
&$\mathtt{C}$ (see Proposition~\ref{Prop-Repl})\\
$\phi \rightarrow \left( {\neg \phi} \rightarrow {\neg \left( \phi \rightarrow \phi \right)} \right)$
&from 1, 2\\
${\neg \phi} \rightarrow \left( \phi \rightarrow {\neg \left( \phi \rightarrow \phi \right)} \right)$
&from 3.
\end{hilbert}
On the other hand, observe that $\phi \rightarrow {\neg \left( \phi \rightarrow \phi \right)} \vdash_L {\neg \phi}$:
\begin{hilbert}
$\phi \rightarrow {\neg \left( \phi \rightarrow \phi \right)}$
&{hypothesis}\\
$\left( \phi \rightarrow {\neg \left( \phi \rightarrow \phi \right)} \right) \rightarrow \left( {\neg \neg \left( \phi \rightarrow \phi \right)} \rightarrow {\neg \phi} \right)$
&$\mathtt{C}$ (see Proposition~\ref{Prop-Repl})\\
${\neg \neg \left( \phi \rightarrow \phi \right)} \rightarrow {\neg \phi}$
&from 1, 2\\
$\neg \neg \left( \phi \rightarrow \phi \right)$
&$\mathtt{N2}^\circ$\\
$\neg \phi$
&from 4, 3.
\end{hilbert}
By the deduction theorem for $L$, this gives us the implication from right to left.
\end{proof}

%Hence $\mathtt{N1}^\bullet$ is derivable in $\mathsf{N} + \left\{ \mathtt{N2}^\circ \right\}$.

%

Before proceeding, a few observations from \cite{Speranski-2020} are worth recalling here.

\begin{Prop}[see \cite{Speranski-2020}] \label{Prop:Obs}
\enumiroman
\begin{enumerate}

\item $\mathtt{N2}^\circ$ is derivable in $\mathsf{N} + \left\{ \mathtt{N1}^\bullet \right\}$.

\item $\mathtt{N1}^\circ$ and $\mathtt{N}^\ast$ are derivable in $\mathsf{N} + \left\{ \mathtt{N2}^\bullet \right\}$.

\end{enumerate}
\end{Prop}

%

So in particular, $\mathtt{N2}^\circ$ is deductively weaker than $\mathtt{N1}^\bullet$, which implies the fol\-low\-ing.

\begin{Coro}
$\mathsf{N} + \left\{ \mathtt{N1}^\bullet, \mathtt{E} \right\}$ coincides with $\mathsf{JL}$.
\end{Coro}

\begin{proof}
Since $\mathtt{N2}^\circ$ and $\mathtt{N1}^\bullet$ are derivable in $\mathsf{N} + \left\{ \mathtt{N1}^\bullet \right\}$ and $\mathsf{JL}$ respectively, we have
\[
{\mathsf{N} + \left\{ \mathtt{N1}^\bullet, \mathtt{E} \right\}}\ =\
{\mathsf{N} + \left\{ \mathtt{N2}^\circ, \mathtt{N1}^\bullet, \mathtt{E} \right\}}\ =\
{\mathsf{JL} + \left\{ \mathtt{N1}^\bullet \right\}}\ =\
\mathsf{JL}
\]
(using Lemma~\ref{Lemm:NE} for the second equality).
\end{proof}

%

Interestingly enough, $\mathtt{N1}^\circ$ is stronger than $\mathtt{N2}^\circ$ semantically but not deductively, as the next result shows.

\begin{Prop}[cf.\ \cite{Odintsov-2010}] \label{Prop:no_negations}
No formula beginning with $\neg$ can be derived in $\mathsf{N} + \left\{ \mathtt{N2}^\bullet, \mathtt{E} \right\}$. In particular, $\mathtt{N2}^\circ$ is not derivable in $\mathsf{N} + \left\{ \mathtt{N2}^\bullet, \mathtt{E} \right\}$.\footnote{Bear in mind that $\mathsf{N} + \left\{ \mathtt{N2}^\bullet, \mathtt{E} \right\}$ coincides with $\mathsf{N} + \left\{ \mathtt{N1}^\circ, \mathtt{N}^\ast, \mathtt{N2}^\bullet, \mathtt{E} \right\}$.}
\end{Prop}

%...

\begin{proof}
The analogous result for $\mathsf{N} + \left\{ \mathtt{N1}^\circ, \mathtt{N}^\ast \right\}$ was proved in \cite{Odintsov-2010}, using a `Kleene slash', and the same argument applies to $\mathsf{N} + \left\{ \mathtt{N2}^\bullet, \mathtt{E} \right\}$.
\end{proof}

%у нас тут всюду субклассические системы, в которых нельзя вывести $\phi$ и $\neg \phi$ одновременно

%

Finally, we turn to the extensions of $\mathsf{N}^\circ$, $\mathsf{N}^\ast$ and $\mathsf{N}^\bullet$ obtained by adding $\mathtt{E}$.

\begin{Theo}
\enumiroman
\begin{enumerate}

\item $\mathsf{N}^\circ + \left\{ \mathtt{E} \right\} = \mathsf{IL}$.

\item $\mathsf{N}^\ast + \left\{ \mathtt{E} \right\} = \mathsf{IL} + \left\{ \mathtt{WEM} \right\}$.

\item $\mathsf{N}^\bullet + \left\{ \mathtt{E} \right\} = \mathsf{CL}$.

\end{enumerate}
\end{Theo}

%Notice that $\mathsf{N}^\bullet + \left\{ \mathtt{E} \right\}$ coincides with $\mathsf{N} + \left\{ \mathtt{N2}^\circ, \mathtt{N2}^\bullet, \mathtt{E} \right\}$.

\begin{proof}
\fbox{i}~\,By Lemma~\ref{Lemm:NE}, $\mathsf{N}^\circ + \left\{ \mathtt{E} \right\}$ coincides with $\mathsf{JL} + \left\{ \mathtt{N1}^\circ \right\}$, i.e.\ with  $\mathsf{IL}$.

\fbox{ii}~\,By (i), $\mathsf{N}^\ast + \left\{ \mathtt{E} \right\}$ coincides with $\mathsf{IL} + \left\{ \mathtt{N}^\ast \right\}$. Thus it remains to show that $\mathtt{N}^\ast$ and $\mathtt{WEM}$ are equivalent over $\mathsf{IL}$.\footnote{In
fact, it is straightforward to prove this using the possible world semantics for $\mathsf{IL}$ (see e.g.\ \cite[Section~3]{Segerberg-1968}). Here a syntactic proof is provided.}
Notice that $\mathtt{WEM}$ is easily derivable in $\mathsf{IL} + \left\{ \mathtt{N}^\ast \right\}$:
\begin{hilbert}
$\neg \left( \phi \wedge {\neg \phi} \right)$
&$\mathsf{JL}$\\
$\neg \left( \phi \wedge {\neg \phi} \right) \rightarrow {{\neg \phi} \vee {\neg \neg \phi}}$
&$\mathtt{N}^\ast$\\
${\neg \phi} \vee {\neg \neg \phi}$
&from 1, 2.
\end{hilbert}
On the other hand, ${\neg \phi} \vee {\neg \psi}$ can be derived from $\neg \left( \phi \wedge \psi \right)$ in $\mathsf{IL} + \left\{ \mathtt{WEM} \right\}$ as follows:
\begin{hilbert}
${\neg \phi} \vee {\neg \neg \phi}$
&$\mathtt{WEM}$\\
${\neg \psi} \vee {\neg \neg \psi}$
&$\mathtt{WEM}$\\
$\left( {\neg \phi} \vee {\neg \neg \phi} \right) \wedge \left( {\neg \psi} \vee {\neg \neg \psi} \right)$
&from 1, 2\\
$\left( {\neg \phi} \wedge {\neg \psi} \right) \vee \left( {\neg \phi} \wedge {\neg \neg \psi} \right) \vee \left( {\neg \neg \phi} \wedge {\neg \psi} \right) \vee \left( {\neg \neg \phi} \wedge {\neg \neg \psi} \right)$
&from 3\\
${{\neg \phi} \wedge {\neg \psi}} \rightarrow {{\neg \phi} \vee {\neg \psi}}$
&\\
${{\neg \phi} \wedge {\neg \neg \psi}} \rightarrow {{\neg \phi} \vee {\neg \psi}}$
&\\
${{\neg \neg \phi} \wedge {\neg \psi}} \rightarrow {{\neg \phi} \vee {\neg \psi}}$
&\\
$\neg \left( \phi \wedge \psi \right)$
&hypothesis\\
${{\neg \neg \phi} \wedge {\neg \neg \psi}} \rightarrow {\neg \left( \phi \wedge \psi \right)}$
&from 8\\
${{\neg \neg \phi} \wedge {\neg \neg \psi}} \rightarrow {\neg \neg \left( \phi \wedge \psi \right)}$
&$\mathsf{JL}$\\
${{\neg \neg \phi} \wedge {\neg \neg \psi}} \rightarrow {{\neg \left( \phi \wedge \psi \right)} \wedge {\neg \neg \left( \phi \wedge \psi \right)}}$
&from 9, 10\\
${{\neg \left( \phi \wedge \psi \right)} \wedge {\neg \neg \left( \phi \wedge \psi \right)}} \rightarrow {{\neg \phi} \vee {\neg \psi}}$
&$\mathsf{IL}$\\
${{\neg \neg \phi} \wedge {\neg \neg \psi}} \rightarrow {{\neg \phi} \vee {\neg \psi}}$
&from 11, 12\\
${\neg \phi} \vee {\neg \psi}$
&from 4--7, 13.\\
\end{hilbert}
By the deduction theorem for $\mathsf{IL} + \left\{ \mathtt{WEM} \right\}$, this gives us $\mathtt{N}^\ast$.

\fbox{iii}~\,By (ii), $\mathsf{N}^\bullet + \left\{ \mathtt{E} \right\}$ coincides with $\mathsf{IL} + \left\{ \mathtt{N2}^\bullet \right\}$, i.e.\ with $\mathsf{CL}$.
\end{proof}

%(iii) can also be proved semantically: since $x \leqslant x^\ast$ and $x^\ast \leqslant x^{\ast \ast} = x$, we have $x^\ast = x$; thus $x$ turns out to be the greatest element in $\left\{ y \mid x \leqslant y \right\}$. 

%$\mathsf{IL} + \left\{ \mathtt{WEM} \right\}$ соответствует шкалам Раутли таким, что $u \leqslant u^\ast$ для всех $u \in W$ (фактически это интуиционистские шкалы, где для любого $u \in W$ в $\left\{ w \mid u \leqslant w \right\}$ есть наибольший элемент):
% \begin{proof}
% \fbox{$\Longrightarrow$}~\,Suppose $\mathcal{W}$ is specific. Let $\mathcal{M}$ be a model over $\mathcal{W}$ and $u \in W$. Assume $u \Vdash p \rightarrow q$ and $u \Vdash {\neg q}$. Then $u \Vdash {\neg p}$, of course.

% \medskip
% \fbox{$\Longleftarrow$}~\,Suppose $\mathcal{W}$ is not specific, i.e.\ there is $u \in W$ such that $u \not \leqslant u^{\ast}$. Consider a model $\mathcal{M}$ such that
% \[
% {I \left( p \right)}\ :=\ \widehat{u}
% \quad \text{and} \quad
% {I \left( q \right)}\ :=\ {\widehat{u} \cup \widehat{u^{\ast}}} .
% \]
% Note that for every $v \in \widehat{u}$ we have $v \Vdash p \wedge q$. Hence $u \Vdash p \leftrightarrow q$. On the other hand, $u^{\ast} \nVdash p$ and $u^{\ast} \vdash q$, so $u \Vdash {\neg p}$ and $u \nVdash {\neg q}$. Hence $u \nVdash {\neg p} \leftrightarrow {\neg q}$. Thus $\mathtt{I}$ fails in $\mathcal{M}$.\footnote{It
% should be remarked that $u$ is a `non-normal' world: $u \Vdash p \wedge {\neg p}$.}
% \end{proof}

%%%

%\pagebreak
\section{Certain canonical extensions} \label{section:canonical}

Note that every canonical logic containing $\mathtt{N1}^\circ$ must contain $\mathtt{N2}^\circ$. So in par\-ti\-cu\-lar,~we have the following negative result.

%

\begin{Prop}
Let $L$ be a logic between $\mathsf{N} + \left\{ \mathtt{N1}^\circ \right\}$ and $\mathsf{N} + \left\{ \mathtt{N2}^\bullet, \mathtt{E} \right\}$. Then $L$ is not canonical.
\end{Prop}

%Since $L$ does not extend $\mathsf{N}^\ast$, $L$ is trivially not Routley canonical.

\begin{proof}
For any frame $\mathcal{W}$, if $\mathcal{W} \Vdash L$, then $\mathcal{W} \Vdash \mathtt{N1}^\circ$ and therefore $\mathcal{W} \Vdash \mathtt{N2}^\circ$ (see Table~\ref{table:properties}). Thus $\vDash_L {\neg \neg \left( p \rightarrow p \right)}$. On the other hand, we have $\nvdash_L \neg \neg \left( p \rightarrow p \right)$ by Pro\-po\-si\-ti\-on~\ref{Prop:no_negations}. Hence $L$ is not canonical by Theorem~\ref{Theorem_Completeness}.
\end{proof}

%By similar reasoning, $L$ is not Routley canonical.

%

Obviously, $\mathsf{N}$ and $\mathsf{N}^\ast$ are canonical and Routley canonical respectively. Also, one can check that $\mathsf{N}^\circ$ is canonical and $\mathsf{N}^\bullet$ is Routley canonical; cf.\ \cite{Speranski-2020,Odintsov-Wansing-2021}. Further examples can be obtained by using so-called `canonical schemes'.

%

Let $L$ be a logic and $\mathtt{S}$ be a scheme. We call $\mathtt{S}$ \emph{canonical over $L$} iff $\mathcal{W}^{L'} \Vdash \mathtt{S}$ for every extension $L'$ of $L + \left\{ \mathtt{S} \right\}$. Similarly with `Routley canonical' in place of `canonical'. For instance, since the formulas of the form $\phi \rightarrow \phi$ are valid in all frames, $\mathtt{N2}^\circ$ turns out to be canonical over $\mathsf{N}$.

For the purposes of the next proof note that if $L$ includes $\mathtt{N2}^\circ$, then some ne\-ga\-ted~formulas belong to $L$, and hence for every $\Gamma \in W^L$ we have $\underline{\Gamma} \ne \varnothing$.

\begin{Theo}
$\mathtt{N1}^\circ$, $\mathtt{N}^\ast$, $\mathtt{N1}^\bullet$ and $\mathtt{N2}^\bullet$ are canonical over $\mathsf{N} + \left\{ \mathtt{N2}^\circ \right\}$.
\end{Theo}

%Perhaps $\mathtt{E}$ should be dropped here.

\begin{proof}
Let $\mathtt{S}$ be one of the schemes above, and let $L$ be an extension of $\mathsf{N} + \left\{ \mathtt{N2}^\circ, \mathtt{S} \right\}$. We want to show that $\mathcal{W}^L$ has the property corresponding to $\mathtt{S}$.

\fbox{$\mathtt{N1}^\circ$}~\,Let $\Gamma \in W^L$. We need to find $\Delta \in W^L$ such that $\underline{\Gamma} \cap \Delta = \varnothing$. It suffices to show that $\nvdash_L \underline{\Gamma}$~--- because a suitable $\Delta$ can then be obtained by applying Lem\-ma~\ref{Extension_Lemma}. Now assume, by way of contradiction, that $\vdash_L \underline{\Gamma}$. So $\top \vdash_L \underline{\Gamma}$; thus $\top \in \underline{\Gamma}$ by Proposition~\ref{Negation_Observations}, i.e.\ $\neg \top \in \Gamma$. Hence we obtain $\Gamma = \F$ (using $\mathtt{N1}^\circ$), a contradiction.

\fbox{$\mathtt{N}^\ast$}~\,Let $\Gamma, \Delta, \Sigma \in W^L$ be such that $\underline{\Gamma} \cap \Delta = \varnothing$ and $\underline{\Gamma} \cap \Sigma = \varnothing$. We need to find $\Pi \in W^L$ such that
\[
{\underline{\Gamma} \cap \Pi}\ =\ \varnothing
\quad \text{and} \quad
{\Delta \cup \Sigma}\ \subseteq\ \Pi .
\]
It suffices to show that $\Delta \cup \Sigma \nvdash_L \underline{\Gamma}$~--- because a suitable $\Pi$ can then be obtained by applying Lemma~\ref{Extension_Lemma}. Now assume, by way of contradiction, that $\Delta \cup \Sigma \vdash_L \underline{\Gamma}$. Since $\Delta$ and $\Sigma$ are closed under conjunction, while $\underline{\Gamma}$ is closed under disjunction by Proposition~\ref{Negation_Observations}, we have
\[
\left\{ \phi, \psi \right\} \vdash_L \theta
\quad \text{for some} \enskip \phi \in \Delta, \enskip \psi \in \Sigma \enskip \text{and} \enskip \theta \in \underline{\Gamma} .
\]
So ${\phi \wedge \psi} \rightarrow \theta \in L$. Therefore ${\neg \theta} \rightarrow {\neg \left( \phi \wedge \psi \right)} \in L$ (by $\mathtt{CR}$). This implies ${\neg \left( \phi \wedge \psi \right)}\linebreak \in \Gamma$ (since ${\neg \theta} \in \Gamma$). Thus ${\neg \phi} \vee {\neg \psi} \in \Gamma$ (using $\mathtt{N}^\ast$), which gives ${\neg \phi} \in \Gamma$ or ${\neg \psi} \in \Gamma$, i.e.\ $\phi \in \underline{\Gamma}$ or $\psi \in \underline{\Gamma}$. Hence we obtain $\underline{\Gamma} \cap \Delta \ne \varnothing$ or $\underline{\Gamma} \cap \Sigma \ne \varnothing$, a contradiction.

\fbox{$\mathtt{N1}^\bullet$}~\,Since the composition of $R_L$ and $\leqslant_L^{-1}$ coincides with $R_L$, it suffices to prove that $R_L$ is symmetric. Let $\Gamma, \Delta \in W^L$ be such that $\underline{\Gamma} \cap \Delta = \varnothing$. We need to show that $\underline{\Delta} \cap \Gamma = \varnothing$. This is easy: if $\phi \in \Gamma$, then ${\neg {\neg \phi}} \in \Gamma$ (using $\mathtt{N1}^\bullet$), i.e.\ ${\neg \phi} \in \underline{\Gamma}$, which implies ${\neg \phi} \not \in \Delta$, i.e.\ $\phi \not \in \underline{\Delta}$.

%Notice that $R^L \circ {\left( \leqslant^L \right)}^{-1}$ coincides with $R^L$.

\fbox{$\mathtt{N2}^\bullet$}~\,Assume, by way of contradiction, that $\mathcal{W}^L$ does~not have the property cor\-res\-pon\-d\-ing to $\mathtt{N2}^\bullet$, i.e.\ there exists $\Gamma \in W^L$ such that for every $\Delta \in W^L$,
\[
{\underline{\Gamma} \cap \Delta}\ =\ \varnothing
\quad \Longrightarrow \quad
\begin{tabular}{c}
there exists $\Sigma \in W^L$ such that\\[0.25em]
$\underline{\Delta} \cap \Sigma = \varnothing$ and $\Sigma \not \subseteq \Gamma$.
\end{tabular}
\]
For each $\Delta \in W^L$ such that $\underline{\Gamma} \cap \Delta = \varnothing$, choose $\Sigma_\Delta \in W^L$ and $\phi_\Delta \in \F$ satisfying
\[
{\underline{\Delta} \cap \Sigma_\Delta}\ =\ \varnothing
\quad \text{and} \quad
\phi_\Delta\ \in {\Sigma_\Delta \setminus \Gamma} .
\] %they exist by the assumption
Take $\Pi_0$ to be $\left\{ {\neg \phi_{\Delta}} \mid \Delta \in W^L ~ \text{and} ~ \underline{\Gamma} \cap \Delta = \varnothing \right\}$. Observe that $\Pi_0 \ne \varnothing$:
\begin{itemize}

\item[]
Assume that $\Pi_0 = \varnothing$, i.e.\ there exists no $\Delta \in W^L$ such that $\underline{\Gamma} \cap \Delta = \varnothing$. Then $\phi \vdash_L \underline{\Gamma}$ for all $\phi \in \F$. So $\underline{\Gamma} = \F$ by Proposition~\ref{Negation_Observations}. Hence we obtain $\Gamma = \F$ (using $\mathtt{N2}^\bullet$), a contradiction.

\end{itemize}
Next, it is not hard to show that $\Pi_0 \nvdash_L \underline{\Gamma}$:
\begin{itemize}

\item[]
Assume that $\Pi_0 \vdash_L \Gamma$. So ${\neg \phi_{\Delta_0}} \wedge \ldots \wedge {\neg \phi_{\Delta_n}} \vdash_L \underline{\Gamma}$ for some ${\neg \phi_{\Delta_0}}, \ldots, {\neg \phi_{\Delta_n}}\linebreak \in \Pi_0$. Thus ${\neg \phi_{\Delta_0}} \wedge \ldots \wedge {\neg \phi_{\Delta_n}} \in \underline{\Gamma}$ by Proposition~\ref{Negation_Observations}, i.e.\
\[
{\neg \left( {\neg \phi_{\Delta_0}} \wedge \ldots \wedge {\neg \phi_{\Delta_n}} \right)}\ \in\ \Gamma .
\]
From this we obtain ${\neg \neg \phi_{\Delta_0}} \vee \ldots \vee {\neg \neg \phi_{\Delta_n}} \in \Gamma$ (using $\mathtt{N}^\ast$), and hence $\phi_{\Delta_0} \vee \ldots \vee \phi_{\Delta_n} \in \Gamma$ (using $\mathtt{N2}^\bullet$).\footnote{By Proposition~\ref{Prop:Obs}, $\mathtt{N}^\ast$ is derivable in $L$.} Therefore one of  $\phi_{\Delta_0}$, \ldots, $\phi_{\Delta_n}$ must be in $\Gamma$, a contradiction.

\end{itemize}
Finally, let $\Pi \in W^L$ be such that $\Pi_0 \subseteq \Pi$ and $\Pi \nvdash_L \underline{\Gamma}$; the latter implies $\underline{\Gamma} \cap \Pi = \varnothing$, of course. %which exists by Lemma~\ref{Extension_Lemma}.
Then $\phi_{\Pi} \in \Sigma_\Pi \subseteq \F \setminus \underline{\Pi}$, which~contradicts ${\neg \phi_{\Pi}} \in \Pi_0 \subseteq \Pi$.
\end{proof}

% \fbox{$\mathtt{E}$}~\,Let $\Gamma, \Delta \in W^L$ be such that $\underline{\Gamma} \cap \Delta = \varnothing$. We need to find $\Sigma \in W^L$ such that
% \[
% {\underline{\Gamma} \cap \Sigma}\ =\ \varnothing
% \quad \text{and} \quad
% {\Gamma \cup \Delta}\ \subseteq\ \Sigma .
% \]
% It suffices to show that $\Gamma \cup \Delta \nvdash_L \underline{\Gamma}$. %--- because a suitable $\Sigma$ can then be obtained by applying Lemma~\ref{Extension_Lemma}. 
% Assume, by way of contradiction, that $\Gamma \cup \Delta \vdash_L \underline{\Gamma}$, i.e.\ we have
% \[
% \left\{ \phi, \psi \right\} \vdash_L \theta
% \quad \text{for some} \enskip \phi \in \Gamma, \enskip \psi \in \Delta \enskip \text{and} \enskip \theta \in \underline{\Gamma} .
% \]
% So $\phi \vdash_L \psi \rightarrow \theta$. Therefore $\phi \vdash_L {\neg \theta} \rightarrow {\neg \psi}$ (using $\mathtt{C}$). %by $\mathtt{E}$
% This implies $\Gamma \vdash_L {\neg \psi}$ (since $\left\{ \phi, {\neg \theta} \right\} \subseteq \Gamma$), which gives ${\neg \psi} \in \Gamma$, i.e.\ $\psi \in \underline{\Gamma}$. Hence we obtain $\underline{\Gamma} \cap \Delta \ne \varnothing$, a contradiction.

%

\begin{Coro}
Let $S \subseteq \left\{ \mathtt{N1}^\circ, \mathtt{N}^\ast, \mathtt{N1}^\bullet, \mathtt{N2}^\bullet \right\}$. Then $\left( \mathsf{N} \cup \left\{ \mathtt{N2}^\circ \right\} \right) + S$ is canonical.
\end{Coro}

\begin{proof}
Immediate.
\end{proof}

%

\begin{Theo}
$\mathtt{N1}^\bullet$ and $\mathtt{N2}^\bullet$ are Routley canonical over $\mathsf{N}^\ast$.
\end{Theo}

\begin{proof}
Let $\mathtt{S}$ be one of the schemes above, and let $L$ be an extension of $\mathsf{N}^\ast + \left\{ \mathtt{S} \right\}$. We want to show that $\mathcal{W}^L$ has the property corresponding to $\mathtt{S}$.

\fbox{$\mathtt{N1}^\bullet$}~\,It suffices to show that for any $\Gamma \in W^L$ we have $\Gamma \subseteq \Gamma^{\ast \ast}$. This is easy: if $\phi \in \Gamma$, then ${\neg \neg \phi} \in \Gamma$ (using $\mathtt{N1}^\bullet$), i.e.\ ${\neg \phi} \not \in \Gamma^\ast$, i.e.\ $\phi \in \Gamma^{\ast \ast}$.

\fbox{$\mathtt{N2}^\bullet$}~\,Similarly to $\mathtt{N1}^\bullet$.
\end{proof}

%

\begin{Coro}
$\mathsf{N}^\ast + \left\{ \mathtt{N1}^\bullet \right\}$, $\mathsf{N}^\ast + \left\{ \mathtt{N2}^\bullet \right\}$ and $\mathsf{N}^\bullet$ are Routley canonical.
\end{Coro}

\begin{proof}
Immediate.
\end{proof}

%%%

%\pagebreak
\section{The method of filtration revisited} \label{section:filtration}

The decidability of $\mathsf{N}$ and $\mathsf{N}^\ast$ can be established using the method of filtration as presented in \cite[Section~4]{Drobyshevich-Odintsov-2013}. We are going to develop a somewhat more flexible approach to filtrations, which will lead to further decidability results.

\subsection{General filtrations}

Fix a model $\mathcal{M} = \langle \mathcal{W}, \xi \rangle$. Let $\Phi \subseteq \F$ be closed under subformulas. Take
\[
\equiv_\Phi\ :=\
{\left\{
\left( x, y \right) \in W^2 \mid
\text{for all $\phi \in \Phi$, $\mathcal{M}, x \Vdash \phi$ iff $\mathcal{M}, y \Vdash \phi$}
\right\}} .
\]
For every $x \in W$, denote by ${\left[ x \right]}_\Phi$ the equivalence class of $x$ under $\equiv_\Phi$. We shall often omit the subscript ${}_\Phi$ if it is clear from the context. By a \emph{$\Phi$-filtration of $\mathcal{M}$} we mean a model
\[
\mathcal{M}'\ =\ \langle \langle W_\Phi, \leqslant', \R' \rangle, \xi_\Phi \rangle
\]
where:
\begin{itemize}

\item $W_\Phi$ is $\left\{ \left[ x \right] \mid x \in W \right\}$;

\item $\leqslant'$ is such that:
\begin{itemize}

\item for all $x, y \in W$, if $x \leqslant y$, then $\left[ x \right] \leqslant' \left[ y \right]$;

\item for all $x, y \in W$ and $\phi \in \Phi$, if $\left[ x \right] \leqslant' \left[ y \right]$ and $\mathcal{M}, x \Vdash \phi$, then $\mathcal{M}, y \Vdash \phi$;

\end{itemize}

\item $R'$ is such that:
\begin{itemize}

\item for all $x, y \in W$, if $x R y$, then $\left[ x \right] R' \left[ y \right]$;

\item for all $x, y \in W$ and $\neg \phi \in \Phi$, if $\left[ x \right] R' \left[ y \right]$ and $\mathcal{M}, x \Vdash {\neg \phi}$, then $\mathcal{M}, y \nVdash \phi$;

\end{itemize}

\item $\xi_\Phi$ is the function mapping each $p \in \mathrm{Prop}$ to $\left\{ \left[ x \right] \mid x \in \xi \left( p \right) ~ \text{and} ~ p \in \Phi \right\}$.

\end{itemize}
Obviously, $W_\Phi$ and $\xi_\Phi$ are both uniquely determined by $\mathcal{M}$ and $\Phi$, unlike $\leqslant'$ and $R'$. Define
\begin{align*}
\leqslant_\Phi\
&:=\ \text{the transitive closure of $\left\{ \left( {\left[ x \right]}, {\left[ y \right]} \right) \mid x \leqslant y \right\}$},\\
R_\Phi\
&:=\ \text{the composition of $\leqslant_\Phi$, $\left\{ \left( {\left[ x \right]}, {\left[ y \right]} \right) \mid x R y \right\}$ and $\leqslant_\Phi^{-1}$} .
\end{align*}
To make this definition easier to handle, denote by $\sqsubseteq$ the transitive closure of\linebreak \mbox{$\leqslant \cup \equiv$}, i.e.\ $x \sqsubseteq y$ iff there exist $x_0, \ldots, x_n \in W$ such that: \pagebreak
\begin{itemize}

\item $x_0 = x$ and $x_n = y$;

\item for every $i \in \left\{ 0, \ldots, n-1 \right\}$ we have $x_i \leqslant x_{i+1}$ or $x_i \equiv x_{i+1}$.

\end{itemize}
Now, using $\sqsubseteq$, the relations $\leqslant_\Phi$ and $R_\Phi$ can be described as follows: %more explicitly
\begin{align*}
{\left[ x \right] \leqslant_\Phi \left[ y \right]}
\quad &\Longleftrightarrow \quad
x \sqsubseteq y ;\\
{\left[ x \right]} \R_\Phi {\left[ y \right]}
\quad &\Longleftrightarrow \quad
x \sqsubseteq u \R v \sqsupseteq y \quad \text{for some} \enskip {u, v \in W} .
\end{align*}
On the other hand, following \cite[Section~4]{Drobyshevich-Odintsov-2013}, one may consider
\begin{align*}
\leqslant^\Phi\
&:=\ {\left\{ \left( {\left[ x \right]}, {\left[ y \right]} \right) \mid \text{for all} ~ {\phi \in \Phi}, ~ \text{if} ~ {\mathcal{M}, x \Vdash \phi}, ~ \text{then} ~ {\mathcal{M}, y \Vdash \phi} \right\}},\\
R^\Phi\
&:=\ {\left\{ \left( {\left[ x \right]}, {\left[ y \right]} \right) \mid \text{for all} ~ {\neg \phi \in \Phi}, ~ \text{if} ~ {\mathcal{M}, x \Vdash {\neg \phi}}, ~ \text{then} ~ {\mathcal{M}, y \nVdash \phi} \right\}} .
\end{align*}
Substituting $\leqslant_\Phi$, $R_\Phi$ and $\leqslant^\Phi$, $R^\Phi$ for $\leqslant'$, $R'$, we get
\[
\mathcal{M}_\Phi\ :=\
\langle \langle W_\Phi, \leqslant_\Phi, R_\Phi \rangle, \xi_\Phi \rangle
\quad \text{and} \quad
\mathcal{M}^\Phi\ :=\
\langle \langle W_\Phi, \leqslant^\Phi, R^\Phi \rangle, \xi_\Phi \rangle .\footnotemark
\]
Naturally, $\langle W_\Phi, \leqslant_\Phi, R_\Phi \rangle$ and $\langle W_\Phi, \leqslant^\Phi, R^\Phi \rangle$ are abbreviated to $\mathcal{W}_\Phi$ and $\mathcal{W}^\Phi$ res\-pec\-ti\-ve\-ly. It is easy to see that for every $\Phi$-filtration $\mathcal{M}'$ of $\mathcal{M}$,
\[
\leqslant_\Phi\ \subseteq\ \leqslant'\ \subseteq\ \leqslant^\Phi
\quad \text{and} \quad
R'\ \subseteq\ R^\Phi ;
\]
furthermore, in the case where $\mathcal{M}'$ is strictly condensed we also have $R_\Phi \subseteq R'$.

\footnotetext{In \cite{Drobyshevich-Odintsov-2013}, only filtrations of the form $\mathcal{M}^\Phi$ (which are, in a sense, rather `syntactic') %because $\leqslant$ and $R$ are not directly employed
were con\-si\-der\-ed. Since our approach allows other kinds of filtration, it appears to be more flexible.}

%

\begin{Prop}
Let $\mathcal{M}$ and $\Phi$ be as above. Then $\mathcal{W}_\Phi$ is a strictly condensed frame and $\mathcal{M}_\Phi$ is a $\Phi$-filtration of $\mathcal{M}$.
\end{Prop} %we don't even need $\leqslant \circ R \subseteq R$ here

\begin{proof}
Obviously, $\leqslant_\Phi$ is a preordering on $W_\Phi$. We also have ${\leqslant_\Phi \circ \R_\Phi \circ \leqslant_\Phi^{-1}} \subseteq {\R_\Phi}$:
\begin{itemize}

\item[]
Let $x, y \in W$. Suppose there exist $u, v \in W$ such that
\[
{\left[ x \right]}\ \leqslant_\Phi\ {\left[ u \right]}, \quad
{\left[ u \right]}\ R_\Phi\ {\left[ v \right]} \quad \text{and} \quad
{\left[ y \right]}\ \leqslant_\Phi\ {\left[ v \right]} .
\]
Then $x \sqsubseteq u$, $y \sqsubseteq v$ and there are $s, t \in W$ such that $u \sqsubseteq s \R t \sqsupseteq v$. Hence $x \sqsubseteq s \R t \sqsupseteq y$, which implies $\left[ x \right] R_\Phi 
\left[ y \right]$.

\end{itemize}
Thus $\mathcal{W}_\Phi$ is a strictly condensed frame. The rest is routine.
\end{proof}

%

\begin{Prop}[see {\cite[Section~4]{Drobyshevich-Odintsov-2013}}]
Let $\mathcal{M}$ and $\Phi$ be as above. Then $\mathcal{W}^\Phi$ is a strictly condensed frame and $\mathcal{M}^\Phi$ is a $\Phi$-filtration of $\mathcal{M}$.
\end{Prop}

\begin{proof}
Evidently, $\leqslant_\Phi$ is a preordering on $W_\Phi$. We also have ${\leqslant^\Phi \circ \R^\Phi \circ \mathrel{\left( \leqslant^\Phi \right)}^{-1}} \subseteq {\R_\Phi}$:
\begin{itemize}

\item[]
Let $x, y \in W$. Suppose there exist $u, v \in W$ such that
\[
{\left[ x \right]}\ \leqslant^\Phi\ {\left[ u \right]}, \quad
{\left[ u \right]}\ R^\Phi\ {\left[ v \right]} \quad \text{and} \quad
{\left[ y \right]}\ \leqslant^\Phi\ {\left[ v \right]} .
\]
Observe that for all $\neg \phi \in \Phi$, if $\mathcal{M}, x \Vdash \neg \phi$, then $\mathcal{M}, u \Vdash \neg \phi$, and hence $\mathcal{M}, v \nVdash \phi$, which implies $\mathcal{M}, y \nVdash \phi$.

\end{itemize}
Thus $\mathcal{W}^\Phi$ is a strictly condensed frame. The rest is clear.
\end{proof}

%

\begin{Lemm} \label{Lemm:filt}
Let $\mathcal{M}$, $\Phi$ and $\mathcal{M}'$ be as above. Then for any $x \in W$ and $\phi \in \Phi$,
\[
\mathcal{M}, x \Vdash \phi
\quad \Longleftrightarrow \quad
\mathcal{M}', {\left[ x \right]} \Vdash \phi .
\]
\end{Lemm}

\begin{proof} %for $\mathcal{M}' = \mathcal{M}_\Phi$
By induction on the complexity of $\phi$.

The case where $\phi \in \mathrm{Prop}$ is trivial.

Suppose $\phi = \neg \psi$. Consider each of the two implications separately.
\begin{itemize}

\item[\fbox{$\Longrightarrow$}]
Assume $x \Vdash \phi$. Let $y \in W$ be such that $\left[ x \right] R' \left[ y \right]$. Then $y \nVdash \psi$. So we have $\left[ y \right] \nVdash \psi$ by the inductive hypothesis.

\item[\fbox{$\Longleftarrow$}]
Assume $\left[ x \right] \Vdash \phi$. Let $y \in W$ be such that $x R y$. Then $\left[ x \right] R' \left[ y \right]$, and hence $\left[ y \right] \nVdash \psi$. So we have $y \nVdash \psi$ by the inductive hypothesis.

\end{itemize}

The other cases can be handled as in intuitionistic logic.
\end{proof}

% \begin{proof} %in case $\mathcal{M}' = \mathcal{M}_\Phi$
% By induction on the complexity of $\phi$.
%
% The case where $\phi \in \mathrm{Prop}$ is trivial.
%
% Suppose $\phi = \neg \psi$. Consider each of the two implications separately.
% \begin{itemize}
%
% \item[\fbox{$\Longrightarrow$}]
% Assume that $x \Vdash \phi$. Let $y \in W$ be such that $\left[ x \right] R_\Phi \left[ y \right]$. Then $x \sqsubseteq u \R v \sqsupseteq y$ for some $u, v \linebreak \in W$. Hence $u \Vdash \phi$ (by the definition of $\sqsubseteq$). So in particular, $v \nVdash \psi$, which implies $y \nVdash \psi$. Thus $\left[ y \right] \nVdash \psi$ by the inductive hypothesis.
%
% \item[\fbox{$\Longleftarrow$}]
% Assume that $\left[ x \right] \Vdash \phi$. Let $y \in W$ be such that $x R y$. Then $\left[ x \right] R_\Phi \left[ y \right]$ and therefore $\left[ y \right] \nVdash \psi$. Thus $y \nVdash \psi$ by the inductive hypothesis.
%
% \end{itemize}
%
% The other cases can be handled as in intuitionistic logic.
% \end{proof}

%

By a standard argument, this gives the following.

\begin{Theo}[see {\cite[Section~4]{Drobyshevich-Odintsov-2013}}]
$\mathsf{N}$ has the finite model property and is decidable.
\end{Theo}

%

Further applications can be obtained by studying what happens to a given frame property when we pass from $\mathcal{M}$ to $\mathcal{M}_\Phi$ or $\mathcal{M}^\Phi$ for a suitable $\Phi$.

%

\begin{Lemm}
Let $\mathcal{M}$, $\Phi$ and $\mathcal{M}'$ be as above, and let $\mathtt{S} \in \left\{ \mathtt{N1}^\circ, \mathtt{N2}^\circ \right\}$. Suppose $\mathcal{W} \Vdash \mathtt{S}$. Then $\mathcal{W}' \Vdash \mathtt{S}$.\footnote{Here $\mathcal{W}'$ abbreviates $\langle W_\Phi, \leqslant', R' \rangle$.}
\end{Lemm}

\begin{proof}
\fbox{$\mathtt{N1}^\circ$}~\,Since $\mathcal{W}$ is serial (see Table~\ref{table:properties}), so is $\mathcal{W}'$. Thus $\mathcal{W}' \Vdash \mathtt{N1}^\circ$.

\fbox{$\mathtt{N2}^\circ$}~\,Immediate from Lemma~\ref{Lemm:filt}~--- because $\mathtt{N2}^\circ$ may be treated as variable-free.
\end{proof}

%

\begin{Theo}
$\mathsf{N} + \left\{ \mathtt{N2}^\circ \right\}$ and $\mathsf{N}^\circ$ have the finite model property and are decidable.
\end{Theo}

%

Concerning more complex schemes:

\begin{Lemm}
Let $\mathcal{M}$ and $\Phi$ be as above. Suppose $\mathcal{W} \Vdash \mathtt{N1}^\bullet$. Then $\mathcal{W}_\Phi \Vdash \mathtt{N1}^\bullet$.
\end{Lemm}

%Perhaps $\mathtt{E}$ should be dropped here.

\begin{proof}
Note the composition of $R_\Phi$ and $\leqslant_\Phi^{-1}$ coincides with $R_\Phi$. So it suffices to show that $R_\Phi$ is symmetric (see Table~\ref{table:properties}). Let $x, y \in W$ be such that $\left[ x \right] R_\Phi \left[ y \right]$. Then $x \sqsubseteq u \R v \sqsupseteq y$ for some $u, v \in W$. Since $\R \circ \leqslant^{-1}$ is symmetric, there exists $t \in W$ such that $v \R t \geqslant u$. Hence
\[
y\ \sqsubseteq\ v\ \R\ t\ \sqsupseteq\ u\ \sqsupseteq\ x .
\]
Therefore $\left[ y \right] R_\Phi \left[ x \right]$.
\end{proof}

% \fbox{$\mathtt{E}$}~\,Let $x, y \in W$ be such that $\left[ x \right] R_\Phi \left[ y \right]$. Then $x \sqsubseteq u \R v \sqsupseteq y$ for some $u, v \in W$. Note that $\mathcal{W}$ has the property corresponding to $\mathtt{E}$. So there is $z \in W$ such that $u \R z \geqslant u, v$. Hence
% \[
% x\ \sqsubseteq\ u\ \R\ z,
% \quad
% x\ \sqsubseteq\ u\ \sqsubseteq\ z
% \quad \text{and} \quad
% y\ \sqsubseteq\ v\ \sqsubseteq\ z .
% \]
% Thus $\left[ x \right] R_\Phi \left[ z \right] \geqslant_\Phi {\left[ x \right]}, {\left[ y \right]}$.

% \begin{itemize}
%
% \item if $R$ is symmetric, i.e.\ $R \subseteq R^{-1}$, then so is $R_\Phi$;
%
% \item if $R$ is weakly dense, i.e.\ $R \subseteq R \circ R^{-1}$, then so is $R_\Phi$.
%
% \end{itemize}

%

\begin{Theo} \label{Theo:N11-dec}
$\mathsf{N} + \left\{ \mathtt{N1}^\bullet \right\}$ and $\mathsf{N}^\circ + \left\{ \mathtt{N1}^\bullet \right\}$ have the finite model property and are decidable.
\end{Theo}

%

For each $\Phi \subseteq \F$, denote by $N \left( \Phi \right)$ the closure of $\Phi$ under negation, i.e.\ the least set $\Psi$ of formulas such that $\Phi \subseteq \Psi$ and $\left\{ \neg \phi \mid \phi \in \Psi \right\} \subseteq \Psi$. Notice that the scheme ${\neg \neg \phi} \leftrightarrow {\neg \neg \neg \neg \phi}$ can be derived in $\mathsf{N} + \left\{ \mathtt{N1}^\bullet \right\}$ as follows:
\begin{hilbert}
${\neg \phi} \rightarrow {\neg \neg \neg \phi}$
&$\mathtt{N1}^\bullet$\\
${\neg \neg \neg \neg \phi} \rightarrow {\neg \neg \phi}$
&from 1 (by $\mathtt{CR}$)\\
${\neg \neg \phi} \rightarrow {\neg \neg \neg \neg \phi}$
&$\mathtt{N1}^\bullet$\\
${\neg \neg \phi} \leftrightarrow {\neg \neg \neg \neg \phi}$
&from 2, 3.
\end{hilbert}
Hence if $\Phi \subseteq \F$ is finite, then $N \left( \Phi \right)$ may be treated as finite modulo $\mathsf{N} + \left\{ \mathtt{N1}^\bullet \right\}$, so $N \left( \Phi \right)$ is finitely based over any model whose frame validates $\mathtt{N1}^\bullet$.\footnote{It
follows that for any $\mathcal{M}$ and $\Phi$ as above, if $\mathcal{W} \Vdash \mathtt{N1}^\bullet$ and $\Phi$ is finite, then $W_{N \left( \Phi \right)}$ is finite~--- though $N \left( \Phi \right)$ is infinite, provided that $\Phi \ne \varnothing$.}

%

\begin{Lemm} \label{Lemm:N11-cfilt}
Let $\mathcal{M}$ and $\Phi$ be as above. Suppose $\mathcal{W} \Vdash \mathtt{N1}^\bullet$. Then $\mathcal{W}^{N \left( \Phi \right)} \Vdash \mathtt{N1}^\bullet$.
\end{Lemm}

\begin{proof}
For convenience, denote $N \left( \Phi \right)$ by $\Psi$. Let $x, y \in W$ be such that $\left[ x \right] R^\Psi \left[ y \right]$. For every $\phi \in \Psi$, if $\mathcal{M}, x \Vdash \phi$, then $\mathcal{M}, x \Vdash {\neg \neg \phi}$ (by $\mathtt{N1}^\bullet$), and therefore $\mathcal{M}, y \nVdash {\neg \phi}$ (because $\neg \phi \in \Psi$ and $\left[ x \right] R^\Psi \left[ y \right]$). Thus $\left[ y \right] R^\Psi \left[ x \right]$.
\end{proof}

%

This gives us another way of proving Theorem~\ref{Theo:N11-dec}.

%Call $\Gamma \subseteq \F$ \emph{finitely based over $\mathcal{M}$} iff there exists a finite $\Delta \subseteq \F$ such that for every $\phi \in \Gamma$ there exists $\psi \in \Delta$ such that $\mathcal{M} \Vdash \phi \leftrightarrow \psi$.

%

For each $\Phi \subseteq \F$ we denote by $C \left( \Phi \right)$ the closure of $\Phi$ under conjunction, disjunction and negation. Evidently, the scheme ${\neg \phi} \leftrightarrow {\neg \neg \neg \phi}$ can be derived in $\mathsf{N} + \left\{ \mathtt{N2}^\bullet \right\}$:
\begin{hilbert}
${\neg \neg \phi} \rightarrow \phi$
&$\mathtt{N2}^\bullet$\\
${\neg \phi} \rightarrow {\neg \neg \neg \phi}$
&from 1 (by $\mathtt{CR}$)\\
${\neg \neg \neg \phi} \rightarrow {\neg \phi}$
&$\mathtt{N2}^\bullet$\\
${\neg \phi} \leftrightarrow {\neg \neg \neg \phi}$
&from 2, 3.
\end{hilbert}
Also, it is known that the following schemes are derivable in $\mathsf{N} + \left\{ \mathtt{N}^\ast \right\}$, and hence in $\mathsf{N} + \left\{ \mathtt{N2}^\bullet \right\}$ (by Proposition~\ref{Prop:Obs}):
\begin{itemize}

\item $\neg \left( \phi \vee \psi \right) \leftrightarrow \left( {\neg \phi} \wedge {\neg \psi} \right)$;

\item $\neg \left( \phi \wedge \psi \right) \leftrightarrow \left( {\neg \phi} \vee {\neg \psi} \right)$.

\end{itemize}
Consequently, if $\Phi \subseteq \F$ is finite, then $C \left( \Phi \right)$ may be treated as finite modulo $\mathsf{N} + \left\{ \mathtt{N2}^\bullet \right\}$, so $C \left( \Phi \right)$ is finitely based over any model whose frame validates $\mathtt{N2}^\bullet$.

%For each $\Phi \subseteq \F$ we denote by $C \left( \Phi \right)$ the collection of all formulas that can be built from elements of $\Phi$ using $\wedge$, $\vee$ and $\neg$.

%

\begin{Lemm}
Let $\mathcal{M}$ and $\Phi$ be as above, with $\Phi$ finite. Suppose $\mathcal{W} \Vdash \mathtt{N2}^\bullet$. Then $\mathcal{W}^{C \left( \Phi \right)} \Vdash \mathtt{N2}^\bullet$.
\end{Lemm}

\begin{proof}
For convenience, take $\Psi := C \left( \Phi \right)$. Assume, by way of contradiction, that $\mathcal{W}^\Psi$ does~not have the property corresponding to $\mathtt{N2}^\bullet$, i.e.\ there exists $x \in W$ such that for every $y \in W$,
\[
{\left[ x \right] R^\Psi \left[ y \right]}
\quad \Longrightarrow \quad
\begin{tabular}{c}
there exists $z \in W$ such that\\[0.25em]
$\left[ y \right] R^\Psi \left[ z \right]$ and $\left[ z \right] \not \leqslant^\Psi \left[ x \right]$.
\end{tabular}
\]
For each $y \in W$ such that $\left[ x \right] R^\Psi \left[ y \right]$, choose $z_y \in W$ and $\phi_y \in \Psi$ satisfying
\[
{\left[ y \right] R^\Psi \left[ z_y \right]} ,
\quad
\mathcal{M}, z_y \Vdash \phi_y
\quad \text{and} \quad 
\mathcal{M}, x \nVdash \phi_y .
\] %they exist by the assumption
Take $\Theta$ to be $\left\{ \phi_y \mid y \in W ~ \text{and} ~ {\left[ x \right] R^\Psi \left[ y \right]} \right\}$. Obviously, since $\mathcal{W}$ is serial (recall Pro\-po\-si\-ti\-on~\ref{Prop:Obs}), $\Theta$ is non-empty. Moreover, it can be treated as a finite set (see the comments made just before this lemma). Consider
\[
\theta\ :=\ {\bigvee \Theta} .
\]
We have $\mathcal{M}, x \nVdash \theta$, which implies $\mathcal{M}, x \nVdash {\neg \neg \theta}$ (by $\mathtt{N2}^\bullet$), so $\mathcal{M}^\Psi, \left[ x \right] \nVdash {\neg \neg \theta}$ by Lemma~\ref{Lemm:filt}.
On the other hand, for every $y \in W$, if $\left[ x \right] R^\Phi \left[ y \right]$, then $\mathcal{M}, z_y \Vdash \theta$, so $\mathcal{M}^\Psi, \left[ z_y \right] \Vdash \theta$ by Lemma~\ref{Lemm:filt}, and therefore $\mathcal{M}^\Psi, \left[ y \right] \nVdash \neg \theta$. Thus $\mathcal{M}^\Psi, \left[ x \right] \Vdash {\neg \neg \theta}$, a  contradiction.
\end{proof}

%

\begin{Theo} \label{Theo:Hype-dec}
$\mathsf{N}^\ast + \left\{ \mathtt{N2}^\bullet \right\}$ and $\mathsf{N}^\bullet$ have the finite model property and are decidable.
\end{Theo}

%%%

%\pagebreak
\subsection{More specific filtrations}

Now we are going to present a different way of proving Theorem~\ref{Theo:Hype-dec}. It uses a special kind of filtration suitable for Routley models whose frames validate $\mathtt{N1}^\bullet$ or $\mathtt{N2}^\bullet$.

Fix a Routley model $\mathbf{M}$. Let $\Phi \subseteq \F$ be closed under subformulas and under negation~--- so in particular, $N \left( \Phi \right) = \Phi$. Define the \emph{special $\Phi$-filtration of $\mathbf{M}$} to be
\[
\mathbf{M}_\Phi\ =\ \langle \langle W_\Phi, \leqslant_\Phi, \ast_\Phi \rangle, \xi_\Phi \rangle
\]
where $W_\Phi$, $\leqslant_\Phi$ and $\xi_\Phi$ are as before, and $\ast_\Phi$ maps each $\left[ x \right]$ in $W_\Phi$ to $\left[ x^\ast \right]$. Note that since $\Phi$ is closed under negation, the definition of $\ast_\Phi$ is correct; furthermore, one can easily check that $\ast_\Phi$ is anti-monotone with respect to $\leqslant_\Phi$. Thus $\mathbf{M}_\Phi$ is a Routley model. Naturally, we~shall~abbreviate~$\langle W_\Phi, \leqslant_\Phi, \ast_\Phi \rangle$ to $\mathbf{W}_\Phi$.

%

\begin{Lemm} \label{Lemm:fil-star}
Let $\mathbf{M}$ and $\Phi$ be as above. Then for any $x \in W$ and $\phi \in \Phi$,
\[
\mathbf{M}, x \Vdash \phi
\quad \Longleftrightarrow \quad
\mathbf{M}_\Phi, {\left[ x \right]} \Vdash \phi .
\]
\end{Lemm}

\begin{proof}
By induction on the complexity of $\phi$.

The case where $\phi \in \mathrm{Prop}$ is trivial.

Suppose $\phi = \neg \psi$. Then
\begin{align*}
\mathbf{M}, x \Vdash \phi
\quad &\Longleftrightarrow \quad
\mathbf{M}, x^\ast \nVdash \psi\\
\quad &\Longleftrightarrow \quad
\mathbf{M}_\Phi, {\left[ x^\ast \right]} \nVdash \psi\\
\quad &\Longleftrightarrow \quad
\mathbf{M}_\Phi, {\left[ x \right]}^\ast \nVdash \psi\\
\quad &\Longleftrightarrow \quad
\mathbf{M}_\Phi, {\left[ x \right]} \Vdash \phi
\end{align*}
where ${\left[ x \right]}^\ast$ stands for $\ast_\Phi \left( \left[ x \right] \right)$, of course.

The other cases can be handled as in intuitionistic logic.
\end{proof}

%

\begin{Lemm}
Let $\mathbf{M}$ and $\Phi$ be as above, and let $\mathtt{S} \in \left\{ \mathtt{N1}^\bullet, \mathtt{N2}^\bullet \right\}$. Suppose $\mathbf{W} \Vdash \mathtt{S}$. Then $\mathbf{W}_\Phi \Vdash \mathtt{S}$.
\end{Lemm}

\begin{proof}
It is easy to check that for every Routley frame $\mathbf{W}'$:
\begin{align*}
\mathbf{W}' \Vdash \mathtt{N1}^\bullet
\quad &\Longleftrightarrow \quad
{x \leqslant x^{\ast \ast}} \enskip \text{for all} ~ {x \in W'} ;\\
\mathbf{W}' \Vdash \mathtt{N2}^\bullet
\quad &\Longleftrightarrow \quad
{x^{\ast \ast} \leqslant x} \enskip \text{for all} ~ {x \in W'} .
\end{align*}
In particular, this holds for $\mathbf{W}' \in \left\{ \mathbf{W}, \mathbf{W}_\Phi \right\}$.

\fbox{$\mathtt{N1}^\bullet$}~\,For every $x \in W$ we have $\left[ x \right] \leqslant_\Phi \left[ x^{\ast \ast} \right] = {\left[ x^\ast \right]}^\ast = {\left[ x \right]}^{\ast \ast}$. Thus $\mathbf{W}_\Phi \Vdash \mathtt{N1}^\bullet$.

\fbox{$\mathtt{N2}^\bullet$}~\,Similarly to $\mathtt{N1}^\bullet$.
\end{proof}

%

This leads to a refinement of Theorem~\ref{Theo:Hype-dec}:

\begin{Theo}
$\mathsf{N}^\ast + \left\{ \mathtt{N1}^\bullet \right\}$, $\mathsf{N}^\ast + \left\{ \mathtt{N2}^\bullet \right\}$ and $\mathsf{N}^\bullet$ have the finite model property in terms of Routley models and are decidable.
\end{Theo}

%%%

\section{Further discussion}

One may wish to look at $\mathsf{N}$ and its extensions from a somewhat more general point of view. In particular, following \cite{Vakarelov-1989}, Do\v{s}en's semantics can be modified by replacing $\langle W, \leqslant, R \rangle$ by $\langle W, \leqslant, R, N \rangle$
where $N$ is a subset of $W$ such that for any $x, y \in W$,
\[
x\ \in\ N
\quad \text{and} \quad
x\ \leqslant y
\quad \Longrightarrow \quad
y \in N
\]
(the elements of $N$ are called \emph{normal worlds}). Then $\mathcal{M}, x \Vdash \phi$ is defined as before, except that the negation clause becomes a bit more complicated:
\[
\mathcal{M}, x \Vdash {\neg \psi}
\quad :\Longleftrightarrow \quad
{\left( \mathcal{M}, y \nVdash \psi \quad \text{for all} \enskip {y \in R \left( x \right)} \right)}
\enskip \text{and} \enskip
x \in N .
\]
Naturally, some of the claims made with Do\v{s}en's semantics in mind may fail when we pass to the modified semantics. One may proceed to study the problems discussed above in this more general setting.

%%%

%\newpage
\begin{thebibliography}{99}

\bibitem{Bezhanishvili-Colacito-de-Jongh-2019}
N.\ Bezhanishvili, A.\ Colacito, D.\ de Jongh.
A study of subminimal logics of negation and their modal companions.
In: A.\ Silva et al., eds., \emph{Language, Logic, and Computation: Proceedings of the 12th International Tbilisi Symposium}, LNCS 11456,
Springer, 2019, 21--41.

\bibitem{Cabalar-Odintsov-Pearse-2006} %
P.\ Cabalar, S.\,P.\ Odintsov, D.\ Pearce.
Logical foundations of well-founded semantics.
In: P.\ Doherty et al., eds., \emph{Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning},
AAAI Press, 2006, 25--36.

\bibitem{Dosen-1986} %
K.\ Do\v{s}en.
Negation as a modal operator.
\emph{Reports on Mathematical Logic} {\bf 20} (1986), 15--27.

\bibitem{Drobyshevich-Odintsov-2013} %
S.\,A.\ Drobyshevich, S.\,P.\ Odintsov.
Finite model property for negative modalities.
\emph{Siberian Electronic Mathematical Reports} {\bf 10} (2013), 1--21. [In Russian.]

\bibitem{Hazen-1995}
A.\,P.\ Hazen.
Is even minimal negation constructive?
\emph{Analysis} {\bf 55}:2 (1995), 105--107.
 
\bibitem{Leitgeb-2019} %
H.\ Leitgeb.
HYPE: A system of hyperintensional logic (with an application to semantic pa\-ra\-dox\-es).
\emph{Journal of Philosophical Logic} {\bf 48}:2 (2019), 305--405.
%\href{http://dx.doi.org/10.1007/s10992-018-9467-0}{doi:\,10.1007/s10992-018-9467-0}

\bibitem{Moisil-1942} %
G.\,C.\ Moisil.
Logique modale.
\emph{Disquisitiones Mathematicae et Physica} {\bf 2} (1942), 3--98.

\bibitem{Odintsov-Wansing-2021} %
S.\,P.\ Odintsov and H.\ Wansing.
Routley star and hyperintensionality.
\emph{Journal of Philosophical Logic} {\bf 50}:1 (2021), 33--56.
%DOI: 10.1007/s10992-020-09558-5

\bibitem{Odintsov-2010} %
S.\,P.\ Odintsov.
Combining intuitionistic connectives and Routley negation.
\emph{Siberian Elec\-tro\-nic Mathematical Reports} {\bf 7} (2010), 21--41.
%Available at \href{http://semr.math.nsc.ru/v7/p21-41.pdf}{http://semr.math.nsc.ru/}

\bibitem{Segerberg-1968}
K.\ Segerberg.
Propositional logics related to Heyting's and Johansson's.
\emph{Theoria} {\bf 34}:1 (1968), 26--61.
%DOI: 10.1111/j.1755-2567.1968.tb00337.x

\bibitem{Speranski-2020} %
S.\,O.\ Speranski.
Negation as a modality in a quantified setting.
\emph{Journal of Logic and Com\-pu\-ta\-tion} {\bf 31}:5 (2021), 1330--1355.
%\href{http://dx.doi.org/10.1093/logcom/exab025}{doi:\,10.1093/logcom/exab025}

\bibitem{Vakarelov-1989} %
D.\ Vakarelov.
Consistency, completeness and negation.
In: G.\ Priest et al., eds., \emph{Paraconsistent Logics. Essays on the Inconsistent},
Philosophia Verlag, 1989, 238--363.

\end{thebibliography}

%%%

\end{document}
