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



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





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


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

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



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

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

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

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




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




\thispagestyle{empty}

\title[Minimal logic with linearity axiom]{\large On extensions of minimal logic with linearity axiom}


\author[D.M. ANISHCHENKO, S.P. ODINTSOV]{{\bf D.M. Anishchenko},\ {\bf S.P. Odintsov}\protect\orcidicon{0000-0003-3115-1293}}



	\address{Dmitriy Mikhailovich Anishchenko
	\newline\hphantom{iii} Novosibirsk State University,
	\newline\hphantom{iii} ul. Pirogova, 1,
	\newline\hphantom{iii} 630090, Novosibirsk, Russia}%
\email{d.anishchenko@g.nsu.ru}%
\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 Anishchenko D.M., Odintsov S.P.,
On extensions of minimal logic with linearity axiom}
\thanks{\copyright \ 2024 Anishchenko D.M., Odintsov S.P.}
\thanks{\rm The work is supported by  State Contracts of the Sobolev Institute of Mathematics (Project FWNF-2022-0012)}
\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:} The Dummett logic is a superintuitionistic logic obtained by adding the linearity axiom to intuitionistic logic. This is one of the first non-classical logics, whose lattice of axiomatic extensions was completely described. In this paper we investigate the logic $JC$ obtained via adding the linearity axiom to minimal logic of Johansson. So $JC$ is a natural paraconsistent analog of the Dummett logic. We describe the lattice of $JC$-extensions, prove that every element of this lattice is finitely axiomatizable, has the finite model property, and is decidable. Finally, we prove that $JC$ has exactly two pretabular extensions. \medskip

\noindent{\bf Keywords:} Dummett's logic, minimal logic, linearity axiom, lattice of extensions, algebraic semantics, $j$-algebra, opremum, decidability, pretabularity.
 \end{quote}
}

\bigskip
The {\em Dummett logic} (or {\em G\"{o}del-Dummett logic}, or {\em logic of chains}) $LC$ is an important superintuitionistic logic obtained by adding to intuitionistic logic $Int$ the linearity axiom $ ( p \rightarrow q ) \vee ( q \rightarrow p ) $.

In 2003 J. von Plato \cite{Plato2003} opened for the logical community that a logical system equivalent to $LC$  was introduced in the work by T.~Skolem written in 1913 \cite{Skolem1913}. It is remarkable that this work was written in the setting of Schr\"{o}der's algebraic approach, which differs essentially from the dominating Frege-Russel-Hilbert tradition. This difference von Plato describes \cite[p.~153]{Plato2003} as follows: `Logic is not tied to a strict formal syntax, but studies the relations between concepts in a direct way. The situation is similar to mathematics in general, where one usually studies the structures of interest, say arithmetic, without the mediation of a concrete formal syntax'.  The main technical result of Skolem's work is the discovery of a normal form of formulas.  In $LC$ every formula is equivalent to a disjunction of conjunctions or a conjunction of disjunctions of formulas  of the form  $(p \rightarrow q)$ or  $\neg(p \rightarrow q)$, where $p$ and $q$ are propositional variables.

The rediscovery of $LC$ by M.~Dummett was inspired by K.~G\"{o}del \cite{Godel1932}, who constructed a sequence of matrices to prove the non-tabularity of intuitionistic logic. In 1959 M.~Dummett \cite{Dummett1959} introduced $LC$  as the extension of the intuitionsitic logic via the linearity axiom and proved that $LC$ is complete w.r.t. the family of matrices introduced in \cite{Godel1932}. 

Later D.~Ulrich \cite{Ulrich1970} proved that every $LC$ extension has the finite model property. Finally, M.~Dunn and R.~Meyer \cite{DunnMeyer1971} have found out all proper extensions of $LC$. It turns out that all such extensions are tabular, which strengthens the results of Ulrich and implies the pretabularity of $LC$. Notice that one year later L.~Maksimova \cite{Maksimova1972} proved that there are exactly three pretabular superintuitionistic logics. Naturally, $LC$ is one of such logics.

Recall that a logic is called {\em paraconsistent}, if it admits theories that are contradictory, but however non-trivial. Logics with trivial contradictory theories are  called {\em explosive}. Minimal logic $J$ of Johansson \cite{Johansson1937} can be obtained from $Int$ via omitting the axiom {\em ex contradictione quodlibet} $ECQ:=\neg p \rightarrow (p \rightarrow q)$, more exactly, $Int=J+ECQ$. This is a natural paraconsistent analog of intuitionistic logic. 

%\medskip
\begin{center}
	\parbox{10mm}{
		\begin{picture}(20,140)(0,0)
			\put(10,120){\circle*{2}} \put(10,100){\circle*{2}}
			\put(10,40){\circle*{1}} \put(10,35){\circle*{1}}
			\put(10,30){\circle*{1}} \put(10,60){\circle*{2}} \put(10,80){\circle*{2}}
			\put(10,10){\circle*{2}}
			
			\put(13,8){$LC$} \put(13,58){$L_4$} \put(13,78){$L_3$} \put(13,98){$CL$}
			\put(13,118){$\mathrm{Form}$} \put(10,60){\line(0,1){60}}
		\end{picture}
	}
\end{center}

%\medskip
\centerline{Figure 1. The lattice $\mathcal{E}LC$.}

\bigskip
The main object of our investigations is the logic $JC$ obtained by adding the linearity axiom to $J$. So $JC$ can be considered as a paraconsistent analog of the Dummett logic $LC$. We transfer the results by M.~Dunn and R.~Meyer  to the logic $JC$. Except for description of the lattice of $JC$-extensions we prove that every such extension is  finitely axiomatizable modulo $JC$, has the finite model property, and is decidable as a consequence. Finally, we prove that the logic $JC$ has exactly two pretabular extensions, one of which coincides with $LC$.

It should be noted that $LC$ is one of the first non-classical logics, whose lattice of extensions was completely described. Earlier such description was obtained for the modal logic $S5$ \cite{Scroggs1951} and for the logic $RM$ \cite{Dunn1970}, an extension of the  relevant logic $R$ with so called mingle-axiom. The lattice $\mathcal{E}LC$ of all $LC$-extensions is an infinite descending chain with the least element as presented at Figure~1. The greatest element $\mathrm{Form}$ is the trivial logic consisting of all formulas, the second element is the classical logic $CL$, the logic $L_n$ is determined by the $n$-element linearly ordered Heyting algebra.

M.~Kracht \cite{Kracht1998} studied extensions of the constructive Nelson's logic $N3$ with strong negation. In particlular, he described the lattice of extensions of the logic $N3C=N3+\{(p\rightarrow q)\vee(q\rightarrow p)\}$, a conservative extension of $LC$.  As we can see from Figure~2 this lattice is essentially more complicated then $\mathcal{E}LC$, but still admits an explicit presentation.

%\smallskip
\begin{center}
	\parbox{60mm}{
		\begin{picture}(140,197)(0,0)
			
			\put(90,0){\circle*{2}}
			
			\put(90,60){\circle*{2}}
			\put(90,90){\circle*{2}}
			\put(90,120){\circle*{2}}
			\put(90,150){\circle*{2}}
			\put(90,180){\circle*{2}}
			%\put(90,195){\circle*{2}}
			
			\put(0,90){\circle*{2}}
			\put(15,75){\circle*{2}}
			\put(30,60){\circle*{2}}
			\put(30,120){\circle*{2}}
			\put(45,45){\circle*{2}} 
			\put(45,105){\circle*{2}}
			\put(45,135){\circle*{2}}
			
			
			\put(60,30){\circle*{2}}
			 \put(60,90){\circle*{2}}
			 \put(60,120){\circle*{2}}
			 \put(60,150){\circle*{2}}
			
			 \put(75,165){\circle*{2}}
			 \put(75,135){\circle*{2}}
		 
			\put(75,105){\circle*{2}} 
			\put(75,75){\circle*{2}} 
		
			
			\put(10,100){\circle*{1}} 
			\put(15,105){\circle*{1}}
			\put(20,110){\circle*{1}} 
			
			\put(25,85){\circle*{1}}
			\put(30,90){\circle*{1}} 
			\put(35,95){\circle*{1}}
			
			\put(40,70){\circle*{1}} 
			\put(45,75){\circle*{1}}
			\put(50,80){\circle*{1}} 
			
			\put(55,55){\circle*{1}}
			\put(60,60){\circle*{1}} 
			\put(65,65){\circle*{1}}
			
			\put(70,40){\circle*{1}} 
			\put(75,45){\circle*{1}}
			\put(80,50){\circle*{1}} 
			
			\put(70,20){\circle*{1}}
			\put(75,15){\circle*{1}} \put(80,10){\circle*{1}}
			
			\put(30,120){\line(1,1){60}} \put(45,105){\line(1,1){45}}
			\put(60,90){\line(1,1){30}} \put(75,75){\line(1,1){15}}
			\put(0,90){\line(1,-1){60}} \put(30,120){\line(1,-1){60}}
			\put(45,135){\line(1,-1){45}} \put(60,150){\line(1,-1){30}}
			\put(75,165){\line(1,-1){15}}
			
			
			 \put(80,-14){${\bf N3C}$} \put(80,183){$\mathrm{Form}$}
			
		\end{picture}
	}
\end{center}

\vspace{7mm}
\centerline{Figure 2. The lattice $\mathcal{E}N3C$.}

\medskip
Later S.~Odintsov \cite{Odintsov2007} described the lattice of extesions of the logic $N4C=N4 +\{(p\rightarrow q)\vee(q\rightarrow p)\}$, where $N4$ is the paraconsistent version of the constructive Nelson's logic,  $N3=N4+\{ \mathord{\sim} p\rightarrow (p\rightarrow q)\}$. $N4C$ also is  a conservative extension of $LC$. It turns out that the lattice $\mathcal{E}N4C$ has much more complicated structure as compared to $\mathcal{E}N3C$ and we cannot draw a diagramm presenting explicitly the structure of this lattice. As we will see the same holds for the lattice of $JC$-extensions.  To explain the nature of such complications we say a few words on methods that are used to describe the lattice of extensions of one or another logic. Usually we deal with logics which can be characterized via varieties of algebras. Every variety is generated by its finitely generated subdirectly irreducible algebras ($\mathsf{fsi}$-algebras). So first we describe the  $\mathsf{fsi}$-algebras modelling the logic $L$ we are interested in. Temporarily we denote this class of algebras as $\mathrm{Mod}_\mathsf{fsi}(L)$. Further, we consider the preorder $\sqsubseteq$ on $\mathrm{Mod}_\mathsf{fsi}(L)$ defined as follows:
\[ \mathbf{A}\sqsubseteq\mathbf{B}\ \ \Leftrightarrow\ \ L\mathbf{A}\subseteq L\mathbf{B}, \] 
where $L\mathbf{A}$ denotes the logic of $\mathbf{A}$, i.e. the set of all formulas valid on the algebra  $\mathbf{A}$. Naturally, this preorder is stable under isomorphisms, and factoring out the preorder $\langle \mathrm{Mod}_\mathsf{fsi}(L), \sqsubseteq \rangle$ w.r.t. the isomorphism relation we obtain the partial order $\mathcal{P}_\mathsf{fsi} L$ of isomorphism types of $\mathsf{fsi}$-algebras modelling $L$. It is clear that for a logic $L'$ extending $L$ isomorphism types of algebras from $\mathrm{Mod}_\mathsf{fsi}(L')$ form a cone (upward closed subset) of $\mathcal{P}_\mathsf{fsi} L$, and that different cones correspond to different $L$-extensions. Usually it is possible to prove that just defined mapping from $\mathcal{E}(L)$ to the cone lattice of $\mathcal{P}_\mathsf{fsi} L$ is onto, and that this is a dual isomorphism of lattices. 

The simple structure of $\mathcal{E}LC$ is explained by the fact that its partial order $\mathcal{P}_\mathsf{fsi} LC$ is linear. Due to this reason the lattice of cones of this order is linear too. The order  $\mathcal{P}_\mathsf{fsi} N3C$ consists of two infinite chains connected one with the other. In case of $N4C^\bot$ the order $\mathcal{P}_\mathsf{fsi} N4C^\bot$ has an explicite description, but it is much more complicated, so one can describe $\mathcal{E}N4C^\bot$ only as the lattice dually isomorphic to the cone lattice of $\mathcal{P}_\mathsf{fsi} N4C^\bot$. The same holds for the logic $JC$ investigated in this article.

Our paper is structured as follows. Section 1 is devoted to preliminary remarks. In Section~2 we describe the partial order $\mathcal{P}_\mathsf{fsi} JC$ and cones of this order. Finally, in Section~3 we establish that $\mathcal{E}JC$ and the cone lattice of $\mathcal{P}_\mathsf{fsi} JC$ are dually isomorphic, prove that all elements of $\mathcal{E}JC$ are finitely axiomatizable and decidable, and find out pretabular $JC$-extensions.  


\section{Preliminaries}

We consider logics defined in the propositional language $\mathcal{L} = \{ \vee, \wedge
, \rightarrow, \bot \}$ containing the binary connectives of disjunction, conjunction, implication, and the absurdity constant. Formulas of this language ($\mathcal{L}$-formulas) are constructed in a standard way from $\bot$ and propositional variables occuring to a fixed countable set $\mathrm{Prop}$ with the help of logical connectives. The negation connective we consider as an abbreviation, $\neg \varphi:=\varphi \rightarrow \bot$. The set of all $\mathcal{L}$-formulas is denoted as $\mathrm{Form}_{\mathcal{L}}$. We write $\varphi(p_1,\ldots,p_n)$ for $\varphi\in\mathrm{Form}_{\mathcal{L}}$ in case all propositional variables occuring $\varphi$ are among $p_1$, \ldots, $p_n$. 

By a {\em logic}  $L$ we mean a set of formulas ($L\subseteq\mathrm{Form}_{\mathcal{L}}$) closed under the rules of substitution (SUB) and {\em modus ponens} (MP):
\[ (\mbox{SUB})\ \ \frac{\varphi(p_1,\ldots,p_n)}{\varphi(\psi_1,\ldots,\psi_n)}, \ \ \ \ \ 
(\mbox{MP})\ \ \frac{\varphi\ \ \ \varphi\rightarrow\psi}{\psi}, \]
where $\varphi$,$\psi$,$\psi_1,\ldots,\psi_n\in\mathrm{Form}_{\mathcal{L}}$. 

For a logic $L$, we denote by $\mathcal{E} L$ the set of all logics containing $L$.   Set-theoretical intersection $\cap$ and the operation $+$, where $L_1 + L_2$ is the least logic containing $L_1\cup L_2$, turn $\mathcal{E} L$ to a complete lattice. This follows from the fact that the intersection of any family of logics is a logic too. We  call $\mathcal{E} L$ the {\em lattice of $L$-extensions}.   If $X\subseteq\mathrm{Form}_{\mathcal{L}}$, then $L+X$ denotes the least logic in $\mathcal{E} L$ containing $X$.

{\em Minimal logic} or {\em Johansson's logic} $J$ is the least logic containing the following formulas:

\medskip
\begin{tabular}{l l}
	$ J1. \; \; p \rightarrow (q \rightarrow p) $; &
	$ J2. \; \; (p \wedge q) \rightarrow p $; \\
	$ J3. \; \; (p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r)) $; &
	$ J4. \; \; (p \wedge q) \rightarrow q $; \\
	$ J5. \; \; (p \rightarrow q) \rightarrow ((p \rightarrow r)
	\rightarrow (p \rightarrow (q \wedge r))) $; &
	$ J6. \; \; p \rightarrow (p \vee q) $; \\
	$ J7. \; \; (p \rightarrow r) \rightarrow ((q \rightarrow r)
	\rightarrow ((p \vee q) \rightarrow r)) $; &
	$ J8. \; \; q \rightarrow (p \vee q) $. \\
\end{tabular} \\

\medskip

Now {\em intuitionistic logic} $Int$ can be defined as $Int=J+\{ \bot\rightarrow p\}$, and {\em classical logic} as $CL=Int+\{ p\vee\neg p\}$.

Put:
\[ JC=J+\{ (p\rightarrow q)\vee(q\rightarrow p) \},\ \ \ LC=Int+\{ (p\rightarrow q)\vee(q\rightarrow p) \}.\] 
Logic $LC$ is the {\em logic of chains} or the {\em Dummett logic}. The main object of our investigations  is logic $JC$, a natural paraconsistent analog of the Dummett logic.

Now we consider an algebraic semantics for logics from $\mathcal{E} J$. Algebras we denote by boldface uppercase letters, the universes of algebras by corresponding italic uppercase letters.


An {\em implicative lattice} is an algebra $ {\bf A} = \langle A, \wedge, \vee, \rightarrow \rangle$ such that its reduct $ \langle A, \wedge, \vee \rangle $ is a lattice and the operation $\rightarrow$ satisfies the following equivalence for all $a, b, c \in A$:
$$ c \leq_\mathbf{A} a \rightarrow b \Leftrightarrow c \wedge a \leq_\mathbf{A} b,$$
where $\leq_\mathbf{A}$ denotes the lattice ordering of $ \langle A, \wedge, \vee \rangle $. Recall that $a\leq_\mathbf{A} b$ iff $a\wedge b=a$.

It is easy to see that for every $a\in A$, the implication $a\rightarrow a$ is the greatest element of $\mathbf{A}$ w.r.t. $\leq_\mathbf{A}$. In what follows the greatest element of $\mathbf{A}$ we denote as $1_\mathbf{A}$. The next property of implication readily follows from its definition:
\begin{equation}
	a\rightarrow b=1_\mathbf{A}\ \ \text{iff}\ \ a\leq_\mathbf{A} b \ \ \text{for any} \ a,b\in A
	\label{imp_unit}
\end{equation}

It is well known that every implicative lattice is distributive and that the class $\mathcal{V}_{imp}$ of all implicative lattices is a variety, i.e. this class can be axiomatized by identities (see, e.g., \cite{Rasiowa1974})

An algebra ${\bf A} = \langle A, \wedge, \vee, \rightarrow, \perp \rangle $ is called a $j${\em -algebra} if its $\bot$-free reduct $ \langle A, \wedge, \vee, \rightarrow \rangle $ is an implicative lattice.

A $j$-algebra ${\bf A} = \langle A, \wedge, \vee, \rightarrow, \perp \rangle $ is called a {\em Heyting algebra} ({\em negative algebra}) if $\perp$ is the least (greatest) element of $\mathbf{A}$ with respect to $\leq_\mathbf{A}$.

Obviously, the class $\mathcal{V}_j$ of all $j$-algebras,  the class $\mathcal{V}_H$ of all Heyting algebras, and the class $\mathcal{V}_{neg}$ of all negative algebras are varieties too.

Let $\mathbf{A}$ be a $j$-algebra. Every homomorphism $v:\mathrm{Form}_\mathcal{L}\rightarrow\mathbf{A}$ from the algebra of formulas into $\mathbf{A}$ is called an $\mathbf{A}$-{\em valuation}. For every formula $\varphi$, we say that $\varphi$ is {\em true at} an $\mathbf{A}$-valuation $v$ and write $\mathbf{A},v\models\varphi$ if $v(\varphi)=1_\mathbf{A}$. We say that $\varphi$ is {\em true on} $\mathbf{A}$ and write $\mathbf{A}\models\varphi$ if $\mathbf{A},v\models\varphi$ holds for every $\mathbf{A}$-valuation $v$.

For a set $\Gamma$ of formulas, we write $\mathbf{A}\models\Gamma$ and say that $\mathbf{A}$ is a {\em model for} $\Gamma$ if $\mathbf{A}\models\varphi$ for all $\varphi\in\Gamma$. 

Let $\mathcal{K}$ be a class of $j$-algebras. We write $\mathcal{K}\models\varphi$ if $\mathbf{A}\models\varphi$ for all $\mathbf{A}\in\mathcal{K}$, and $\mathcal{K}\models\Gamma$ if $\mathcal{K}\models\varphi$ for all $\varphi\in\Gamma$.

For an algebra $\mathbf{A}$, the lattice of its congruences  is denoted by $\mathrm{Con}(\mathbf{A})$. For a variety $\mathcal{V}$, we denote by $\mathrm{Sub}(\mathcal{V})$ the lattice of its subvarieties. In both cases, the lattice ordering coincides with the inclusion relation, see \cite{BurrSanka} for details. Moreover, it is known that the variety $\mathcal{V}_j$ of all j-algebras is congruence-dustributive, i.e. the lattice $\mathrm{Con}(\mathbf{A})$ is distributive for every $\mathbf{A}\in\mathcal{V}_j$.

Congruences of a $j$-algebra ${\bf A}$ are is one-to-one correspondence with filters on $\mathbf{A}$. Recall that a  non-empty subset $F\subseteq A$ is a {\em filter on} a $j$-algebra $\mathbf{A}$ if for every $a,b\in A$: (i) $a\in F$ and $b\in F$ imply $a\wedge b\in F$; (ii) $a\leq_\mathbf{A} b$ and $a\in F$ imply $b\in F$.  The lattice of all filters on $\mathbf{A}$ we denote $\mathcal{F}(\mathbf{A})$. For every $\theta\in\mathrm{Con}(\mathbf{A})$ and every $F\in\mathcal{F}(\mathbf{A})$ we put:
\[ F_\theta:=\{ a\in A \mid (a,1_\mathbf{A})\in\theta\}, \ \ \ \theta_F:=\{ (a,b)\mid a\rightarrow b,\, b\rightarrow a\in F\}.\]
The mapprings   $\theta\mapsto F_\theta$ and $F\mapsto \theta_F$ are mutually inverse isomorphisms between $\mathrm{Con}(\mathbf{A})$ and  $\mathcal{F}(\mathbf{A})$.

For a logic $L\in\mathcal{E} J$ and for a variety $\mathcal{V}\in\mathrm{Sub}(\mathcal{V}_j)$, we put
\[ V(L)  :=  \{  \mathbf{A} | \; \mathbf{A}\in\mathcal{V}_j\ \text{and}\ \mathbf{A} \vDash L \};\ \  L\mathcal{V}:=\{ \varphi \mid \mathcal{V}\models \varphi\}. \] 
For an arbitrary class of $j$-algebras $\mathcal{K}$,  we also put $L\mathcal{K}=\{ \varphi \mid \mathcal{K}\models\varphi\}$. If a logic $L\in\mathcal{E}J$ is such that $L=L\mathcal{K}$ we say that $L$ is {\em complete w.r.t.} $\mathcal{K}$. For a $j$-algebra $\mathbf{A}$, we write $L\mathbf{A}$ instead of $L\{\mathbf{A}\}$ and call $L\mathbf{A}$ the {\em logic of} $\mathbf{A}$.

Since the fact that a formula $\varphi$ is true on a $j$-algebra $\mathbf{A}$ is equivalent to the validity of the identity $\varphi=p\rightarrow p$ on $\mathbf{A}$, we have $V(L)\in\mathrm{Sub}(\mathcal{V}_j)$ for every $L\in\mathcal{E} J$. It is known also that $L\mathcal{V}\in\mathcal{E} J$ for every $\mathcal{V}\in\mathrm{Sub}(\mathcal{V}_j)$. Moreover, the following statement holds, see, e.g. \cite{ConstrNeg}. 

\begin{theorem}
	The mappings $L\mapsto V(L)$ and $\mathcal{V}\mapsto L\mathcal{V}$ are mutually inverse dual isomorphisms \footnote{By a dual isomorphism between lattices $\mathbf{A}$ and $\mathbf{B}$ we mean an isomorphism between $\mathbf{A}$ and $\mathbf{B}^{op}$, where $\mathbf{B}^{op}$ is the lattice with the same universe as $\mathbf{B}$ and reversed order.} between lattices $\mathcal{E} J$ and $\mathrm{Sub}(\mathcal{V}_j)$. In particular, for every $L_0\in\mathcal{E} J$ and  $\mathcal{V}_0\in\mathcal{V}_j$ we have		
	\[ L(V(L_0)) = L_0\ \ \text{and}\ \ V(L(\mathcal{V}_0)) = \mathcal{V}_0.\] 
\end{theorem}

This statement implies, in particular, that $\varphi\in J$ iff $\varphi$ is true on every  $j$-algebra. Since $\bot\rightarrow p$ is true on $\mathbf{A}$ iff $\bot$ is the least element of $\mathbf{A}$ w.r.t. $\leq_{\bf A}$ we obtain that $V(Int)=\mathcal{V}_H$ and $L(\mathcal{V}_H)=Int$. Naturally, the restriction of $L\mapsto V(L)$ to $\mathcal{E} Int$ is a dual isomorphism between $\mathcal{E} Int$ and $\mathrm{Sub}(\mathcal{V}_H)$.  Similarly, the restriction of $L\mapsto V(L)$ to $\mathcal{E} L_0$ for every $L_0\in \mathcal{E} J$ is a dual isomorphism between $\mathcal{E} L_0$ and $\mathrm{Sub}( V(L_0))$.

Let us recall an important fact from universal algebra. Every variety $\mathcal{V}$ of algebras is generated by the family $\mathcal{V}_\mathsf{fsi}$ of its finitely generated subdirectly irreducible algebras ($\mathsf{fsi}$-algebras). For a definition of subdirectly irreducible algebra the reader may consult \cite{BurrSanka}. For our goals it will be enough to give a characterization of subdirectly irreducible $j$-algebras.

An element $*_\mathbf{A}$ of a $j$-algebra $\mathbf{A}$ is called an {\em opremum} of $\mathbf{A}$ if $*_\mathbf{A}\neq 1_\mathbf{A}$ and $b\leq *_\mathbf{A}$ for every $b\in\mathbf{A}$ different from $1_\mathbf{A}$.


\begin{theorem} (see, e.g. \cite{Rautenberg1979}) A $j$-algebra $\mathbf{A}$ is subdirectly irreducible if and only if there is an opremum $*_\mathbf{A}$ in $\mathbf{A}$.
\end{theorem}

We define the preorder on $(\mathcal{V}_j)_\mathsf{fsi}$ as follows: $\mathbf{A}\sqsubseteq\mathbf{B}$ iff $L\mathbf{A}\subseteq L\mathbf{B}$ for $\mathbf{A},\mathbf{B}\in(\mathcal{V}_j)_\mathsf{fsi}$.
The well known Jonsson Theorem (see \cite{BurrSanka}) provides a useful characterization of this preorder. This theorem says that in a congruence distributive variety, all subdirectly irreducible elements of the subvariety generated by the class $\mathcal{K}$ of algebras belong to $\mathsf{HSUp}(\mathcal{K})$.\footnote{For a class of algebras $\mathcal{K}$, the class of all homomorphic images of algebras from $\mathcal{K}$ is denoted as $\mathsf{H}(\mathcal{K})$, the class of all subalgebras of algebras from $\mathcal{K}$ as $\mathsf{S}(\mathcal{K})$, finally, the class of all ultraproducts of algebras from $\mathcal{K}$ is denoted as $\mathsf{Up}(\mathcal{K})$.} If an algebra $\mathbf{A}$ is finite, then $\mathsf{HSUp}(\{\mathbf{A}\})=\mathsf{HS}(\{\mathbf{A}\})$. The variety of $j$-algebras is congruence distributive, therefore, for any finite  $\mathbf{A}$, $\mathbf{B}\in (\mathcal{V}_j)_\mathsf{fsi}$ we have
$$\mathbf{A}\sqsubseteq\mathbf{B}\ \Leftrightarrow\ L\mathbf{A}\subseteq L\mathbf{B}\ \Leftrightarrow\ \mathbf{B}\in\mathsf{HS}(\{\mathbf{A}\}).$$

\section{Isomorphism types of algebras from $(V(JC))_\mathsf{fsi}$}

As it follows from Theorem~1 the lattice $\mathcal{E} JC$ is dually isomorphic to the lattice $\mathrm{Sub}(V(JC))$. So it would be enough  to decribe the lattice of subvarieties of the variety $V(JC)$ consisting of all $JC$-models.

First we describe $\mathsf{fsi}$-algebras from the variety $V(JC)$. The next statement is an immediate generalization of the characterization of $\mathsf{fsi}$-algebras from $V(LC)$ obtained in \cite{DunnMeyer1971}.

\begin{proposition}\label{fsiJC} Let $\mathbf{A}$ be a $j$-algebra. Then $\mathbf{A}\in(V(JC))_{\mathsf{fsi}}$ if and only if $\mathbf{A}$ is finite and linearly ordered.
\end{proposition}

\begin{proof} First we assume that $\mathbf{A}$ is finite and linearly ordered $j$-algebra. Since $\mathbf{A}$ is finite it is finitely generated. Finiteness of $\mathbf{A}$ implies that every non-unit element lies under some maximal non-unit element. The linearity of $\mathbf{A}$ implies that there is only one maximal non-unit element, which is an opremum of $\mathbf{A}$. Thus, $\mathbf{A}$ is an $\mathsf{fsi}$-algebra. It follows immediately from (\ref{imp_unit}) that $(p\rightarrow q)\vee(q\rightarrow p)$ is true on a linearly ordered $j$-algebra. Consequently, $\mathbf{A}\in (V(JC))_\mathsf{fsi}$.
	
	Now we assume that $\mathbf{A}\in(V(JC))_{\mathsf{fsi}}$. If $a\not\leq_\mathbf{A} b$ and $b\not\leq_\mathbf{A} a$ for some $a,b\in\mathbf{A}$, then  we have $(a\rightarrow b)\vee(b\rightarrow a)\leq *_\mathbf{A}$ by (\ref{imp_unit}), which conflicts with $\mathbf{A}\models (p\rightarrow q)\vee(q\rightarrow p)$. Thus, $\mathbf{A}$ is linearly ordered.
	
	Let $X$ be a finite set generating $\mathbf{A}$. We just proved that $\mathbf{A}$ is linearly ordered. Consequently, $a\vee b$, $a\wedge b\in \{ a,b\}$ for $a,b\in\mathbf{A}$. Further, notice that 
	$a\rightarrow b\in \{ 1_\mathbf{A}, b \}$. If $a\leq_\mathbf{A} b$, then $a\rightarrow b=1_\mathbf{A}$ by (\ref{imp_unit}). If $b\lvertneqq_\mathbf{A} a$, then  $a\rightarrow b=b$. Indeed, $a\wedge b=b$ and $a\wedge c\gvertneqq b$ for $c\gvertneqq b$. Thus, except for generators $\mathbf{A}$ may contain only $\bot$ and $1_\mathbf{A}$. Consequently, $\mathbf{A}$ is finite.
	
\end{proof}

In the last proof we established the following.

\begin{corollary}\label{cor1} Let $\mathbf{A}$ be a linearly ordered $j$-algebra. The implication act on $\mathbf{A}$ as follows:
	\begin{equation}
		a\rightarrow b=
		\begin{cases}
			1_\mathbf{A}, & a\leq_\mathbf{A} b;\\
			b, & \text{otherwise}.
		\end{cases}
		\label{2}
	\end{equation}
	
	Moreover, if $\{\bot_\mathbf{A},1_\mathbf{A}\}\subseteq X\subseteq |\mathbf{A}|$, then $X$ is the universe of a subalgebra of $\mathbf{A}$.
\end{corollary}

From Proposition~\ref{fsiJC} we conclude that up to isomorphism every element of $(V(JC))_{\mathsf{fsi}}$ is determined by the number of its elements and by the interpretation of $\bot$ in this finite linear order. Thus, we may code isomorphism types of algebras from $(V(JC))_{\mathsf{fsi}}$ by pairs of positive natural numbers. We say that $\mathbf{A}\in (V(JC))_{\mathsf{fsi}}$ is of type $(m, n)$, and write $\mathsf{tp}(\mathbf{A})=(m,n)$,  if $m$ is the number of elements greater or equal to $\bot$, and $n$ is the number of elements of $\mathbf{A}$, which are smaller or equal to $\bot$. 

Now we are ready to describe the preordering $\sqsubseteq$ on $(V(JC))_{\mathsf{fsi}}$. Recall that $\mathbf{A}\sqsubseteq\mathbf{B}$ iff $L\mathbf{A}\subseteq L\mathbf{B}$ iff $\mathbf{B}\in\mathsf{HS}(\{\mathbf{A}\})$ for $\mathsf{fsi}$-algebras $\mathbf{A}$ and $\mathbf{B}$.

\begin{proposition} Let $\mathbf{A},\mathbf{B}\in (V(JC))_{\mathsf{fsi}}$, $\mathsf{tp}(\mathbf{A})=(m,n)$, and $\mathsf{tp}(\mathbf{B})=(k,l)$. The following equivalence holds:
	\[ \mathbf{A}\sqsubseteq\mathbf{B} \ \ \Leftrightarrow\ \ k\leq m\ \text{and}\ l\leq n.\]
\end{proposition}

\begin{proof} If $\mathbf{B}\in\mathsf{HS}(\{\mathbf{A}\})$, then obviously $k\leq m$ and $l\leq n$.
	
	Assume that $k\leq m$ and $l\leq n$ and prove the inverse implication. Assume additionally that $1_\mathbf{A}\neq \bot_\mathbf{A}$  and $1_\mathbf{B}\neq \bot_\mathbf{B}$. By Corollary~\ref{cor1} arbitrary subset $X$ of $|\mathbf{A}|$ containing $1_\mathbf{A}$ and $\bot_\mathbf{A}$ is the universe of a subalgebra of $\mathbf{A}$. This immediately implies that $\mathbf{A}$ has a subalgebra isomorphic to $\mathbf{B}$, i.e., $\mathbf{B}\in\mathsf{S}(\{\mathbf{A}\})$. The same holds if $1_\mathbf{A}= \bot_\mathbf{A}$  and $1_\mathbf{B}= \bot_\mathbf{B}$. 
	
	It remains to consider the case $1_\mathbf{A}\neq \bot_\mathbf{A}$  and $1_\mathbf{B}= \bot_\mathbf{B}$, when $\mathbf{B}\not\in\mathsf{S}(\{\mathbf{A}\})$. Put $F=\{ a \mid \bot_\mathbf{A}\leq_\mathbf{A} a\}$ and $\mathbf{A}':=\mathbf{A}/F$. It follows easily from (\ref{2}) that $[a]_F=F$ for $a\in F$ and $[a]_F=\{ a\}$ for $a\not\in F$. Thus, $\mathsf{tp}(\mathbf{A}')=(1,n)$ and by the above argument $\mathbf{B}\in \mathsf{S}(\mathbf{A}')$. From $\mathbf{A}'\in\mathsf{H}(\mathbf A)$ we conclude $\mathbf{A}\sqsubseteq\mathbf{B}$.
	
\end{proof}

Put $\mathbb{N}^+ = \{  1, 2, 3, ...  \}$ and $\mathcal{P}=\langle(\mathbb{N}^+)^2, \preceq \rangle$, where $(m, n) \preceq (k, l)$ iff $k \leq m $ and $ l \leq n$. It is clear that $\preceq$ is a partial order on the set of pairs of positive natural numbers. The stucture of this ordering is presented on the following diagramm.

\vspace{3mm}
\begin{center}
	\parbox{60mm}{
		\begin{picture}(140,100)(0,0)
			
			\put(0,0){\circle*{2}} \put(40,0){\circle*{2}} \put(80,0){\circle*{2}} \put(120,0){\circle*{2}} 
			\put(160,0){\circle*{2}} \put(20,20){\circle*{2}} \put(60,20){\circle*{2}} \put(100,20){\circle*{2}} \put(140,20){\circle*{2}} \put(40,40){\circle*{2}} \put(80,40){\circle*{2}} \put(120,40){\circle*{2}} \put(60,60){\circle*{2}} \put(100,60){\circle*{2}} \put(80,80){\circle*{2}} 
			
			\put(-20,-20){\circle*{1}} \put(-15,-15){\circle*{1}} \put(-10,-10){\circle*{1}}
			\put(20,-20){\circle*{1}} \put(25,-15){\circle*{1}} \put(30,-10){\circle*{1}}  
			\put(60,-20){\circle*{1}} \put(65,-15){\circle*{1}} \put(70,-10){\circle*{1}} 
			\put(100,-20){\circle*{1}} \put(105,-15){\circle*{1}} \put(110,-10){\circle*{1}}
			\put(180,-20){\circle*{1}} \put(175,-15){\circle*{1}} \put(170,-10){\circle*{1}}  
			
			\put(0,0){\line(1,1){80}} \put(40,0){\line(1,1){60}} \put(80,0){\line(1,1){40}} \put(120,0){\line(1,1){20}}
			\put(40,0){\line(-1,1){20}} \put(80,0){\line(-1,1){40}} \put(120,0){\line(-1,1){60}}	\put(160,0){\line(-1,1){80}}
			
			\put(81,81){$(1,1)$} \put(121,41){$(1,3)$} \put(161,1){$(1,5)$}
			\put(15,41){$(3,1)$} \put(-25,1){$(5,1)$}	
			
			
			
		\end{picture}
	}
\end{center}

\vspace{10mm}
\begin{center} Figure 3.
\end{center}

\bigskip
Recall that a subset $X\subseteq (\mathbb{N}^+)^2$ is a {\em cone} ({\em upward closed set}) w.r.t. $\preceq$ if for every $a\in X$ and $b\in (\mathbb{N}^+)^2$ such that $a\preceq b$ we have $b\in X$. The set of all cones w.r.t. $\preceq$ form a lattice with the inclusion relation as its lattice order. We denote this lattice $\mathrm{Up}(\mathcal{P})$.

For $L\in\mathcal{E} JC$ put $\mathsf{tp}(L):=\{ \mathsf{tp}(\mathbf{A}) \mid \mathbf{A}\in (V(L))_\mathsf{fsi}\}$.  From the just obtained characterization of $\sqsubseteq$ we infer the next fact.

\begin{corollary} For every $L\in\mathcal{E} JC$ we have $\mathsf{tp}(L)\in\mathrm{Up}(\mathcal{P})$. Moreover, the mapping $\mathsf{tp}:\mathcal{E} JC\rightarrow\mathrm{Up}(\mathcal{P})$ is one-to-one and order reversing.
\end{corollary}

\begin{proof}
	From Proposition~2 we obtain $\mathsf{tp}(L)\in\mathrm{Up}(\mathcal{P})$ for $L\in\mathcal{E} JC$. According to Theorem~1 the mapping $L\mapsto V(L)$ is order reversing, consequently, $\mathsf{tp}$ is order reversing too. Finally, if $L_1\neq L_2$, then $(V(L_1))_\mathsf{fsi}\neq (V(L_2))_\mathsf{fsi}$. This fact implies that $\mathsf{tp}$ is one-to-one.  
\end{proof}


In other words, for every $JC$-extension $L$ the set of types of $\mathsf{fsi}$-algebras modelling $L$ form a cone w.r.t. $\preceq$. In what follows we prove that every cone from $\mathrm{Up}(\mathcal{P})$ can be realized as $\mathsf{tp}(L)$ for some $JC$-extension $L$. But first we obtain  more explicit decription of cones from  $\mathrm{Up}(\mathcal{P})$.

For $(m,n)\in(\mathbb{N}^+)^2$ we denote by $(m,n)\uparrow$ the principal cone generated by $(m,n)$, i.e.,
\[ (m,n)\uparrow:=\{ (k,l)\mid (m,n)\preceq (k,l)\}=\{ (k,l)\mid k\leq m,\ l\leq n\}.\]
Every principal cone $(m,n)\uparrow$ is finite as it follows from its definition. For a proper cone $X\in\mathrm{Up}(\mathcal{P})$, i.e., such cone that $\varnothing\neq X\neq(\mathbb{N}^+)^2$, we define two natural numbers $r(X)$ and $l(X)$ as follows: $r(X)$ is the greatest natural number such that $(m,r(X))\in X$ for all $m\in\mathbb{N}^+$, and there is $n\in\mathbb{N}^+$ such that $(n,r(X)+1)\not\in X$. The number $l(X)$ is defined is a dual way, this is the greatest natural number such that $(l(X),m)\in X$ for all $m\in\mathbb{N}^+$, and there is $n\in\mathbb{N}^+$ such that $(l(X)+1,n)\not\in X$.

It can be easily seen that natural numbers $l(X)$ and $r(X)$ are well defined for every proper cone $X$. Moreover, $r(X)=0$ iff $(m,1)\not\in X$ for some $m$, and $l(X)=0$ iff $(1,n)\not\in X$ for some $n$.

Now we associate with every proper cone $X\in\mathrm{Up}(\mathcal{P})$ two subcones $W^r(X)$ and $W^l(X)$:
\[ W^r(X):=\{ (m,n) \mid n\leq r(X)\}\ \ \text{and}\ \ W^l(X):=\{ (m,n) \mid m\leq l(X)\}.\]
Obviously, $W^r(X)=\varnothing$ iff $r(X)=0$, and $W^l(X)=\varnothing$ iff $l(X)=0$. Moreover, if one of these subcones is not empty, then it is infinite.

Now we are ready to describe cones from $\mathrm{Up}(\mathcal{P})$.

\begin{proposition} Every proper cone $X\in\mathrm{Up}(\mathcal{P})$ is the union of cones $W^r(X)$, $W^l(X)$, and of finite number of principal cones.
\end{proposition}

\begin{proof} By definition of $r(X)$ and $l(X)$ there are $m$ and $n$ such that $$\{ (m,r(X)+1),(l(X)+1,n)\}\cap X=\varnothing.$$  Notice that in this case
	\[X\setminus(W^l(X)\cup W^r(X))\subseteq (m,n)\uparrow.\]
	Indeed, assume that $(s,t)$ is such that $l(X)+1\leq s$, $r(X)+1\leq t$, and $(s,t)\not\in (m,n)\uparrow$. In this case either $m<s$, or $n<t$. If $m<s$, then $(s,t)\preceq (m,r(X)+1)$, and so $(s,t)\not\in X$. If $n<t$, then again $(s,t)\not\in X$ in view of  $(s,t)\preceq (l(X)+1,n)$.
	
	Let $(u_1,v_1),\ldots (u_n,v_n)$ be all elements of $X\cap (m,n)\uparrow$ minimal w.r.t. $\preceq$. Then
	\[X=W^l(X)\cup W^r(X)\cup(u_1,v_1)\uparrow\cup\ldots\cup (u_n,v_n)\uparrow.\]	\end{proof}


\section{The dual isomorphism of lattices $\mathcal{E}JC$ and $\mathrm{Up}(\mathcal{P})$}

We just noticed that the mapping $\mathsf{tp}$ assigning to a $JC$-extension $L$ the cone of isomorphism  types of algebras from $(V(L))_\mathsf{fsi}$ is one-to-one and order reversing. Now we prove that $\mathsf{tp}$ is a dual lattice isomorphism between $\mathcal{E}JC$ and $\mathrm{Up}(\mathcal{P})$. To this end given a cone $X\in\mathrm{Up}(\mathcal{P})$ we provide an axiomatization for a logic $L\in\mathcal{E}JC$ such that $\mathsf{tp}(L)=X$.

For $n\in\mathbb{N^+}$, we define the following formula with propositional variables from the list $p_1,\ldots,p_n$: 
$$ {\bf \tau}_n := p_1 \vee (p_1 \rightarrow p_2) \vee \cdots \vee ( p_{n-1} \rightarrow p_n).$$

\begin{lemma} Let ${\bf A}$ be a finite linearly ordered $j$-algebra. Then the following equivalence holds:  
	$$ {\bf A}  \models {\bf \tau}_n   \; \Leftrightarrow \;  |A| \leq n . $$
\end{lemma}

\begin{proof} Let $v$ be an arbitrary $\mathbf{A}$-valuation. It follows easily from (\ref{2}) that $\mathbf{A},v\not\models\tau_n$ iff  $$1_{\bf A} \gneqq v(p_1) \gneqq v(p_2) \gneqq \cdots \gneqq v(p_n).$$ Thus, $\mathbf{A}\not\models\tau_n$ iff $A$ contains at least $n+1$ different elements.
\end{proof}

Let $\mathbf{A}$ be a $j$-algebra. Put 
$$A^{\bot} := \{ b \in A \mid b \geq_\mathbf{A} \bot_\mathbf{A} \; \}\ \ \text{and}\ \ A_{\bot} := \{ b \in A \mid b \leq_\mathbf{A} \bot_\mathbf{A} \; \}.$$ 
For $a, b \in A_{\bot}$, we put $a \rightarrow_{\bot} b = (a \rightarrow b) \wedge \bot_\mathbf{A}$.

It is obvious that the set $A^\bot$ is closed under the operations of $\mathbf{A}$ and that $\mathbf{A}^{\bot} = \langle A^{\bot}, \wedge, \vee, \rightarrow, \bot \rangle$ is a Heyting algebra. The set $A_\bot$ is closed under $\vee$, $\wedge$, $\rightarrow_\bot$, and $ \mathbf{A}_{\bot} = \langle A_{\bot}, \wedge, \vee, \rightarrow_{\bot}, \bot \rangle$ is a negative algebra.

Moreover, it is known \cite[Prop.~4.2.3]{ConstrNeg} that for every formula $\phi(p_1, \cdots , p_n)$ the following holds:
$$ \mathbf{A} \models \phi(p_1 \vee \bot, \cdots , p_n \vee \bot) \; \Leftrightarrow \; \mathbf{A}^{\bot} \models \phi(p_1, \cdots , p_n); $$
$$ \mathbf{A} \models \bot \rightarrow \phi(p_1, \cdots , p_n) \; \Leftrightarrow \; \mathbf{A}_{\bot} \models \phi(p_1, \cdots , p_n). $$
We will use these equivalences and Lemma~1 to establish the following facts.

\begin{proposition} Let $m,n\in\mathbb{N}^+$, $\mathbf{A}\in (V(JC))_\mathsf{fsi}$, and $X\in\mathrm{Up}(\mathcal{P})$. Then the following equivalences hold:
	\begin{enumerate}
		\item $\mathsf{tp}(\mathbf{A})\in (m,n)\uparrow$ iff $\mathbf{A}\models \tau_m(p_1\vee\bot,\ldots,p_m\vee\bot)$ and $\mathbf{A}\models \bot\rightarrow\tau_n$;
		
		\item $\mathsf{tp}(\mathbf{A})\in W^r(X)$ iff $\mathbf{A}\models \bot\rightarrow\tau_{r(X)}$;
		
		\item $\mathsf{tp}(\mathbf{A})\in W^l(X)$ iff $\mathbf{A}\models \tau_{l(X)}(p_1\vee\bot,\ldots,p_{l(X)}\vee\bot)$.
	\end{enumerate}
\end{proposition} 

\begin{proof} To prove Item~1  recall that $\mathsf{tp}(\mathbf{A})\in (m,n)\uparrow$ means exactly that $|A^\bot|\leq m$ and $|A_\bot|\leq n$. The latter is equivalent by Lemma~1 to $\mathbf{A}^\bot\models \tau_m$ and $\mathbf{A}_\bot\models \tau_n$, i.e., $\mathbf{A}\models \tau_m(p_1\vee\bot,\ldots,p_m\vee\bot)$ and $\mathbf{A}\models \bot\rightarrow\tau_n$.
	
	Items~2 and ~3 follow in a similar way from the observations that $\mathsf{tp}(\mathbf{A})\in W^r(X)$ iff $|A_\bot|\leq r(X)$, and that $\mathsf{tp}(\mathbf{A})\in W^l(X)$ iff $|A^\bot|\leq l(X)$.
	
\end{proof}

\begin{theorem} The mapping $\mathsf{tp}:\mathcal{E} JC\rightarrow\mathrm{Up}(\mathcal{P})$ is a dual lattice isomorphism between $\mathcal{E}JC$ and $\mathrm{Up}(\mathcal{P})$.
\end{theorem}

\begin{proof} Since an order isomorphism of two lattices is also a lattice isomorphism and we know that  $\mathsf{tp}:\mathcal{E} JC\rightarrow\mathrm{Up}(\mathcal{P})$ is a one-to-one and order reversing mapping, it will be enough to prove that $\mathsf{tp}$ maps $\mathcal{E} JC$ onto $\mathrm{Up}(\mathcal{P})$.
	
	Take an arbitrary cone $X\in \mathrm{Up}(\mathcal{P})$.  According to Proposition~3 it can be represented as 
	\[X=W^l(X)\cup W^r(X)\cup(u_1,v_1)\uparrow\cup\ldots\cup (u_n,v_n)\uparrow,\]
	for some $u_1,v_1,\ldots,u_n,v_n\in\mathbb{N}^+$.
	Put 
	\[ L^{l(X)}= JC+\{\tau_{l(X)}(p_1\vee\bot,\ldots,p_{l(X)}\vee\bot)\}, \ \ L^{r(X)}=JC+\{ \bot\rightarrow\tau_{r(X)}\},\]	
	\[ L^{u_i,v_i}= JC+\{ \tau_{u_i}(p_1\vee\bot,\ldots,p_{u_i}\vee\bot), \bot\rightarrow\tau_{v_i}\},\ i=1,\ldots,n.\]
	Proposition~4 implies that
	\[ \mathsf{tp}(L^{l(X)})=W^l(X), \ \mathsf{tp}(L^{r(X)})=W^r(X), \ \mathsf{tp}(L^{u_i,v_i})=(u_i,v_i)\uparrow,\  i=1,\ldots,n.\]
	
	Since $L\mapsto V(L)$, $L\in \mathcal{E}JC$, is a dual lattice isomorphism, we have $V(L_1\cap L_2)=V(L_1)+V(L_2)$ and \[ (V(L_1))_\mathsf{fsi}\cup(V(L_2))_\mathsf{fsi}\subseteq (V(L_1\cap L_2))_\mathsf{fsi}.\]
	To prove  the inverse inclusion, and so the equality 
	\begin{equation}
	(V(L_1\cap L_2))_\mathsf{fsi}=(V(L_1))_\mathsf{fsi}\cup(V(L_2))_\mathsf{fsi} 
	\label{three}
	\end{equation} for logics finitely axiomatizable modulo $JC$ we need the following results.
		
	S.~Miura \cite{Miura1966} noticed that an intersection of two superintuitionistic logics can be axiomatized by repeatedless disjunctions of theirs axioms. This result can be easily generalized to extensions of minimal logic \cite[Prop.~2.1.5]{ConstrNeg}. More exactly, a {\em repeatedless disjunction} of formulas $\varphi(p_1,\ldots,p_n)$ and $\psi(p_1,\ldots,p_m)$ is a formula $\varphi\underline{\vee}\psi:=\varphi(p_1,\ldots,p_n)\vee\psi(p_{n+1},\ldots,p_{n+m})$. Further, if $L\in\mathcal{E}J$, $L_1=L+\{\varphi_i\mid i\in I_1\}$, and $L_2=L+\{\psi_j\mid j\in I_2\}$, then
	\[ L_1\cap L_2=L+\{ \varphi_i\underline{\vee}\psi_j \mid i\in I_1, j\in I_2\}.\]
	
	In particular, if $L_1=JC+\{ \varphi(p_1,\ldots,p_n)\}$ and $L_2=JC+\{ \psi(p_1,\ldots,p_m)\}$, then 
	$L_1\cap L_2=JC+\{ \varphi\underline{\vee}\psi\}$. Take a linerly ordered $\mathsf{fsi}$-algebra $\mathbf{A}$ such that $\mathbf{A}\not\in (V(L_1))_\mathsf{fsi}\cup(V(L_2))_\mathsf{fsi}$, i.e. 
	\[ v_1(\varphi(p_1,\ldots,p_n))\leq *_\mathbf{A}\ \text{and}\  v_2(\psi(p_1,\ldots,p_m))\leq *_\mathbf{A}\] for some $\mathbf{A}$-valuations $v_1$ and $v_2$. Let $v(p_i)=v_1(p_i)$ for $i=1,\ldots,n$ and $v(p_{n+i})=v_2(p_i)$ for $i=1,\ldots,m$. Then we have $v(\varphi\underline{\vee}\psi)\leq *_\mathbf{A}$, and so $\mathbf{A}\not\in (V(L_1\cap L_2))_\mathsf{fsi}$. We have thus proved (\ref{three}) for finitely axiomatizable $JC$-extensions.
	 
	 The just obtained result implies that for an arbitrary cone $X\in \mathrm{Up}(\mathcal{P})$ we have $\mathsf{tp}(L)=X$, where
	\begin{equation}
		L= L^{l(X)}\cap L^{r(X)} \cap L^{u_1,v_1}\cap\ldots\cap L^{u_n,v_n}.
		\label{four}
	\end{equation}
	
\end{proof}


\begin{proposition} Every logic from $\mathcal{E} JC$ is finitely axiomatizable, has the finite model property, and is decidable.
\end{proposition}

\begin{proof} Every logic $L\in\mathcal{E} JC$ is finitely axiomatizable modulo $JC$ according to (\ref{four}). 	
	
	Every $L\in\mathcal{E} JC$ has the finite model property due to the fact that $L$ is complete w.r.t. the family of its $\mathsf{fsi}$-models, which are all finite according to Proposition~1.
	
	Finally, for every $L\in\mathcal{E} JC$ its set of $\mathsf{fsi}$-models is decidable. Indeed, we noticed that up to isomorphism $\mathsf{fsi}$-models of $JC$ can be coded by pairs of natural numbers. According to Corollary~2 and Proposition~3 for every $L\in\mathcal{E} JC$, the family $(V(L))_\mathsf{fsi}$ is coded by a finite union of sets having one of the following forms
	\[ \{ (k,l) \mid k\leq n\}, \ \  \{ (k,l) \mid l\leq m\},\ \  \{ (k,l) \mid k\leq r,\ l\leq s\}.\]
	Thus, every $L\in\mathcal{E} JC$ is complete w.r.t. to a decidable set of finite algebras. Consequently, $L$ is decidable according to the well known Harrop Theorem saying that a logic with enumerable set of theorems, which is complete w.r.t. to an enumerable set of finite models, is decidable.
	
\end{proof}

Finally, we describe pretabular $JC$-extensions. Recall that a logic $L\in\mathcal{E} J$ is {\em tabular} if $L=L\mathbf{A}$ for some finite $j$-algebra $\mathbf{A}$. We call  a logic $L\in\mathcal{E} J$  {\em pretabular} if $L$ is not tabular, but every its proper extension is. 

\begin{proposition} The lattice $\mathcal{E} JC$ contains exactly two pretabular logics: the Dummett logic $LC$ and $NegC=JC+\{\bot\}$. 
\end{proposition}

\begin{proof} If $L=L\mathbf{A}$, then $V(L)=V(\{\mathbf{A}\})$. If additionally we assume that $\mathbf{A}$ is finite, then $(V(L))_\mathsf{fsi}\subseteq \mathsf{HS}(\{\mathbf{A}\})$ by Jonsson's lemma. The finiteness of $\mathbf{A}$ implies that $(V(L))_\mathsf{fsi}$ is finite up to isomorphism. Thus, tabular logics from $\mathcal{E} JC$ are such logics $L$ that the cone $\mathsf{tp}(L)$ is finite. Respectively, pretabular logics from $\mathcal{E} JC$ are such logics $L$ that the cone $\mathsf{tp}(L)$ is infinite, but every proper subcone of $\mathsf{tp}(L)$ is finite. It is enough to have a look at Figure~3 to understand that there are only two such cones in $\mathrm{Up}(\mathcal{P})$:
	\[ C_1=\{ (n,1) \mid n\in\mathbb{N}^+\}\ \ \text{and}\ \ C_2=\{ (1,n) \mid n\in\mathbb{N}^+\}. \]
	The cone $C_1$ contains exactly  isomorphism types of algebras that have no elements lying strictly under $\bot$, i.e. $\mathsf{tp}(\mathbf{A})\in C_1$ if and only if $\mathbf{A}$ is a finite linear Heyting algebra. Thus, $\mathsf{tp}(LC)=C_1$. On the other hand, $\mathsf{tp}(\mathbf{A})\in C_2$ iff $\bot$ is the greatest element of $\mathbf{A}$. Clearly, such algebras are distinguished in $(V(JC))_\mathsf{fsi}$ with the help of formula $\bot$, and we have $\mathsf{tp}(NegC)=C_2$.
	
\end{proof}




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

	\bibitem{BurrSanka} S.~Burris, H.P.~Sankappanavar, \href{https://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html}{\it A course in universal algebra}, Graduate Texts in Math., \textbf{78}, New York, Springer, 1981.

\bibitem{Dummett1959} M. Dummett, \href{https://doi.org/10.2307/2964753}{\it A propositional calculus with a denumerable matrix}, The Journal of Symbolic Logic, \textbf{24} (1959), 97--106.

\bibitem{Dunn1970} J.M. Dunn,  \href{https://doi.org/10.2307/2271149}{\it Algebraic completeness results for R-Mingle and its extensions}, The Journal of Symbolic Logic, \textbf{35} (1970), 1--13.

\bibitem{DunnMeyer1971} J.M. Dunn, R.K. Meyer,  \href{https://doi.org/10.1002/malq.19710170126}{\it Algebraic completeness results for Dummett's LC and its extensions}, Zeitschrift f\"{u}r Mathematische Logik und Grundlagen der Mathematik, \textbf{17}:2 (1971), 225--230.

\bibitem{ALSMeeting1970} J.K. Feibleman, R.M. Smullyan, R.L. Vaught, \href{https://doi.org/10.2307/2270571}{\it Meeting of the Association for Symbolic Logic}, The Journal of Symbolic Logic, \textbf{35}:2 (1970), 352--363. `

\bibitem{Godel1932} K. G\"{o}del, \href{https://doi.org/10.1093/oso/9780195147209.003.0026
}{\it Zum intuitionistischen Aussagenkalk\"{u}l}, S.~Feferman et al. (eds.) Kurt  G\"{o}del Collected Works, Vol.I: Publications 1929--1936, Oxford, Oxford University Press, 2001.

\bibitem{Johansson1937} I. Johansson, \href{http://www.numdam.org/item/CM_1937__4__119_0/}{\it Der Minimalkalk\"{u}l, ein reduzierter intuitionistischer
Formalismus}, Compositio Mathematika, \textbf{4} (1937), 119--136.

\bibitem{Kracht1998} M. Kracht, \href{https://doi.org/10.1023/A:1004222213212}{\it On extensions of intermediate logics by strong negation}.
Journal of Philosophical Logic, \textbf{27}:1 (1998), 49--73.

\bibitem{Maksimova1972} L.L. Maksimova, \href{https://doi.org/10.1007/BF02330744}{\it Pretabular superintuitionistic logics}, Algebra and Logic, \textbf{11}:5 (1972), 558--570.

\bibitem{Miura1966} S. Miura, \href{https://doi.org/10.1017/S0027763000011715}{\it A remark on the intersection of two logics}, Nagoja Mathematical Journal, \textbf{26} (1966), 167--171.

\bibitem{Odintsov2006} S.P. Odintsov, \href{https://doi.org/10.3103/S1055134407020034}{\it The lattice of extensions of minimal logic}, Siberian Advances in Mathematics, \textbf{9} (2006), 60--108.

\bibitem{Odintsov2007} S.P. Odintsov, \href{https://doi.org/10.1007/s11202-007-0012-6}{\it On Extensions of Nelson's Logic Satisfying Dummett's Axiom}, Siberian Mathematical Journal, \textbf{48}:1 (2007), 112--125.

\bibitem{ConstrNeg} S. Odintsov, \href{https://doi.org/10.1007/978-1-4020-6867-6}{\it Constructive negations and paraconsistency}, Dordrecht, Springer, 2008.

\bibitem{Rasiowa1974} H. Rasiowa, \href{https://philpapers.org/rec/RASAAA-2}{\it An algebraic approach to non-classical logics}, PWN, Warszawa, 1974, 53--55.

\bibitem{Rautenberg1979} W. Rautenberg,  \href{https://www.amazon.de/Logik-Grundlagen-Mathematik-Band-nichtklassische/dp/3528083859}{\it Klassische und nichtclassische Aussagenlogik}, Braunschweig, Vieweg, 1979.

\bibitem{Scroggs1951} S.J. Scroggs, \href{https://doi.org/10.2307/2266683}{\it Extensions of the Lewis system S5}, The Journal of Symbolic Logic, \textbf{16} (1951), 112--120.

\bibitem{Skolem1913} T. Skolem, {\em Om konstitutionen av den identiske kalkuls grupper}, Proceedings of the 3rd Scandinavian Mathematical Congress, Kristiania, 1913, 149--163. English translation in \cite{SkFenstad1970}.

\bibitem{SkFenstad1970} T. Skolem, \href{https://archive.org/details/selectedworksinl0000thsk}{\it Selected Works in Logic}, ed. by J.~E.~Fenstad. Universitetsforlaget, Oslo, 1970.

\bibitem{Ulrich1970} D. Ulrich, {\it Decidability results for some classes of propositional calculi}, The Journal of Symbolic Logic, \textbf{35} (1970), ~353--354, as a part of \cite{ALSMeeting1970}. 

\bibitem{Plato2003} J. von Plato,  \href{https://doi.org/10.1023/A:1022997524909}{\it Skolem's Discovery of G\"{o}del-Dummett Logic}, Studia Logica, \textbf{73} (2003), 153--157.


%\bibitem{IntroNCL} S.P.~Odintsov, S.O.~Speranski, S.A.~Drobyshevich. {\it Introduction to Non-classical Logics}, %Novosibirsk State University, Novosibirsk, 2014.

\end{thebibliography}
\end{document}
