text:
\section{Introduction}
Sahlqvist theory has a long history in normal modal logic, going back to \cite{Sa75}. The Sahlqvist theorem in \cite{Sa75} gives a syntactic definition of a class of modal formulas, the {\em Sahlqvist class}, each member of which defines an elementary (i.e.\ first-order definable) class of frames and is canonical.

Over the years, many extensions, variations and analogues of this result have appeared, including alternative proofs in e.g.\ \cite{SaVa89}, generalizations to arbitrary modal signatures \cite{dRVe95}, variations of the correspondence language \cite{OhSc97,Benthem06}, Sahlqvist-type results for hybrid logics  \cite{tCMaVi06},  various substructural logics \cite{Kurtonina,DunnGP05,Ge06}, mu-calculus  \cite{BeHovB12}, and enlargements of the Sahlqvist class to e.g.\ the {\em inductive} formulas of \cite{GorankoV06}, to mention but a few.

Recently, a uniform and modular theory has emerged, called {\em unified correspondence} \cite{CoGhPa14}, which subsumes the above results and extends them to logics with a {\em non-classical} propositional base. It is built on duality-theoretic insights \cite{ConPalSou12} and uniformly exports the state-of-the-art in Sahlqvist theory from normal modal logic to a wide range of logics which include, among others, intuitionistic and distributive and general (non-distributive) lattice-based (modal) logics \cite{ConPal12, ConPal13},  non-normal (regular) modal logics based on distributive lattices of arbitrary modal signature \cite{PaSoZh15b}, hybrid logics \cite{CoRo14}, many valued logics, \cite{manyval} and bi-intuitionistic and lattice-based modal mu-calculus \cite{CoCr14,CoFoPaSo15,long-version}.

The breadth of this work has stimulated many and varied applications. Some are closely related to the core concerns of the theory itself, such as understanding the relationship between different methodologies for obtaining canonicity results \cite{PaSoZh15a,CPZ:constructive}, or the exploration of the limits of applicability of the theory \cite{zhao2017Hausdorff, zhao2016possibility} or of the phenomenon of pseudocorrespondence \cite{CoPaSoZh15}.  Other, possibly surprising applications include the dual characterizations of classes of finite lattices \cite{FrPaSa14}, the identification of the syntactic shape of axioms which can be translated into structural rules of a proper display calculus \cite{GrMaPaTzZh15} and of internal Gentzen calculi for the logics of strict implication \cite{MaZh15}, and the epistemic interpretation of lattice-based modal logic in terms of categorization theory in management science \cite{categorization, TarkPaper}. The approach underlying these results relies only on  the order-theoretic properties of the algebraic interpretations of logical connectives, abstracting away from specific logical signatures.

Featuring prominently among the logics targeted by  these developments are  (bi-)intuitionistic logic and their all modal expansions.
The theory of these logics has been intensively studied over the past seventy years using the  G\"{o}del-McKinsey-Tarski translation \cite{Godel:Interp, McKinseyTarski:Translation}, henceforth simply the GMT translation, as a key tool.
Specifically, since the 1940s and up to the present day, versions of the GMT translation have been used for transferring and reflecting results between classical and intuitionistic logics and their extensions and expansions (see e.g.\ \cite{mckinsey1948some, blok1976varieties, esakia1976modal, fischerservi1977modal, ChagrovZ91, WoZa97, WoZa98, wolter2014blok, vBBeHo16}. More on this in Section \ref{ssec:brief history}).

In view of this state-of-the-art, it is natural to ask (1) whether a general perspective on G\"odel-McKinsey-Tarski translations can be attained, also based on  order-theoretic principles like those underlying the general definition of Sahlqvist and inductive formulas and inequalities, which accounts for the known G\"odel-McKinsey-Tarski translations and applies uniformly to all signatures of normal (distributive) lattice expansions; (2) whether this general perspective can be used to transfer  correspondence and canonicity theorems for Sahlqvist and inductive formulas and inequalities in the signatures described above under G\"odel-McKinsey-Tarski translations.
In the present paper, we set out to answer these questions.

Notice that in general, GMT translations do not preserve the Sahlqvist shape.
For instance,
the original GMT translation
transforms the Sahlqvist inequality $\Box\Diamond p\leq \Diamond p$ into ${\Box\Diamond\Box_G p}\leq \Diamond \Box_G p$,  which is not Sahlqvist, and in fact does not even have a first-order correspondent \cite{vanBenthem:Reduction:Principles}. Any translation which `boxes' propositional variables would suffer from this problem (for further discussion  see \cite[Section 36.9]{CoGhPa14}).
However, {\em some} GMT translations preserve the shape of {\em some} Sahlqvist and inductive formulas or inequalities.
This has been exploited by Gehrke, Nagahashi and Venema in \cite{GeNaVe05} to obtain the correspondence part of their Sahlqvist theorem for Distributive Modal Logic. The need to establish a suitable match between GMT translations and Sahlqvist and inductive formulas or inequalities in each signature gives us a concrete reason to investigate GMT translations as a class.

The starting point of our analysis, and first contribution of the present paper, is an order-theoretic  generalization of the main semantic property of the original GMT translation. We show that  this generalization provides a unifying pattern, instantiated in the concrete GMT translations in each setting of interest to the present paper. As an application of this generalization, we prove two transfer results, which are the main contributions of the present paper: the transfer of {\em generalized Sahlqvist correspondence} from multi-modal (classical) modal logic to logics of arbitrary normal distributive lattice expansions and, in a more restricted setting, the transfer of {\em generalized Sahlqvist canonicity} from multi-modal (classical) modal logic  to logics of arbitrary normal {\em bi-Heyting algebra} expansions. The transfer of correspondence extends \cite[Theorem 3.7]{GeNaVe05} both as regards the setting (from Distributive Modal Logic to arbitrary normal DLE-logics) and the scope (from Sahlqvist to inductive inequalities). The transfer of canonicity is entirely novel also in its formulation, in the sense that it targets specific, syntactically defined classes. Finally, we  analyze the difficulties in extending the transfer of canonicity to  normal DLE-logics. Thanks to this analysis,  we identify a route towards this result, which -- however -- calls for a much higher level of technical sophistication than required by the usual route.
\begin{comment}
The conclusions that can be drawn from these results are twofold. On the one hand, when available, the transfer of results are a very powerful and concise route
, would require techniques that are not currently available.  Therefore the existing unified correspondence techniques remain the most economical route to these results.
\end{comment}
\begin{comment}
Overall, powerful and elegant as it is, the translation method does not provide autonomous foundations for a general Sahlqvist theory.
Indeed, any general development of Sahlqvist theory requires a uniform way to recognize Sahlqvist-type classes across logical signatures. For a treatment via translation to provide autonomous foundations for a general Sahlqvist theory, the specification of these syntactic classes  cannot be derived from the translation itself, but should be independent from it. The definitions of Sahlqvist and inductive inequalities  provided by unified correspondence are based on the order-theoretic analysis of the connectives of the logic under consideration, and are able to provide the required independent background. Thus, the transfer of generalized Sahlqvist theory developed in the present paper is, in fact, yet another application of unified correspondence.
\end{comment}

The paper is structured as follows. Section \ref{sec:preliminaries} collects preliminaries on  logics of normal DLEs and their algebraic and relational semantics. In Section \ref{semantic environment} we discuss  GMT translations in various DLE settings in the literature  and the semantic underpinnings of the GMT translation for intuitionistic logic. In Section \ref{ssec:template} we introduce a general template which accounts for the main semantic property of GMT translations---their being full and faithful---in the setting of ordered algebras of arbitrary signatures. In Section \ref{sec:instantiations}, we show that the GMT translations of interest instantiate this template. This sets the stage for Sections \ref{sec:Corresp:Via:Trans} and \ref{sec:canonicity} where we present our transfer results.
We conclude in Section \ref{Sec:Conclusions}.

\section{Preliminaries on normal DLEs and their logics}\label{sec:preliminaries}

In this section we collect some basic background on logics of normal distributive lattice expansions (DLEs). All the logics which we will consider in this paper are particular instances of DLE-logics.

\subsection{Language and axiomatization of basic DLE-logics}\label{subset:language:algsemantics}
Our base language is an unspecified but fixed language $\mathcal{L}_\mathrm{DLE}$, to be interpreted over distributive lattice expansions of compatible similarity type.
We will make heavy use of the following auxiliary definition: an {\em order-type} over $n\in \mathbb{N}$\footnote{Throughout the paper, order-types will be typically associated with arrays of variables $\vec p: = (p_1,\ldots, p_n)$. When the order of the variables in $\vec p$ is not specified, we will sometimes abuse notation and write $\varepsilon(p) = 1$ or $\varepsilon(p) = \partial$.} is an $n$-tuple $\epsilon\in \{1, \partial\}^n$. For every order type $\epsilon$, we denote its {\em opposite} order type by $\epsilon^\partial$, that is, $\epsilon^\partial_i = 1$ iff $\epsilon_i=\partial$ for every $1 \leq i \leq n$. For any lattice $\mathbb{A}$, we let $\mathbb{A}^1: = \mathbb{A}$ and $\mathbb{A}^\partial$ be the dual lattice, that is, the lattice associated with the converse partial order of $\mathbb{A}$. For any order type $\varepsilon$, we let $\mathbb{A}^\varepsilon: = \Pi_{i = 1}^n \mathbb{A}^{\varepsilon_i}$.

	The language $\mathcal{L}_\mathrm{DLE}(\mathcal{F}, \mathcal{G})$ (from now on abbreviated as $\mathcal{L}_\mathrm{DLE}$) takes as parameters: 1) a denumerable set $\mathsf{PROP}$ of proposition letters, elements of which are denoted $p,q,r$, possibly with indexes; 2) disjoint sets of connectives $\mathcal{F}$ and  $\mathcal{G}$.
Each $f\in \mathcal{F}$ and $g\in \mathcal{G}$ has arity $n_f\in \mathbb{N}$ (resp.\ $n_g\in \mathbb{N}$) and is associated with some order-type $\varepsilon_f$ over $n_f$ (resp.\ $\varepsilon_g$ over $n_g$).\footnote{Unary $f$ (resp.\ $g$) will be sometimes denoted as $\Diamond$ (resp.\ $\Box$) if the order-type is 1, and $\lhd$ (resp.\ $\rhd$) if the order-type is $\partial$.}
The terms (formulas) of $\mathcal{L}_\mathrm{DLE}$ are defined recursively as follows:
	\[
	\phi ::= p \mid \bot \mid \top \mid \phi \wedge \phi \mid \phi \vee \phi \mid f(\overline{\phi}) \mid g(\overline{\phi})
	\]
	where $p \in \mathsf{PROP}$, $f \in \mathcal{F}$, $g \in \mathcal{G}$. Terms in $\mathcal{L}_\mathrm{DLE}$ will be denoted either by $s,t$, or by lowercase Greek letters such as $\varphi, \psi, \gamma$ etc.

\begin{definition}
		\label{def:DLE:logic:general}
		For any language $\mathcal{L}_\mathrm{DLE} = \mathcal{L}_\mathrm{DLE}(\mathcal{F}, \mathcal{G})$, the {\em basic}, or {\em minimal} $\mathcal{L}_\mathrm{DLE}$-{\em logic} is a set of sequents $\phi\vdash\psi$, with $\phi,\psi\in\mathcal{L}_\mathrm{LE}$, which contains the following axioms:
		\begin{itemize}
			\item Sequents for  lattice operations:
			\begin{align*}
				&p\vdash p, && \bot\vdash p, && p\vdash \top, & & p\wedge (q\vee r)\vdash (p\wedge q)\vee (p\wedge r), &\\
				&p\vdash p\vee q, && q\vdash p\vee q, && p\wedge q\vdash p, && p\wedge q\vdash q, &
			\end{align*}
			\item Sequents for $f\in \mathcal{F}$ and $g\in \mathcal{G}$:
			\begin{align*}
				& f(p_1,\ldots, \bot,\ldots,p_{n_f}) \vdash \bot,~\mathrm{for}~ \varepsilon_f(i) = 1,\\
				& f(p_1,\ldots, \top,\ldots,p_{n_f}) \vdash \bot,~\mathrm{for}~ \varepsilon_f(i) = \partial,\\
				&\top\vdash g(p_1,\ldots, \top,\ldots,p_{n_g}),~\mathrm{for}~ \varepsilon_g(i) = 1,\\
				&\top\vdash g(p_1,\ldots, \bot,\ldots,p_{n_g}),~\mathrm{for}~ \varepsilon_g(i) = \partial,\\
				&f(p_1,\ldots, p\vee q,\ldots,p_{n_f}) \vdash f(p_1,\ldots, p,\ldots,p_{n_f})\vee f(p_1,\ldots, q,\ldots,p_{n_f}),~\mathrm{for}~ \varepsilon_f(i) = 1,\\
				&f(p_1,\ldots, p\wedge q,\ldots,p_{n_f}) \vdash f(p_1,\ldots, p,\ldots,p_{n_f})\vee f(p_1,\ldots, q,\ldots,p_{n_f}),~\mathrm{for}~ \varepsilon_f(i) = \partial,\\
				& g(p_1,\ldots, p,\ldots,p_{n_g})\wedge g(p_1,\ldots, q,\ldots,p_{n_g})\vdash g(p_1,\ldots, p\wedge q,\ldots,p_{n_g}),~\mathrm{for}~ \varepsilon_g(i) = 1,\\
				& g(p_1,\ldots, p,\ldots,p_{n_g})\wedge g(p_1,\ldots, q,\ldots,p_{n_g})\vdash g(p_1,\ldots, p\vee q,\ldots,p_{n_g}),~\mathrm{for}~ \varepsilon_g(i) = \partial,
			\end{align*}
		\end{itemize}
		and is closed under the following inference rules:
		\begin{displaymath}
			\frac{\phi\vdash \chi\quad \chi\vdash \psi}{\phi\vdash \psi}
			\quad
			\frac{\phi\vdash \psi}{\phi(\chi/p)\vdash\psi(\chi/p)}
			\quad
			\frac{\chi\vdash\phi\quad \chi\vdash\psi}{\chi\vdash \phi\wedge\psi}
			\quad
			\frac{\phi\vdash\chi\quad \psi\vdash\chi}{\phi\vee\psi\vdash\chi}
		\end{displaymath}
		\begin{displaymath}
			 \frac{\phi\vdash\psi}{f(p_1,\ldots,\phi,\ldots,p_n)\vdash f(p_1,\ldots,\psi,\ldots,p_n)}{~(\varepsilon_f(i) = 1)}
		\end{displaymath}
		\begin{displaymath}
			 \frac{\phi\vdash\psi}{f(p_1,\ldots,\psi,\ldots,p_n)\vdash f(p_1,\ldots,\phi,\ldots,p_n)}{~(\varepsilon_f(i) = \partial)}
		\end{displaymath}
		\begin{displaymath}
			 \frac{\phi\vdash\psi}{g(p_1,\ldots,\phi,\ldots,p_n)\vdash g(p_1,\ldots,\psi,\ldots,p_n)}{~(\varepsilon_g(i) = 1)}
		\end{displaymath}
		\begin{displaymath}
			 \frac{\phi\vdash\psi}{g(p_1,\ldots,\psi,\ldots,p_n)\vdash g(p_1,\ldots,\phi,\ldots,p_n)}{~(\varepsilon_g(i) = \partial)}.
		\end{displaymath}
		The minimal DLE-logic is denoted by $\mathbf{L}_\mathrm{DLE}$. For any DLE-language $\mathcal{L}_{\mathrm{DLE}}$, by an {\em $\mathrm{DLE}$-logic} we understand any axiomatic extension of the basic $\mathcal{L}_{\mathrm{DLE}}$-logic in $\mathcal{L}_{\mathrm{DLE}}$.
	\end{definition}

\begin{example}
\label{ex:various DLE-languages}
 The DLE setting is extremely general, covering a wide spectrum of non-classical logics. Here we give a few examples, showing how various languages are obtained as specific instantiations of $\mathcal{F}$ and $\mathcal{G}$. The associated logics extended the basic DLE logics corresponding to these instantiations.

 The formulas of intuitionistic logic are obtained by instantiating $\mathcal{F}: = \varnothing$   and   $\mathcal{G}: = \{\rightarrow\}$ with $n_\rightarrow = 2$, and $\varepsilon_\rightarrow = (\partial, 1)$. The formulas of bi-intuitionistic logic (cf.~\cite{rauszer1974semi})  are obtained by instantiating $\mathcal{F}: = \{\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \}$ with $n_{\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}}  = 2$ and $\varepsilon_{\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}} = (\partial, 1)$,  and   $\mathcal{G}: = \{\rightarrow\}$ with $n_\rightarrow = 2$ and $\varepsilon_\rightarrow = (\partial, 1)$. The formulas of Fischer Servi's intuitionistic modal logic (cf.~\cite{fischerservi1977modal}), Prior's MIPC (cf.~\cite{prior1955time}), and G.~Bezhanishvili's intuitionistic modal logic with universal modalities (cf.~\cite{bezhanishvili2009universal}) are obtained by instantiating $\mathcal{F}: = \{\Diamond\}$ with $n_\Diamond  = 1$ and $\varepsilon_\Diamond = 1$   and   $\mathcal{G}: = \{\rightarrow, \Box\}$ with $n_\rightarrow = 2$, and $\varepsilon_\rightarrow = (\partial, 1)$, and $n_\Box = 1$, and $\varepsilon_\Box = 1$.
 The formulas of Wolter's bi-intuitionistic modal logic (cf.~\cite{wolter1998CoImplication}) are obtained by instantiating $\mathcal{F}: = \{\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}, \Diamond\}$ with $n_\Diamond  = 1$ and $\varepsilon_\Diamond = 1$  and $n_{\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}}  = 2$ and $\varepsilon_{\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}} = (\partial, 1)$,  and   $\mathcal{G}: = \{\rightarrow, \Box\}$ with $n_\rightarrow = 2$, and $\varepsilon_\rightarrow = (\partial, 1)$, and $n_\Box = 1$, and $\varepsilon_\Box = 1$.  The formulas of Dunn's \emph{positive modal logic} (cf.\ \cite{dunn1995positive}) are obtained by instantiating $\mathcal{F}: = \{\Diamond\}$ with $n_\Diamond = 1$, $\varepsilon_\Diamond = 1$  and  $\mathcal{G}: = \{\Box \}$ with $n_\Box = 1$ and $\varepsilon_\Box = 1$. The language of Gehrke, Nagahashi and Venema's \emph{distributive modal logic} (cf.\ \cite{GeNaVe05}) is an expansion of positive modal logic and is obtained by adding the connectives ${\lhd}$ and ${\rhd}$ to $\mathcal{F}$ and $\mathcal{G}$, respectively, with $n_\lhd = n_\rhd = 1$ and $\varepsilon_\lhd = \varepsilon_\rhd = \partial$.
\end{example}

\subsection{Algebraic and relational semantics for basic DLE-logics}\label{ssec: DLEs}
The following definition captures the algebraic setting of the present paper:

	\begin{definition}
		\label{def:DLE}
		For any tuple $(\mathcal{F}, \mathcal{G})$ of disjoint sets of function symbols as above, a {\em distributive lattice expansion} (abbreviated as DLE) is a tuple $\mathbb{A} = (L, \mathcal{F}^\mathbb{A}, \mathcal{G}^\mathbb{A})$ such that $L$ is a bounded distributive lattice, $\mathcal{F}^\mathbb{A} = \{f^\mathbb{A}\mid f\in \mathcal{F}\}$ and $\mathcal{G}^\mathbb{A} = \{g^\mathbb{A}\mid g\in \mathcal{G}\}$, such that every $f^\mathbb{A}\in\mathcal{F}^\mathbb{A}$ (resp.\ $g^\mathbb{A}\in\mathcal{G}^\mathbb{A}$) is an $n_f$-ary (resp.\ $n_g$-ary) operation on $\mathbb{A}$. A DLE is {\em normal} if every $f^\mathbb{A}\in\mathcal{F}^\mathbb{A}$ (resp.\ $g^\mathbb{A}\in\mathcal{G}^\mathbb{A}$) preserves finite (hence also empty) joins (resp.\ meets) in each coordinate with $\epsilon_f(i)=1$ (resp.\ $\epsilon_g(i)=1$) and reverses finite (hence also empty) meets (resp.\ joins) in each coordinate with $\epsilon_f(i)=\partial$ (resp.\ $\epsilon_g(i)=\partial$).\footnote{\label{footnote:DLE vs DLO} Normal DLEs are sometimes referred to as {\em distributive lattices with operators} (DLOs). This terminology derives from the setting of Boolean algebras with operators, in which operators are understood as operations which preserve finite (hence also empty) joins in each coordinate. Thanks to the Boolean negation, operators are typically taken as primitive connectives, and all the other modal operations are reduced to these. However, this terminology is somewhat ambiguous in the lattice setting, in which primitive operations are typically maps which are operators if seen as $\mathbb{A}^\epsilon\to \mathbb{A}^\eta$ for some order-type $\epsilon$ on $n$ and some order-type $\eta\in \{1, \partial\}$. Rather than speaking of lattices with $(\varepsilon, \eta)$-operators, we then speak of normal DLEs. This terminology is also used in other papers developing Sahlqvist-type results at a  level of generality comparable to that of the present paper, e.g.~\cite{GrMaPaTzZh15, long-version}.} Let $\mathbb{DLE}$ be the class of normal DLEs. Sometimes we will refer to certain DLEs as $\mathcal{L}_\mathrm{DLE}$-algebras when we wish to emphasize that these algebras have a compatible signature with the logical language we have fixed.
A distributive lattice is {\em perfect} if it is complete, completely distributive and completely join-generated by  its completely join-prime elements. Equivalently, a distributive lattice is perfect iff it is isomorphic to the lattice of up-sets of some poset. A normal DLE is {\em perfect} if its lattice-reduct is a perfect distributive lattice, and each $f$-operation (resp.\ $g$-operation) is completely join-preserving (resp.\ meet-preserving) in the coordinates $i$ such that $\epsilon_f(i) = 1$ (resp.~$\epsilon_g(i) = 1$) and completely meet-reversing (resp.\ join-reversing) in the coordinates $i$ such that $\epsilon_f(i) = \partial$ (resp.~$\epsilon_g(i) = \partial$). The {\em canonical extension}  of a  normal DLE $\mathbb{A} = (L, \mathcal{F}, \mathcal{G})$
 is  the perfect normal DLE $\mathbb{A}^\delta: = (L^\delta, \mathcal{F}^\sigma, \mathcal{G}^\pi)$, where $L^\delta$  is the canonical extension of  $L$,\footnote{The \emph{canonical extension} of a bounded  lattice $L$ is a complete  lattice $L^\delta$ containing $L$ as a sublattice, such that:
				\begin{enumerate}
					\item \emph{(denseness)} every element of $L^\delta$ is both the join of meets and the meet of joins of elements from $L$;
					\item \emph{(compactness)} for all $S,T \subseteq L$, if $\bigwedge S \leq \bigvee T$ in $L^\delta$, then $\bigwedge F \leq \bigvee G$ for some finite sets $F \subseteq S$ and $G\subseteq T$.
				\end{enumerate}
}
and $\mathcal{F}^\sigma: = \{f^\sigma\mid f\in \mathcal{F}\}$ and  $\mathcal{G}^\pi: = \{g^\pi\mid g\in \mathcal{G}\}$.\footnote{An element $k \in L^\delta$ (resp.~$o\in L^\delta$) is \emph{closed} (resp.\ \emph{open}) if is the meet (resp.\ join) of some subset of $L$. We let $K(L^\delta)$ (resp.~$O(L^\delta)$) denote the set of the closed (resp.~open) elements of $L^\delta$. For every unary, order-preserving map $h : L \to M$ between bounded lattices, the $\sigma$-{\em extension} of $h$ is defined firstly by declaring, for every $k\in K(L^\delta)$,
$$h^\sigma(k):= \bigwedge\{ h(a)\mid a\in L\mbox{ and } k\leq a\},$$ and then, for every $u\in L^\delta$,
$$h^\sigma(u):= \bigvee\{ h^\sigma(k)\mid k\in K(L^\delta)\mbox{ and } k\leq u\}.$$
The $\pi$-{\em extension} of $f$ is defined firstly by declaring, for every $o\in O(L^\delta)$,
$$h^\pi(o):= \bigvee\{ h(a)\mid a\in L\mbox{ and } a\leq o\},$$ and then, for every $u\in L^\delta$,
$$h^\pi(u):= \bigwedge\{ h^\pi(o)\mid o\in O(L^\delta)\mbox{ and } u\leq o\}.$$
The definitions above apply also to operations of any finite arity and order-type. Indeed,
taking  order-duals interchanges closed and open elements:
$K({(L^\delta)}^\partial) = O(L^\delta)$ and $O({(L^\delta)}^\partial) = K(L^\delta)$;  similarly, $K({(L^n)}^\delta) =K(L^\delta)^n$, and $O({(L^n)}^\delta) =O(L^\delta)^n$. Hence,  $K({(L^\delta)}^\epsilon) =\prod_i K(L^\delta)^{\epsilon(i)}$ and $O({(L^\delta)}^\epsilon) =\prod_i O(L^\delta)^{\epsilon(i)}$ for every lattice $L$ and every order-type $\epsilon$ over any $n\in \mathbb{N}$, where
\begin{center}
\begin{tabular}{cc}
$K(L^\delta)^{\epsilon(i)}: =\begin{cases}
K(L^\delta) & \mbox{if } \epsilon(i) = 1\\
O(L^\delta) & \mbox{if } \epsilon(i) = \partial\\
\end{cases}
$ &
$O(L^\delta)^{\epsilon(i)}: =\begin{cases}
O(L^\delta) & \mbox{if } \epsilon(i) = 1\\
K(L^\delta) & \mbox{if } \epsilon(i) = \partial.\\
\end{cases}
$\\
\end{tabular}
\end{center}
From this it follows that
 ${(L^\partial)}^\delta$ can be  identified with ${(L^\delta)}^\partial$,  ${(L^n)}^\delta$ with ${(L^\delta)}^n$, and
${(L^\epsilon)}^\delta$ with ${(L^\delta)}^\epsilon$ for any order type $\epsilon$ over $n$, where $L^\epsilon: = \prod_{i = 1}^n L^{\epsilon(i)}$.
These identifications make it possible to obtain the definition of $\sigma$-and $\pi$-extensions of $\epsilon$-monotone operations of any arity $n$ and order-type $\epsilon$ over $n$ by instantiating the corresponding definitions given above for monotone and unary functions.
}
Canonical extensions of  Heyting algebras, Brouwerian algebras and bi-Heyting algebras are defined by instantiating the definition above in the corresponding  signatures. The canonical extension of any Heyting (resp.~Brouwerian, bi Heyting) algebra is a (perfect) Heyting (resp.~Brouwerian, bi-Heyting) algebra.
\end{definition}

In the present paper we also find it convenient to talk of normal Boolean algebra expansions (BAEs) (respectively, normal Heyting algebra expansions (HAEs), normal bi-Heyting algebra expansions (bHAEs)) which are structures defined as in Definition \ref{def:DLE}, but replacing the distributive lattice $L$ with a Boolean algebra (respectively, Heyting algebra, bi-Heyting algebra). The logics corresponding to these classes will be collectively referred to as normal BAE-logics, normal HAE-logics, normal bHAE-logics. In what follows we will typically drop the adjective `normal'.

In the remainder of the paper, we will abuse notation and write e.g.\ $f$ for $f^\mathbb{A}$ when this causes no confusion.
Normal DLEs constitute the main semantic environment of the present paper. Henceforth, since every DLE is assumed to be normal, the adjective will be typically dropped.
The class of all DLEs is equational, and can be axiomatized by the usual distributive lattice identities and the following equations for any $f\in \mathcal{F}$ (resp.\ $g\in \mathcal{G}$) and $1\leq i\leq n_f$ (resp.\ for each $1\leq j\leq n_g$):
	\begin{itemize}
		\item if $\varepsilon_f(i) = 1$, then $f(p_1,\ldots, p\vee q,\ldots,p_{n_f}) = f(p_1,\ldots, p,\ldots,p_{n_f})\vee f(p_1,\ldots, q,\ldots,p_{n_f})$; moreover if $f\in \mathcal{F}_n$, then $f(p_1,\ldots, \bot,\ldots,p_{n_f}) = \bot$,
		\item if $\varepsilon_f(i) = \partial$, then $f(p_1,\ldots, p\wedge q,\ldots,p_{n_f}) = f(p_1,\ldots, p,\ldots,p_{n_f})\vee f(p_1,\ldots, q,\ldots,p_{n_f})$; moreover if $f\in \mathcal{F}_n$, then  $f(p_1,\ldots, \top,\ldots,p_{n_f}) = \bot$,
		\item if $\varepsilon_g(j) = 1$, then $g(p_1,\ldots, p\wedge q,\ldots,p_{n_g}) = g(p_1,\ldots, p,\ldots,p_{n_g})\wedge g(p_1,\ldots, q,\ldots,p_{n_g})$; moreover if $g\in \mathcal{G}_n$, then  $g(p_1,\ldots, \top,\ldots,p_{n_g}) = \top$,
		\item if $\varepsilon_g(j) = \partial$, then $g(p_1,\ldots, p\vee q,\ldots,p_{n_g}) = g(p_1,\ldots, p,\ldots,p_{n_g})\wedge g(p_1,\ldots, q,\ldots,p_{n_g})$; moreover if $g\in \mathcal{G}_n$, then  $g(p_1,\ldots, \bot,\ldots,p_{n_g}) = \top$.
	\end{itemize}
	Each language $\mathcal{L}_\mathrm{DLE}$ is interpreted in the appropriate class of DLEs. In particular, for every DLE $\mathbb{A}$, each operation $f^\mathbb{A}\in \mathcal{F}^\mathbb{A}$ (resp.\ $g^\mathbb{A}\in \mathcal{G}^\mathbb{A}$) is finitely join-preserving (resp.\ meet-preserving) in each coordinate when regarded as a map $f^\mathbb{A}: \mathbb{A}^{\varepsilon_f}\to \mathbb{A}$ (resp.\ $g^\mathbb{A}: \mathbb{A}^{\varepsilon_g}\to \mathbb{A}$).

	For every DLE $\mathbb{A}$, the symbol $\vdash$ is interpreted as the lattice order $\leq$. A sequent $\phi\vdash\psi$ is valid in $\mathbb{A}$ if $h(\phi)\leq h(\psi)$ for every homomorphism $h$ from the $\mathcal{L}_\mathrm{DLE}$-algebra of formulas over $\mathsf{PROP}$ to $\mathbb{A}$. The notation $\mathbb{DLE}\models\phi\vdash\psi$ indicates that $\phi\vdash\psi$ is valid in every DLE. Then, by means of a routine Lindenbaum-Tarski construction, it can be shown that the minimal DLE-logic $\mathbf{L}_\mathrm{DLE}$ is sound and complete with respect to its corresponding class of algebras $\mathbb{DLE}$, i.e.\ that any sequent $\phi\vdash\psi$ is provable in $\mathbf{L}_\mathrm{DLE}$ iff $\mathbb{DLE}\models\phi\vdash\psi$.

\begin{definition}
\label{def:DLE frame}
An $\mathcal{L}_{\mathrm{DLE}}$-{\em frame} is a tuple $\mathbb{F} = (\mathbb{X}, \mathcal{R}_{\mathcal{F}}, \mathcal{R}_{\mathcal{G}})$ such that $\mathbb{X} = (W, \leq)$ is a (nonempty) poset, $\mathcal{R}_{\mathcal{F}} = \{R_f\mid f\in \mathcal{F}\}$, and $\mathcal{R}_{\mathcal{G}} = \{R_g\mid g\in \mathcal{G}\}$ such that  for each $f\in \mathcal{F}$, the symbol $R_f$  denotes an $(n_f+1)$-ary  relation on $W$ such that
for all $\overline{w}, \overline{v}\in  \mathbb{X}^{\eta_f}$,
\begin{equation}\label{eq:compatibility Rf}
 \mbox{if } R_f(\overline{w})\ \mbox{ and }\ \overline{w}\leq^{\eta_f} \overline{v},\ \mbox{ then }\  R_f(\overline{v}),\end{equation}
where $\eta_f$ is the order-type on $n_f+1$ defined as follows: $\eta_f(1) = 1$ and $\eta_f(i+1) = \epsilon^\partial_f(i)$ for each $1\leq i\leq n_f$.

Likewise, for each $g\in \mathcal{G}$, the symbol  $R_g$ denotes an $(n_g+1)$-ary relation on $W$ such that
for all $\overline{w}, \overline{v}\in  \mathbb{X}^{\eta_g}$,
\begin{equation}\label{eq:compatibility Rg}
\mbox{if } R_g(\overline{w})\   \mbox{ and }\  \overline{w}\geq^{\eta_g} \overline{v},\ \mbox{ then }\ R_g(\overline{v}),\end{equation}
where $\eta_g$ is the order-type on $n_g+1$ defined as follows: $\eta_g(1) = 1$ and $\eta_g(i+1) = \epsilon_g^\partial(i)$ for each $1\leq i\leq n_g$.

An $\mathcal{L}_{\mathrm{DLE}}$-{\em model} is a tuple $\mathbb{M} = (\mathbb{F}, V)$ such that $\mathbb{F}$ is an $\mathcal{L}_{\mathrm{DLE}}$-frame, and $V:\mathsf{Prop}\to \mathcal{P}^{\uparrow}(W)$ is a persistent valuation.
\end{definition}

The defining clauses for the interpretation of each $f\in \mathcal{F}$ and $g\in \mathcal{G}$ on $\mathcal{L}_{\mathrm{DLE}}$-models are given as follows:
\begin{center}
\begin{tabular}{l l l}
$\mathbb{M},w \Vdash f(\overline{\phi})$ & $\quad$ & $\mbox{ iff } \quad \mbox{ there exists some } \overline{v} \in W^{n_f} \mbox{ s.t. } R_f(w, \overline{v}) \mbox{ and } \mathbb{M}, v_i \Vdash^{\epsilon_f(i)} \phi_i \mbox{ for each } 1\leq i\leq n_f,$\\

$\mathbb{M},w \Vdash g(\overline{\phi})$ & $\quad$ &$\mbox{ iff } \quad \mbox{ for any } \overline{v} \in W^{n_g}, \mbox{ if } R_g(w, \overline{v}) \mbox{ then } \mathbb{M}, v_i \Vdash^{\epsilon_g(i)} \phi_i \mbox{ for some } 1\leq i\leq n_g,$\\
\end{tabular}
\end{center}
where $\Vdash^1$ is $\Vdash$ and $\Vdash^\partial$ is $\nVdash$.

\subsection{Sahlqvist and Inductive $\mathcal{L}_\mathrm{DLE}$-inequalities}\label{ssec:Inductive:Ineqs}

In the present subsection, we recall the definitions of {\em Sahlqvist} and {\em inductive} $\mathcal{L}_\mathrm{DLE}$-inequalities (cf.~\cite[Definition 3.4]{ConPal13}), which we will show to be preserved and reflected under suitable GMT translations in Section \ref{sec:Corresp:Via:Trans}. These definitions capture the non-classical counterparts, in each normal modal signature, of the classes of Sahlqvist (\cite{Sa75}) and inductive (\cite{GorankoV06}) formulas. The definition is given in terms of the order-theoretic properties of the interpretation of the logical connectives
(cf.\ \cite{CoGhPa14,ConPal12,ConPal13} for expanded discussions on the design principles of this definition). The fact that this notion applies uniformly across arbitrary normal modal signatures makes it possible to give a very general yet mathematically precise formulation to the question about the transfer of Sahlqvist-type results under GMT translations.

Technically speaking, these definitions are given parametrically in an order type. This contrasts to with the classical case, where the constantly-$1$ order-type is sufficient to encompass all Sahlqvist formulas. As a result, the preservation of the syntactic shape of each of these inequalities requires a GMT translation parametrized by the same order-type. These parametric translations will be introduced in Section \ref{Sec:ParamGMTTrans}.

\begin{definition}[\textbf{Signed Generation Tree}]
	\label{def: signed gen tree}
	The \emph{positive} (resp.\ \emph{negative}) {\em generation tree} of any $\mathcal{L}_\mathrm{DLE}$-term $s$ is defined by labelling the root node of the generation tree of $s$ with the sign $+$ (resp.\ $-$), and then propagating the labelling on each remaining node as follows:
	\begin{itemize}

		\item For any node labelled with $ \lor$ or $\land$, assign the same sign to its children nodes.

		\item For any node labelled with $h\in \mathcal{F}\cup \mathcal{G}$ of arity $n_h\geq 1$, and for any $1\leq i\leq n_h$, assign the same (resp.\ the opposite) sign to its $i$th child node if $\varepsilon_h(i) = 1$ (resp.\ if $\varepsilon_h(i) = \partial$).
	\end{itemize}
	Nodes in signed generation trees are \emph{positive} (resp.\ \emph{negative}) if are signed $+$ (resp.\ $-$).
\end{definition}

Signed generation trees will be mostly used in the context of term inequalities $s\leq t$. In this context we will typically consider the positive generation tree $+s$ for the left-hand side and the negative one $-t$ for the right-hand side.

For any term $s(p_1,\ldots p_n)$, any order type $\epsilon$ over $n$, and any $1 \leq i \leq n$, an \emph{$\epsilon$-critical node} in a signed generation tree of $s$ is a leaf node $+p_i$ with $\epsilon_i = 1$ or $-p_i$ with $\epsilon_i = \partial$. An $\epsilon$-{\em critical branch} in the tree is a branch from an $\epsilon$-critical node. The intuition is that variable occurrences corresponding to $\epsilon$-critical nodes are those that the algorithm ALBA will solve for in the process of eliminating them.

For every term $s(p_1,\ldots p_n)$ and every order type $\epsilon$, we say that $+s$ (resp.\ $-s$) {\em agrees with} $\epsilon$, and write $\epsilon(+s)$ (resp.\ $\epsilon(-s)$), if every leaf in the signed generation tree of $+s$ (resp.\ $-s$) is $\epsilon$-critical.
In other words, $\epsilon(+s)$ (resp.\ $\epsilon(-s)$) means that all variable occurrences corresponding to leaves of $+s$ (resp.\ $-s$) are to be solved for according to $\epsilon$. We will also write $+s'\prec \ast s$ (resp.\ $-s'\prec \ast s$) to indicate that the subterm $s'$ inherits the positive (resp.\ negative) sign from the signed generation tree $\ast s$. Finally, we will write $\epsilon(\gamma) \prec \ast s$ (resp.\ $\epsilon^\partial(\gamma) \prec \ast s$) to indicate that the signed subtree $\gamma$, with the sign inherited from $\ast s$, agrees with $\epsilon$ (resp.\ with $\epsilon^\partial$).
\begin{definition}
	\label{def:good:branch}
	Nodes in signed generation trees will be called \emph{$\Delta$-adjoints}, \emph{syntactically left residual (SLR)}, \emph{syntactically right residual (SRR)}, and \emph{syntactically right adjoint (SRA)}, according to the specification given in Table \ref{Join:and:Meet:Friendly:Table}.
	A branch in a signed generation tree $\ast s$, with $\ast \in \{+, - \}$, is called a \emph{good branch} if it is the concatenation of two paths $P_1$ and $P_2$, one of which may possibly be of length $0$, such that $P_1$ is a path from the leaf consisting (apart from variable nodes) only of PIA-nodes, and $P_2$ consists (apart from variable nodes) only of Skeleton-nodes. A good branch in which the nodes in $P_1$ are all SRA is called {\em excellent}.

	\begin{table}[h]
		\begin{center}
			\begin{tabular}{| c | c |}
				\hline
				Skeleton &PIA\\
				\hline
				$\Delta$-adjoints & SRA \\
				\begin{tabular}{ c c c c c c}
					$+$ &$\vee$ &$\wedge$ &$\phantom{\lhd}$ & &\\
					$-$ &$\wedge$ &$\vee$\\
					\hline
				\end{tabular}
				&
				\begin{tabular}{c c c c }
					$+$ &$\wedge$ &$g$ & with $n_g = 1$ \\
					$-$ &$\vee$ &$f$ & with $n_f = 1$ \\
					\hline
				\end{tabular}
				%
				\\
				SLR &SRR\\
				\begin{tabular}{c c c c }
					$+$ & $\wedge$ &$f$ & with $n_f \geq 1$\\
					$-$ & $\vee$ &$g$ & with $n_g \geq 1$ \\
				\end{tabular}
				%
				&\begin{tabular}{c c c c}
					$+$ &$\vee$ &$g$ & with $n_g \geq 2$\\
					$-$ & $\wedge$ &$f$ & with $n_f \geq 2$\\
				\end{tabular}
				\\
				\hline
			\end{tabular}
		\end{center}
		\caption{Skeleton and PIA nodes for $\mathrm{DLE}$.}\label{Join:and:Meet:Friendly:Table}
		\vspace{-1em}
	\end{table}
\end{definition}

\begin{figure*}
	\begin{center}
		\begin{tikzpicture}
		\draw (-5,-1.5)   -- (-3,1.5) node[above]{\Large$+$} ;
		\draw (-5,-1.5) -- (-1,-1.5) ;
		\draw (-3,1.5) -- (-1,-1.5);
		\draw (-5,0) node{Skeleton}  ;
		\draw[dashed] (-3,1.5) -- (-4,-1.5);

		\draw (-4,-1.5) --(-4.8,-3);
		\draw (-4.8,-3) --(-3.2,-3);
		\draw (-3.2,-3) --(-4,-1.5);
		\draw[dashed] (-4,-1.5) -- (-4,-3);
		\draw[fill] (-4,-3) circle[radius=.1] node[below]{$+p$};

		\draw
		(-2,-1.5) -- (-2.8,-3) -- (-1.2,-3) -- (-2,-1.5);
		\fill[lightgray]
		(-2,-1.5) -- (-2.8,-3) -- (-1.2,-3);
		\draw (-1,-2.25)node{$\gamma$};
		\draw (-5,-2.25) node{PIA}  ;
		\draw (0,1.8) node{$\leq$};
		\draw (5,-1.5)   -- (3,1.5) node[above]{\Large$-$} ;
		\draw (5,-1.5) -- (1,-1.5) ;
		\draw (3,1.5) -- (1,-1.5);
		\draw (5,0) node{Skeleton}  ;

		\draw[dashed] (3,1.5) -- (2,-1.5);
		\draw (2,-1.5) --(2.8,-3);
		\draw (2.8,-3) --(1.2,-3);
		\draw (1.2,-3) --(2,-1.5);
		\draw[dashed] (2,-1.5) -- (2,-3);
		\draw[fill] (2,-3) circle[radius=.1] node[below]{$+p$};
		\draw
		(4,-1.5) -- (4.8,-3) -- (3.2,-3) -- (4, -1.5);
		\fill[lightgray]
		(4,-1.5) -- (4.8,-3) -- (3.2,-3) -- (4, -1.5);
		\draw (5,-2.25)node{$\gamma'$};
		\draw (1,-2.25) node{PIA} ;

		\draw[fill] (-2,-3) circle[radius=.1] node[below]{$-p$};
		\draw[fill] (4,-3) circle[radius=.1] node[below]{$-p$};
		\end{tikzpicture}
		\caption{A schematic representation of inductive inequalities.}
	\end{center}
\end{figure*}

\begin{definition}[Sahlqvist and Inductive inequalities]
	\label{Inducive:Ineq:Def}
	For any order type $\epsilon$, the signed generation tree $*s$ $(* \in \{-, + \})$ of a term $s(p_1,\ldots p_n)$ is \emph{$\epsilon$-Sahlqvist} if
	for all $1 \leq i \leq n$, every $\epsilon$-critical branch with leaf $p_i$ is excellent (cf.\ Definition \ref{def:good:branch}). An inequality $s \leq t$ is \emph{$\epsilon$-Sahlqvist} if the signed generation trees $+s$ and $-t$ are $\epsilon$-Sahlqvist. An inequality $s \leq t$ is \emph{Sahlqvist} if it is $\epsilon$-Sahlqvist for some  $\epsilon$.

	For any order type $\epsilon$ and any irreflexive and transitive relation $<_\Omega$ on $p_1,\ldots p_n$, the signed generation tree $*s$ $(* \in \{-, + \})$ of a term $s(p_1,\ldots p_n)$ is \emph{$(\Omega, \epsilon)$-inductive} if
	\begin{enumerate}
		\item for all $1 \leq i \leq n$, every $\epsilon$-critical branch with leaf $p_i$ is good (cf.\ Definition \ref{def:good:branch});
		\item every $m$-ary SRR-node occurring in the critical branch is of the form $ \circledast(\gamma_1,\dots,\gamma_{j-1},\beta,\gamma_{j+1}\ldots,\gamma_m)$, where for any $h\in\{1,\ldots,m\}\setminus j$:
		%
		\begin{enumerate}
			%
			\item $\epsilon^\partial(\gamma_h) \prec \ast s$ (cf.\ discussion before Definition \ref{def:good:branch}), and

			%
			\item $p_k <_{\Omega} p_i$ for every $p_k$ occurring in $\gamma_h$ and for every $1\leq k\leq n$.
		\end{enumerate}

	\end{enumerate}

	We will refer to $<_{\Omega}$ as the \emph{dependency order} on the variables. An inequality $s \leq t$ is \emph{$(\Omega, \epsilon)$-inductive} if the signed generation trees $+s$ and $-t$ are $(\Omega, \epsilon)$-inductive. An inequality $s \leq t$ is \emph{inductive} if it is $(\Omega, \epsilon)$-inductive for some $<_\Omega$ and $\epsilon$.
\end{definition}
The definition above specializes so as to account for all the settings in which GMT translations have been defined. Below we expand on a selection of these.

\begin{example}[Intuitionistic language]\label{ex: frege ineq}

	As observed in \cite{ConPal12}, the Frege inequality

	\[p\rightarrow(q\rightarrow r)\leq (p\rightarrow q)\rightarrow (p\rightarrow r)\]

	\noindent is not Sahlqvist for any order type, but is $(\Omega, \epsilon)$-inductive, e.g.\ for $r <_\Omega p <_\Omega q$ and $\epsilon(p, q, r) =(1, 1, \partial)$,  as can be seen from the signed generation trees below:

	\begin{center}
		\begin{multicols}{3}
			\begin{tikzpicture}
			\tikzstyle{level 1}=[level distance=1cm, sibling distance=2.5cm]
			\tikzstyle{level 2}=[level distance=1cm, sibling distance=1.5cm]
			\tikzstyle{level 3}=[level distance=1 cm, sibling distance=1.5cm]
			\node[PIA] {$+\rightarrow$}
			child{node{$-p$}}
			child{node[PIA]{$+\rightarrow$}
				child{node{$-q$}}
				child{node{$+r$}}}
			;

			\end{tikzpicture}

			\columnbreak
			$\leq$
			\columnbreak
			\begin{tikzpicture}
			\tikzstyle{level 1}=[level distance=1cm, sibling distance=2.5cm]
			\tikzstyle{level 2}=[level distance=1cm, sibling distance=1.5cm]
			\tikzstyle{level 3}=[level distance=1 cm, sibling distance=1.5cm]
			\node[Ske]{$-\rightarrow$}
			child{node[PIA]{$+\rightarrow$}
				child{node{$-p$}}
				child{node{\circled{$+q$}}}}
			child{node[Ske]{$-\rightarrow$}
				child{node{\circled{$+p$}}}
				child{node{\circled{$-r$}}}}
			;
			\end{tikzpicture}
		\end{multicols}

	\end{center}
	In the picture above, the circled variable occurrences are the $\epsilon$-critical ones, the nodes in double ellipses are Skeleton, and those in single ellipses are PIA.
\end{example}

\begin{example}[Bi-intuitionistic language]\label{ex: non inductive} In \cite[Section 4]{rauszer1974semi}, Rauszer  axiomatizes bi-intuitionistic logic considering the following  axioms among others, which we present in the form of inequalities:
	\[r\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} (q\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} p)\leq (p\vee q)\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} p\quad\quad (q\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} p)\rightarrow \bot\leq p\rightarrow q.\]
	The first inequality is not $(\Omega, \epsilon)$-inductive for any $\Omega$ and $\epsilon$; indeed, in the negative generation tree of $(p\vee q)\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} p$, the variable  $p$ occurs in both subtrees rooted at the children of the root, which is  a binary SRR node, making it impossible to satisfy condition 2(b) of Definition \ref{Inducive:Ineq:Def} for any order-type $\epsilon$ and strict ordering $\Omega$.

	The second inequality is $\epsilon$-Sahlqvist for $\epsilon (p) = 1$ and $\epsilon (q) = \partial$, and is also $(\Omega, \epsilon)$-inductive but not Sahlqvist for $q<_{\Omega} p$ and $\epsilon(p) = \epsilon(q) = \partial$. It is  also $(\Omega, \epsilon)$-inductive but not Sahlqvist for $p<_{\Omega} q$ and $\epsilon(p) = \epsilon(q) = 1$.
\end{example}

\begin{example}[Intuitionistic  bi-modal language]
	The following Fischer Servi inequalities (cf.~\cite{fischerservi1977modal})
	\[\Diamond(q\rightarrow p)\leq \Box q\rightarrow \Diamond p \quad \quad \Diamond q\rightarrow \Box p\leq \Box (q\rightarrow p),\]
	are both $\varepsilon$-Sahlqvist for $\varepsilon(p) = \partial$ and $\varepsilon(q) = 1$, and are also both  $(\Omega, \varepsilon)$-inductive but not Sahlqvist for $p<_{\Omega} q$ and $\varepsilon(p) = \partial$ and $\varepsilon(q) = \partial$.
\end{example}

\begin{example}[Distributive modal  language]
	The following inequalities are key to Dunn's positive modal logic \cite{dunn1995positive}, the language of which is the $\{\lhd, \rhd\}$-free fragment of the language of Distributive Modal Logic \cite{GeNaVe05}:
	\[\Box q\wedge \Diamond p\leq \Diamond(q\wedge p) \quad \quad  \Box (q\vee p)\leq  \Diamond q\vee \Box p.\]
	The inequality on the left (resp.~right) is  $\varepsilon$-Sahlqvist for $\varepsilon(p) = \varepsilon(q) = 1$ (resp.~$\varepsilon(p) = \varepsilon(q) = \partial$), and is  $(\Omega, \varepsilon)$-inductive but not Sahlqvist for $p<_{\Omega} q$ and $\varepsilon(p) = 1$ and $\varepsilon(q) = \partial$ (resp.~$p<_{\Omega} q$ and $\varepsilon(p) = \partial$ and $\varepsilon(q) = 1$).
\end{example}

\section{The GMT translations}\label{semantic environment}

In this section we give a brief overview of some highlights in the history of the G\"{o}del-McKinsey-Tarski translation, its extensions and variations and the uses to which they have been put. We then recall the technical details of the translation and how its is founded upon the interplay of persistent and arbitrary valuations in intuitionistic Kripke frames.

\subsection{Brief history}
\label{ssec:brief history}
The GMT translation originates in the work of G\"{o}del \cite{Godel:Interp} and its algebraic underpinnings were analysed by McKinsey and Tarski in \cite{mckinsey1944algebra, mckinsey1946closed}. In particular, in \cite{mckinsey1944algebra} develops the theory of closure algebras, i.e.\ S4-algebras, while \cite{mckinsey1946closed} shows that every Brouwerian algebra embeds as the subalgebra of closed subsets of some closure algebra. In \cite{McKinseyTarski:Translation} this analysis is used to show that the GMT translation and a number of variations are full and faithful. This result is extended by Dummett and Lemmon \cite{dummett1959modal} in 1959 to all intermediate logics. In 1967 Grzegorczyk \cite{grzegorczyk1967some} showed that Dummett and Lemmon's result also holds if one replaces normal extensions of S4 with normal extension of what is now known as Grzegorczyk's logic. In light these developments, Maksimova and Rybakov \cite{maksimova1974lattice} launched a systematic study of the relationship between the lattice of intermediate logics and that of normal extensions of S4.

In 1976 Blok \cite{blok1976varieties} and Esakia \cite{esakia1976modal} independently built on this work to establish an isomorphism, based the GMT translation, between the lattice of intermediate logics and the lattice of normal extensions of Grzegorczyk's logic.

Between 1989 and 1992, several theorems are proven by Zakharyaschev and Chagrov about the preservation under GMT-based translations of properties such as decidability, finite model property, Kripke and Hallden completeness, disjunction property, and compactness. For detailed surveys on this line of research, the reader is referred to \cite{chagrov1992modal} and \cite{wolter2014blok}.

The first extension of the GMT translation to modal expansions of intuitionistic logic is introduced by Fischer Servi \cite{fischerservi1977modal} in 1977. Between 1979 and 1984 Shehtman and Sotirov also published on extensions (cf.\ discussions in \cite{chagrov1992modal, wolter2014blok}).

In the mid 90s, building on the work of Fischer Servi and Shehtman, Wolter and Zakharyaschev \cite{WoZa98} use an extension of the GMT translation to prove the transfer of a number of results, including finite model property, canonicity, decidability, tabularity and Kripke completeness, for intuitionistic modal logic with box only. In Remark \ref{rmk: comparison canonicity} we will expand on the relationship of their canonicity results (cf.\ \cite[Theorem 12]{WoZa98}) with those of the present paper. In \cite{WoZa97} this line of work is extended to intuitionistic modal logics with box and diamond. Duality theory is developed and the transfer of decidability, finite model property and tabularity under a suitably extended GMT translation is established. Moreover, a Blok-Esakia theorem is proved in this setting.

This research programme is further pursued by Wolter \cite{wolter1998CoImplication} in the setting bi-intuitionistic modal logic, obtained by adding the left residual of the disjunction (also known as co-implication) to the language of intuitionistic modal logic. He develops duality theory for these logics, extends the GMT translation and established a Blok-Esakia theorem.  Recent developments include work by G.\ Bezhanishvili who considers expansions of Prior's MIPC with  universal modalities, extends the GMT translation and establishes a Blok-Esakia theorem.

As the outline above shows, the research program on the transfer of results via GMT translations includes many transfers of completeness and canonicity (the latter in the form of d-persistence) which are closely related to the focus of the present paper. However, there are very few transfer results which specifically concern Sahlqvist theory, and this for the obvious reason that the formulation of such results depends on the availability of an independent definition of Sahlqvist formulas for each setting of (modal expansions of) non-classical logics, and these definitions have not been introduced in any of these settings, neither together nor in isolation, until 2005, when Gehrke, Nagahashi and Venema \cite{GeNaVe05} introduced the notion of Sahlqvist inequalities in the language of Distributive Modal Logic (DML).\footnote
We refer to \cite{CoGhPa14, ConPal13} for a systematic comparison between \cite[Definition 3.4]{GeNaVe05} and the definition of Sahlqvist and inductive inequalities for normal DLE-languages (cf.~Definition \ref{Inducive:Ineq:Def}).} This definition made it possible to formulate the  Sahlqvist correspondence theorem for DML-inequalities (cf.~\cite[Theorem 3.7]{GeNaVe05}) and prove it via reduction to a suitable classical poly-modal logic using GMT translations.

We conclude this brief survey by mentioning a recent paper by van Benthem, N.\ Bezhanishvili and Holliday \cite{vBBeHo16} which studies a GMT-like translation from modal logic with possibility semantics into bi-modal logic. They prove that this translation transfers and reflects first-order correspondence,  but point out that it destroys the Sahlqvist shape of formulas in all but a few special cases.

\subsection{Semantic analysis}\label{ssec: sem analysis godel tarski}
In the present section we recall the definition of the GMT translation in its original setting, highlight its basic semantic underpinning as a toggle between persistent and non-persistent valuations on S4-frames. This analysis will be extended  to a uniform account of the GMT translation for arbitrary normal DLE-logics in the next section.

In what follows, for any partial order $(W,\leq)$, we let $w{\uparrow}: = \{v\in W\mid w\leq v\}$, $w{\downarrow}: = \{v\in W\mid w\geq v\}$ for every $w\in W$, and for every $X\subseteq W$, we let $X{\uparrow}: = \bigcup_{x\in X} x{\uparrow}$ and $X{\downarrow}: = \bigcup_{x\in X} x{\downarrow}$. {\em Up-sets} (resp.\ {\em down-sets}) of $(W, \leq)$ are subsets $X\subseteq W$ such that $X = X{\uparrow}$ (resp.\ $X = X{\downarrow}$). We denote by $\mathcal{P}(W)$ the Boolean algebra of subsets of $W$, and by $\mathcal{P}^{\uparrow}(W)$ (resp.\ $\mathcal{P}^{\downarrow}(W)$) the (bi-)Heyting algebra of up-sets (resp.\ down-sets) of $(W, \leq)$. Finally we let $X^c$ denote the relative complement $W\setminus X$ of every subset $X\subseteq W$.

Fix a denumerable set $\mathsf{Prop}$ of propositional variables. The language of intuitionistic logic over $\mathsf{Prop}$ is given by
\[\mathcal{L}_I\ni\phi:: = p\mid \bot\mid \top\mid \phi\wedge \phi\mid \phi\vee\phi\mid \phi\rightarrow \phi.\]
The language of the normal modal logic S4 over $\mathsf{Prop}$ is given by
\[\mathcal{L}_{S4\Box}\ni\alpha:: = p\mid \bot \mid \alpha\vee \alpha\mid\alpha\wedge \alpha \mid\neg\alpha\mid \Box_{\leq}\alpha.\]

The GMT translation is the map $\tau\colon \mathcal{L}_I\rightarrow \mathcal{L}_{S4\Box}$ defined by the following recursion:
\begin{center}
\begin{tabular}{r c l}
$\tau (p)$ &  = & $\Box_{\leq} p$\\
$\tau (\bot)$ &  = & $\bot$ \\
$\tau (\top)$ &  = & $\top$ \\
$\tau (\phi\wedge \psi)$ &  = & $\tau (\phi)\wedge \tau(\psi)$  \\
$\tau (\phi\vee \psi)$ &  = & $\tau (\phi)\vee \tau(\psi)$  \\
$\tau (\phi \rightarrow \psi)$ &  = & $\Box_{\leq}(\neg\tau (\phi)\vee \tau(\psi))$.  \\
\end{tabular}
\end{center}

Both intuitionistic and S4-formulas can be interpreted on partial orders $\mathbb{F}  = (W, \leq)$, as follows: an S4-model is a tuple $(\mathbb{F}, U)$ where $U: \mathsf{Prop}\to \mathcal{P}(W)$ is a valuation. The interpretation $\Vdash^*$ of S4-formulas on S4-models is defined recursively as follows: for an $w\in W$,
\begin{center}
\begin{tabular}{l l l}
$\mathbb{F}, w, U \Vdash^* p$ &$\quad$& iff $p\in U(p)$\\
$\mathbb{F}, w, U \Vdash^* \bot $ && never\\
$\mathbb{F}, w, U \Vdash^* \top $ && always\\
$\mathbb{F}, w, U \Vdash^* \alpha\wedge \beta$ &&iff $\ \mathbb{F}, w, U \Vdash^* \alpha\ $ and $\ \mathbb{F}, w, U \Vdash^* \beta$\\
$\mathbb{F}, w, U \Vdash^* \alpha\vee \beta$ &&iff $\ \mathbb{F}, w, U \Vdash^* \alpha\ $ or $\ \mathbb{F}, w, U \Vdash^* \beta$\\
$\mathbb{F}, w, U \Vdash^* \neg \alpha $ &&iff  $\ \mathbb{F}, w, U \not\Vdash^* \alpha\ $ \\
$\mathbb{F}, w, U \Vdash^* \Box_\leq\alpha$ && iff   $\ \mathbb{F}, v, U \Vdash^* \alpha\ $ for any $v\in w{\uparrow}$.
\end{tabular}
\end{center}
For any S4-formula $\alpha$ we let $\valb{\alpha}_U: = \{ w\mid \mathbb{F}, w, U\Vdash^*\alpha\}$. It is not difficult to verify that for every $\alpha\in \mathcal{L}_{S4}$ and any valuation $U$,
\begin{equation}\label{eq:extension of box}
\valb{\Box_\leq \alpha}_U = \valb{\alpha}_U^c{\downarrow}^c.
\end{equation}

An intuitionistic model is a tuple $(\mathbb{F}, V)$ where $V: \mathsf{Prop}\to \mathcal{P}^{\uparrow}(W)$ is a {\em persistent} valuation. The interpretation $\Vdash^*$ of S4-formulas on S4-models is defined recursively as follows: for an $w\in W$,
\begin{center}
\begin{tabular}{l l l}
$\mathbb{F}, w, V \Vdash p$ &$\quad$& iff $p\in V(p)$\\
$\mathbb{F}, w, V \Vdash \bot \qquad$ &$\quad$& never\\
$\mathbb{F}, w, V \Vdash \top \qquad$ &$\quad$& always\\
$\mathbb{F}, w, V \Vdash \phi\wedge \psi$ &$\quad$& iff $\ \mathbb{F}, w, V \Vdash \phi\ $ and $\ \mathbb{F}, w, V \Vdash \psi$\\
$\mathbb{F}, w, V \Vdash \phi\vee \psi$  &$\quad$& iff $\ \mathbb{F}, w, V \Vdash \phi\ $ or $\ \mathbb{F}, w, V \Vdash \psi$\\
$\mathbb{F}, w, V \Vdash \phi \rightarrow \psi$ &$\quad$& iff  either  $\ \mathbb{F}, v, V \not\Vdash \phi\ $ or  $\ \mathbb{F}, v, V \Vdash \psi$ for any $v\in w{\uparrow}$.\\
\end{tabular}
\end{center}
For any intuitionistic formula $\phi$ we let $\val{\phi}_V: = \{ w\mid \mathbb{F}, w, V\Vdash\phi\}$. It is not difficult to verify that for all $\phi, \psi\in \mathcal{L}_{I}$ and any persistent valuation $V$,
\begin{equation} \label{eq: extension of rightarrow}
\val{\phi\rightarrow \psi}_V = (\val{\phi}_V^c\cup \val{\psi}_V)^c{\downarrow}^c.
\end{equation}
Clearly, every persistent valuation $V$ on $\mathbb{F}$ is also a valuation on $\mathbb{F}$. Moreover, for every valuation $U$ on $\mathcal{F}$, the assignment mapping every $p\in \mathsf{Prop}$ to $U(p)^c{\downarrow}^c$ defines a persistent valuation $U^{\uparrow}$ on $\mathbb{F}$.
The main semantic property of the GMT translation is stated in the following well-known proposition:

\begin{prop}\label{fact: main property goedel transl}
For every intuitionistic formula $\phi$ and every partial order $\mathbb{F}  = (W, \leq)$,
\[\mathbb{F} \Vdash \phi \quad \mbox{ iff } \quad \mathbb{F} \Vdash^* \tau(\phi).\]
\end{prop}
\begin{proof}
If $\mathbb{F} \not\Vdash \phi$, then $\mathbb{F}, w, V \not\Vdash \phi$ for some persistent valuation $V$ and $w\in W$. That is, $w\notin \val{\phi}_V = \valb{ \tau(\phi)}_V$, the last identity holding by item 1 of Lemma \ref{lemma: main property goedel transl}. Hence, $\mathbb{F}, w, V\not\Vdash^*\tau(\phi)$, i.e.\
$\mathbb{F} \not\Vdash^* \tau(p)$. Conversely, if $\mathbb{F} \not\Vdash^* \tau(\phi)$, then $\mathbb{F}, w, U \not\Vdash \tau(\phi)$ for some valuation $U$ and $w\in W$. That is, $w\notin \valb{\tau(\phi)}_U =  \val{\phi}_{U^{\uparrow}}$, the last identity holding by item 2 of Lemma \ref{lemma: main property goedel transl}. Hence, $\mathbb{F}, w, U^{\uparrow}\not\Vdash \phi$, yielding $\mathbb{F} \not\Vdash \phi$.
\end{proof}

\begin{lemma}\label{lemma: main property goedel transl}
For every intuitionistic formula $\phi$ and every partial order $\mathbb{F}  = (W, \leq)$,
\begin{enumerate}
\item $\val{\phi}_V = \valb{\tau(\phi)}_V$ for every persistent valuation $V$ on $\mathbb{F}$;
\item $\valb{\tau(\phi)}_U = \val{\phi}_{U^{\uparrow}}$ for every valuation $U$ on $\mathbb{F}$.
\end{enumerate}
\end{lemma}
\begin{proof}
1. By induction on $\phi$. As for the base case, let $\phi: = p\in \mathsf{Prop}$. Then, for any persistent valuation $V$,
\begin{center}
\begin{tabular}{r c l l}
$\val{p}_V $&$=$&$V(p)$ & (def.\ of $\val{\cdot}_V$)\\
&$=$&$ V(p)^c{\downarrow}^c$ & ($V$ persistent)\\
&$=$&$\valb{ \Box_{\leq} p}_V$& (equation \eqref{eq:extension of box})\\
&$=$&$\valb{\tau(p)}_V$, & (def.\ of $\tau$)\\
\end{tabular}
 \end{center}
 as required. As for the inductive step, let $\phi: = \psi\rightarrow \chi$. Then, for any persistent valuation $V$,
\begin{center}
\begin{tabular}{r c l l}
$\val{\psi \rightarrow \chi}_V$&$=$&$(\val{\psi}_V^c \cup \val{\chi}_V)^c {\downarrow} ^c$& (equation \eqref{eq:extension of box})\\
&$=$&$(\valb{\tau(\psi)}_V^c \cup \valb{\tau(\chi)}_V)^c {\downarrow}^c$& (induction hypothesis)\\
&$=$&$\valb{\Box_\leq(\neg \tau(\psi)\vee \tau(\chi))}_V$& (equation \eqref{eq:extension of box}, def.\ of $\valb{\cdot}_V$)\\
&$=$&$\valb{\tau(\psi\rightarrow \chi)}_V,$ & (def.\ of $\tau$)\\
\end{tabular}
 \end{center}
 as required. The remaining cases are omitted.

2. By induction on $\phi$. As for the base case, let $\phi: = p\in \mathsf{Prop}$.  Then, for any valuation $U$,
\begin{center}
\begin{tabular}{r c l l}
$\valb{\tau(p)}_U$&$=$&$\valb{\Box_{\leq} p}_U$& (def.\ of $\tau$)\\
&$=$&$\valb{p}_U ^c{\downarrow}^c$ & (equation \eqref{eq:extension of box})\\
&$=$&$U(p)^c{\downarrow}^c$ & (def.\ of $\valb{\cdot}_U$)\\
&$=$&$\val{p}_{U^{\uparrow}}$, & (def.\ of $U^{\uparrow}$) \\
 \end{tabular}
 \end{center}
 as required.
As for the inductive step, let $\phi: = \psi\rightarrow \chi$. Then, for any valuation $U$,
\begin{center}
\begin{tabular}{r c l l}
$\valb{\tau(\psi\rightarrow \chi)}_U$&$=$&$\valb{\Box_{\leq} (\neg \tau(\psi)\vee \tau(\chi))}_U$ & (def.\ of $\tau$)\\
&$=$&$\valb{\neg \tau(\psi)\vee \tau(\chi)}_U ^c{\downarrow}^c$ & (equation \eqref{eq:extension of box})\\
&$=$&$(\valb{\tau(\psi)}_U^c\cup \valb{\tau(\chi)}_U) ^c{\downarrow}^c$ & (def.\ of $\valb{\cdot}_U$) \\
&$=$&$(\val{\psi}_{U^{\uparrow}}^c\cup \val{\chi}_{U^{\uparrow}}) ^c{\downarrow}^c$ & (induction hypothesis)\\
&$=$&$\val{\psi\rightarrow \chi}_{U^{\uparrow}}$, &  (equation \eqref{eq: extension of rightarrow}, $U^{\uparrow}$ persistent)\\
 \end{tabular}
 \end{center}
   as required.
The remaining cases are omitted.
\end{proof}

 Hence, the main semantic property of GMT translation, stated in Proposition \ref{fact: main property goedel transl}, can be understood in terms of the interplay between persistent and nonpersistent valuations, as captured in the above lemma. In the next section, we are going to establish a general template for this interplay and then apply it to the algebraic analysis of GMT translations in various  settings.

\section{Unifying analysis of GMT translations}\label{ssec:template}

In the present section, we  generalize the key mechanism captured in Section \ref{ssec: sem analysis godel tarski} and guaranteeing the preservation and reflection of validity under the GMT translation. Being able to identify this pattern in generality will make it possible to recognise this mechanism in several logical settings, as we do in the following section.

Let $\mathcal{L}_1$ and $\mathcal{L}_2$ be  propositional languages over a given set $X$, and let $\mathbb{A}$ and $\mathbb{B}$ be ordered $\mathcal{L}_1$- and $\mathcal{L}_2$-algebras respectively, such that an order-embedding
$e \colon \mathbb{A} \hookrightarrow \mathbb{B}$ exists. For each $V \in \mathbb{A}^X$ and $U \in \mathbb{B}^X$, let  $\val{\cdot}_V$ and $\valb{\cdot}_U$ denote their unique homomorphic extensions to $\mathcal{L}_1$ and $\mathcal{L}_2$ respectively. Clearly, $e \colon \mathbb{A} \hookrightarrow \mathbb{B}$ lifts to a map $\overline{e}: \mathbb{A}^X \to \mathbb{B}^X$ by the assignment $V\mapsto e\circ V$.
\begin{comment}
\[
e(a) \leq b \quad \mbox{ iff } \quad a \leq \iota(b).
\]
Then the adjunction $e \dashv \iota$ lifts to the adjunction $e \circ (-) \dashv \iota \circ (-)$ between the partially ordered sets of valuations over $\mathbb{A}$ and $\mathbb{B}$: $ e \circ (-) \colon \mathbb{A}^X \to \mathbb{B}^X$ and $\iota \circ (-) \colon \mathbb{B}^X \to \mathbb{A}^X.$ That is, for every $V \in \mathbb{A}^X$, every $U \in \mathbb{B}^X$ and every $x \in X$,
\[
e (V(x)) \leq U(x) \quad \mbox{ iff } \quad V(x) \leq \iota(U(x)).
\]
\marginnote{Conjecture: if the adjunction $e \dashv \iota$ is an interior operator adjunction, then it lifts to a corresponding interior operator adjunction $e \circ (-) \dashv \iota \circ (-)$.}
\end{comment}
\begin{prop}\label{prop: main prop of Godel tarski algebraically}
Let $\tau \colon \mathcal{L}_1 \to \mathcal{L}_2$ and  $r\colon \mathbb{B}^X\to \mathbb{A}^X$ be such that the following conditions hold for every $\phi \in \mathcal{L}_1$:
\begin{enumerate}
\item[(a)] $e(\val{ \phi}_V) = \valb{\tau(\phi)}_{\overline{e}(V)}$ for every $V \in \mathbb{A}^X$;
\item[(b)] $\valb{ \tau (\phi) }_U = e(\val{\phi}_{r(U)})$ for every $U \in \mathbb{B}^X$.
\end{enumerate}
Then, for all $\phi, \psi\in \mathcal{L}_1$,
\[
\mathbb{A} \models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models \tau(\phi)\leq \tau(\psi).
\]
\end{prop}
\begin{proof}
From left to right, suppose contrapositively that $(\mathbb{B},U) \not\models \tau(\phi)\leq \tau(\psi)$ for some $U \in \mathbb{B}^X$, that is, $\valb{\tau(\phi)}_U\not\leq \valb{\tau(\psi)}_U$.  By item (b) above,  this non-inequality is equivalent to $e(\val{\phi}_{r(U)})\not\leq e(\val{\psi}_{r(U)})$, which, by the monotonicity of $e$, implies that $\val{\phi}_{r(U)}\not\leq \val{\psi}_{r(U)}$, that is,  $(\mathbb{A}, r(U)) \not\models \phi\leq \psi$, as required. Conversely, if $(\mathbb{A},V) \not\models \phi\leq \psi$ for some $V \in \mathbb{A}^X$, then $\val{\phi}_{V}\not\leq \val{\psi}_{V}$, and hence, since  $e$ is an order-embedding and by item (a) above, $\valb{\tau(\phi)}_{\overline{e}(V)} = e(\val{\phi}_{V})\not\leq e(\val{\psi}_{V}) = \valb{\tau(\psi)}_{\overline{e}(V)}$, that is   $(\mathbb{B}, \overline{e}(V)) \not\models \tau(\phi)\leq \tau(\psi)$, as required.
\end{proof}
In the proof above we have only made use of the assumption that $e$ is an order-embedding, but have not needed to assume any property of $r$.
Moreover, the proposition above is independent of the logical/algebraic signature of choice, and hence can be used as a general template accounting for the main property of GMT translations. Finally, the proposition holds for {\em arbitrary} ordered algebras. This latter point is key to the treatment of Sahlqvist canonicity via translation.

\section{Instantiations of the general template for GMT translations}\label{sec:instantiations}

In the present section, we look into a family of GMT-type translations, defined for different logics, to which we  apply the template of Section \ref{ssec:template}. We organize these considerations into two subsections, in the first of which we treat the GMT translations for intuitionistic and co-intuitionistic logic and discuss how these extend to bi-intuitionistic logic. In the second subsection we consider parametrized versions of the GMT translation in the style of Gehrke, Nagahashi and Venema \cite{GeNaVe05} for normal modal expansions of bi-intuitionistic and DLE-logics.

\subsection{Non-parametric GMT translations}

As is well known, the semantic underpinnings of the GMT translations for intuitionistic and co-intuitionistic logic are the embeddings of Heyting algebras as the algebras of open elements of interior algebras and of Brouwerian algebras (aka co-Heyting algebras) as algebras of closed elements of closure algebras \cite{mckinsey1946closed}. In the following subsections, the existence of these embeddings will be used to satisfy the key assumptions of Section \ref{ssec:template}.

\subsubsection{Interior operator analysis of the GMT translation for intuitionistic logic}

As observed above, Proposition \ref{prop: main prop of Godel tarski algebraically} generalizes Proposition \ref{fact: main property goedel transl} in more than one way.  In the present subsection, we show that the GMT translation for intuitionistic logic verifies the conditions of Proposition \ref{prop: main prop of Godel tarski algebraically}. This is an alternative proof of the well-known fact that the GMT-translation is full and faithful, not only with respect to perfect algebras (dual to frames), but also with respect to general algebras. This fact is necessary for the proof of the transfer of Sahlqvist canonicity (cf.~Section \ref{sec:canonicity}).
  Towards this goal, we let $X: = \mathsf{Prop}$, $\mathcal{L}_1: = \mathcal{L}_I$, and $\mathcal{L}_2: = \mathcal{L}_{S4}$. Moreover, we let $\mathbb{A}$ be a  Heyting algebra,  and $\mathbb{B}$  a Boolean algebra  such that an order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is  also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$, and has  a right adjoint\footnote{That is, $e(a)\leq b$ iff $a\leq \iota(b)$ for every $a\in \mathbb{A}$ and $b\in \mathbb{B}$. By well known order-theoretic facts (cf.\ \cite{DaPr90}), $e\circ\iota$ is an {\em interior operator}, that is, for every $b, b'\in \mathbb{B}$, \begin{enumerate}
  \item[i1.] $(e\circ\iota)(b)\leq b$;
  \item[i2.] if $b\leq b'$ then $(e\circ\iota)(b)\leq (e\circ\iota)(b')$;
  \item[i3.] $(e\circ\iota)(b)\leq (e\circ\iota)((e\circ\iota)(b))$.
  \end{enumerate}Moreover, $e\circ\iota\circ e = e$ and $\iota = \iota\circ e \circ \iota$ (cf.\ \cite[Lemma 7.26]{DaPr90}).} $\iota\colon \mathbb{B}\to \mathbb{A}$ such that for all $a, b\in \mathbb{A}$,
  \begin{equation}
  \label{eq: rightarrow Rightarrow e and iota}
  a\rightarrow^\mathbb{A} b = \iota(\neg^\mathbb{B} e(a)\vee^\mathbb{B} e(b)).\end{equation}
   Then $\mathbb{B}$ can be endowed with a natural structure of Boolean algebra expansion (BAE) by defining $\Box^\mathbb{B}\colon \mathbb{B}\to \mathbb{B}$ by the assignment $b\mapsto (e\circ \iota)(b)$.
The following is a well known fact in  algebraic modal logic:
\begin{prop}\label{prop:BAE is s4}
The BAE $(\mathbb{B}, \Box^\mathbb{B})$, with $\Box^\mathbb{B}$ defined above, is  normal  and is also an S4-modal algebra.
\end{prop}
\begin{proof}
The fact that $\Box^\mathbb{B}$ preserves finite (hence empty) meets readily follows from the fact that $\iota$ is a right adjoint, and hence preserves existing (thus all finite) meets of $\mathbb{B}$, and $e$ is a lattice homomorphism. For every $b\in \mathbb{B}$, $\iota(b)\leq \iota(b)$ implies that $\Box^\mathbb{B} b = e(\iota(b))\leq b$, which proves (T). For every $b\in \mathbb{B}$, $e(\iota(b))\leq e(\iota(b))$ implies that $\iota(b)\leq \iota(e(\iota(b)))$ and hence $\Box^\mathbb{B} b = e(\iota(b))\leq e(\iota(e(\iota(b)))) = (e\circ\iota)((e\circ\iota)(b)) = \Box^\mathbb{B}\Box^\mathbb{B} b$, which proves K4.
\end{proof}
Finally, we let $r: \mathbb{B}^X\to \mathbb{A}^X$ be defined by the assignment $U\mapsto (\iota\circ U)$.

\begin{prop}
\label{prop:tau verifies a and b}
Let $\mathbb{A}$, $\mathbb{B}$, $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ and $r\colon \mathbb{B}^X\to \mathbb{A}^X$ be as above.\footnote{The assumption that  $e$ is a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ is needed for the inductive steps relative to $\bot, \top, \wedge, \vee$  in the proof this proposition, while condition \eqref{eq: rightarrow Rightarrow e and iota} is needed for the step relative to $\rightarrow$.} Then the GMT translation $\tau$ satisfies conditions (a) and (b) of Proposition \ref{prop: main prop of Godel tarski algebraically} for any formula $\phi\in \mathcal{L}_I$.
\end{prop}
\begin{proof}
By induction on $\phi$. As for the base case, let $\phi: = p\in \mathsf{Prop}$. Then, for any $U\in \mathbb{B}^X$ and   $V\in\mathbb{A}^X$,
\begin{center}
\begin{tabular}{r c l c r c l l}
$e(\val{p}_{r(U)})$ & = & $e((\iota\circ U)(p))$ &\quad\quad &$\valb{\tau(p)}_{\overline{e}(V)}$ & = & $\valb{\Box_{\leq} p}_{\overline{e}(V)}$ \\
& = & $(e\circ \iota)(\valb{p}_U)$ &assoc.\ of $\circ$ && = & $\Box^\mathbb{B}\valb{p}_{\overline{e}(V)}$ \\
& = & $\Box^\mathbb{B}\valb{p}_U$ &\quad\quad && = & $\Box^\mathbb{B}((e\circ V)(p))$ \\
& = & $\valb{\Box_{\leq} p}_U$ &\quad\quad && = & $(e\circ \iota)((e\circ V)(p))$ \\
& = & $\valb{\tau( p)}_U$. &\quad\quad && = & $e((\iota \circ e)(V(p)))$ & assoc.\ of $\circ$\\
&&&&& = & $e(V(p))$ & $e\circ(\iota\circ e) =e$\\
&&&&& = & $e(\val{p}_V)$, \\
\end{tabular}
\end{center}
which proves  the base cases of  (b) and (a) respectively. As for the inductive step, let $\phi: = \psi\rightarrow \chi$. Then, for any $U\in \mathbb{B}^X$ and   $V\in\mathbb{A}^X$,
\begin{center}
\begin{tabular}{r c l  l}
$e(\val{\psi\rightarrow \chi}_{r(U)})$ & = & $e(\val{\psi}_{r(U)}\rightarrow^\mathbb{A} \val{ \chi}_{r(U)})$ \\
& = & $e(\iota(\neg^\mathbb{B} e(\val{\psi}_{r(U)})\vee^\mathbb{B} e(\val{ \chi}_{r(U)})))$ & assumption \eqref{eq: rightarrow Rightarrow e and iota} \\
& = & $e(\iota(\neg^\mathbb{B}\valb{\tau(\psi)}_{U}\vee^\mathbb{B} \valb{\tau(\chi)}_{U}))$ & (induction hypothesis)\\
& = & $(e\circ \iota)(\neg^\mathbb{B}\valb{\tau(\psi)}_{U}\vee^\mathbb{B} \valb{\tau(\chi)}_{U})$ & \\
& = & $\Box^\mathbb{B}(\neg^\mathbb{B} \valb{\tau(\psi)}_{U}\vee^\mathbb{B} \valb{ \tau(\chi)}_{U})$ & \\
& = & $\valb{\Box_\leq(\neg \tau(\psi)\vee\tau(\chi))}_{U}$ & \\
& = & $\valb{\tau(\psi\rightarrow\chi)}_{U}$. & \\
\end{tabular}
\end{center}

\begin{center}
\begin{tabular}{r c l  l}
$e(\val{\psi\rightarrow \chi}_{V})$ & = & $e(\val{\psi}_{V}\rightarrow^\mathbb{A} \val{ \chi}_{V})$ \\
& = & $e(\iota(\neg^\mathbb{B} e(\val{\psi}_{V})\vee^\mathbb{B} e(\val{ \chi}_{V})))$ & assumption \eqref{eq: rightarrow Rightarrow e and iota} \\
& = & $e(\iota(\neg^\mathbb{B} \valb{\tau(\psi)}_{\overline{e}(V)}\vee^\mathbb{B} \valb{ \tau(\chi)}_{\overline{e}(V)}))$ & (induction hypothesis)\\
& = & $(e\circ \iota)(\neg^\mathbb{B} \valb{\tau(\psi)}_{\overline{e}(V)}\vee^\mathbb{B} \valb{ \tau(\chi)}_{\overline{e}(V)})$ & \\
& = & $\Box^\mathbb{B}(\neg^\mathbb{B} \valb{\tau(\psi)}_{\overline{e}(V)}\vee^\mathbb{B} \valb{ \tau(\chi)}_{\overline{e}(V)})$ & \\
& = & $\valb{\Box_\leq(\tau(\psi)\vee\tau(\chi))}_{\overline{e}(V)}$ & \\
& = & $\valb{\tau(\psi\rightarrow\chi)}_{\overline{e}(V)}$. & \\
\end{tabular}
\end{center}
The remaining cases are straightforward, and are left to the reader.
\end{proof}

The following strengthening of Proposition \ref{fact: main property goedel transl} immediately follows from Propositions \ref{prop: main prop of Godel tarski algebraically} and \ref{prop:tau verifies a and b}:
\begin{cor}
Let $\mathbb{A}$ be a Heyting algebra and $\mathbb{B}$ a Boolean algebra such that $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ and $\iota\colon \mathbb{B}\to \mathbb{A}$ exist as above. Then for all intuitionistic formulas $\phi$ and $\psi$,
\[
\mathbb{A} \models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models \tau(\phi)\leq \tau(\psi),
\]
where $\tau$ is the GMT translation.
\end{cor}

We conclude this subsection by showing that
the required embedding of Heyting algebras into Boolean algebras exists. This well known fact appears in its order-dual version already in \cite[Theorem 1.15]{mckinsey1946closed}, where is shown in a purely algebraic way. We give an alternative proof, based on very well known duality-theoretic facts.
The format of the statement is different from the dual of \cite[Theorem 1.15]{mckinsey1946closed} both because it is in the form required by Proposition \ref{prop: main prop of Godel tarski algebraically}, and also because it highlights that the embedding lifts to the canonical extensions of the algebras involved, where it acquires additional properties. This  is relevant to the analysis of canonicity via translation in Section \ref{sec:canonicity}.

\begin{prop}\label{prop:existence of algebras and adjoints:Heyting}
For every Heyting algebra $\mathbb{A}$, there exists a Boolean algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ and has a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ verifying condition \eqref{eq: rightarrow Rightarrow e and iota}. Finally, these facts lift to the canonical extensions of $\mathbb{A}$ and $\mathbb{B}$ as in the following diagram:
\begin{center}

\begin{tikzpicture}[node/.style={circle, draw, fill=black}, scale=1]

\node (A) at (-1.5,-1.5) {$\mathbb{A}$};
\node (A delta) at (-1.5,1.5) {$\mathbb{A}^{\delta}$};
\node (B) at (1.5,-1.5) {$\mathbb{B}$};
\node (B delta) at (1.5,1.5) {$\mathbb{B}^{\delta}$};

\draw [right hook->] (A) to  (A delta);
\draw [right hook->] (B)  to (B delta);
\draw [right hook->] (A)  to node[below] {$e$}  (B);
\draw [right hook->] (A delta)  to node[below] {$e^{\delta}$}  (B delta);

\draw [->] (B delta) to [out=135,in=45, looseness=0.5]  node[below] {\rotatebox[origin=c]{270}{$\vdash$}} node[above] {$\iota^{\pi}$}  (A delta);
\draw [->] (B) to [out=135,in=45, looseness=0.5]  node[below] {\rotatebox[origin=c]{270}{$\vdash$}} node[above] {$\iota$}  (A);

\draw [->] (B delta) to [out=225,in=-45, looseness=1]  node[above] {\rotatebox[origin=c]{270}{$\vdash$}} node[below] {$c$}  (A delta);
\end{tikzpicture}
\end{center}
\end{prop}

\begin{proof}
Via  Esakia duality \cite{Es75}, the Heyting algebra $\mathbb{A}$ can be identified  with the algebra of clopen up-sets of its associated Esakia space $\mathbb{X}_\mathbb{A}$, which is a Priestley space, hence a Stone space. Let $\mathbb{B}$ be the Boolean algebra of the clopen sub{\em sets} of $\mathbb{X}_\mathbb{A}$. Since any clopen up-set is in particular a clopen subset,  a natural order embedding $e: \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is also a lattice homomorphism between $\mathbb{A}$ and $\mathbb{B}$. This shows the first part of the claim.

As to the second part, notice that Esakia spaces are Priestley spaces in which the downward-closure of a clopen set is a clopen set.

Therefore, we can define the map  $\iota\colon \mathbb{B}\to \mathbb{A}$ by the assignment $b\mapsto \neg((\neg b){\downarrow})$ where $b$ is identified with its corresponding clopen set in $\mathbb{X}_\mathbb{A}$, $\neg b$ is identified with the relative complement of the clopen set $b$, and $(\neg b){\downarrow}$ is defined using the order in $\mathbb{X}_\mathbb{A}$. It can be readily verified that $\iota$ is the right adjoint of $e$ and that moreover  condition \eqref{eq: rightarrow Rightarrow e and iota} holds.

Finally, $e:\mathbb{A}\rightarrow\mathbb{B}$ being also a homomorphism between the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ implies that $e$ is smooth and its canonical extension $e^\delta\colon \mathbb{A}^{\delta}\to \mathbb{B}^{\delta}$, besides being an order-embedding, is a complete homomorphism between the lattice reducts of $\mathbb{A}^{\delta}$ and $\mathbb{B}^{\delta}$ (cf.\  \cite[Corollary 4.8]{GeHa01}), and hence is endowed with both a left and a right adjoint. Furthermore, the right adjoint of $e^\delta$ coincides with $\iota^\pi$ (cf.\  \cite[Proposition 4.2]{GePr07}). Hence, $\mathbb{B}^{\delta}$ can be endowed with a natural structure of S4 bi-modal algebra by defining $\Box_{\leq}^{\mathbb{B}^{\delta}}\colon \mathbb{B}^{\delta}\to \mathbb{B}^{\delta}$ by the assignment $u\mapsto (e^\delta\circ \iota^\pi)(u)$, and $\Diamond_{\geq}^{\mathbb{B}^{\delta}}\colon \mathbb{B}^{\delta}\to \mathbb{B}^{\delta}$ by the assignment $u\mapsto (e^\delta\circ c)(u)$.
\end{proof}

\begin{comment}
\begin{prop}
For any formula $\phi$ in $\mathcal{L}_1$, $ U \colon X \to \mathbb{B}$,
\[
\val{ \tau (\phi)}_U = \val{\Box \tau (\phi)}_U.
\]
\end{prop}
\begin{proof}
By induction on $\phi$.
The proposition is proved for atomic formulas. It is easy to show the result for $ \top, \bot $ and $\wedge$.
\begin{itemize}
\item \begin{align*}
\val{\Box ( \tau(\phi) \vee \tau(\psi))}_U & \leq \val{\tau(\phi) \vee \tau(\psi)} &\text{ because } \Box x
\leq x,\\
& = \val{\Box \tau (\phi) \vee \Box \tau (\psi)}_U &\text{ by induction hypothesis,}\\
& \leq \val{\Box (\tau (\phi) \vee \tau(\psi))}_U &\text{ by monotonicity of } \Box,\\
& = \val{\Box ( \tau (\phi \vee \psi))}
\end{align*}
\item
\begin{align*}
\tau (\phi \rightarrow \psi) & = \Box (\tau (\phi) \rightsquigarrow \tau(\psi)) & \text{ by definition of } \tau,\\
\Box \tau (\phi \rightarrow \psi)& = \Box (\Box (\tau (\phi) \rightsquigarrow \tau(\psi))) & \text{ and the monotonicity of } \Box \text{ proves the result.}
\end{align*}
\end{itemize}
\end{proof}
\end{comment}

\subsubsection{The GMT translation for co-intuitionistic logic}
\label{ssec: sem analysis co-godel tarski}

In the present subsection, we  show that the GMT translation for co-intuitionistic logic (which we will sometimes refer to as the co-GMT translation) verifies the conditions of Proposition \ref{prop: main prop of Godel tarski algebraically}. Our presentation is a straightforward dualization of the previous subsection. We include it for the sake of completeness and for introducing some notation.   Semantically, this dualization involves replacing Heyting algebras with co-Heyting algebras (aka Brouwerian algebras cf.~\cite{mckinsey1946closed}), and interior algebras (aka S4 algebras with box) with closure algebras (aka S4 algebras with diamond).

Fix a denumerable set $\mathsf{Prop}$ of propositional variables. The language of co-intuitionistic logic over $\mathsf{Prop}$ is given by
\[\mathcal{L}_C\ni\phi:: = p\mid \bot\mid \top\mid \phi\wedge \phi\mid \phi\vee\phi\mid \phi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \phi.\]
The target language for translating co-intuitionistic logic is that of the normal modal logic S4$\Diamond$ over $\mathsf{Prop}$, given by
\[\mathcal{L}_{S4\Diamond}\ni\alpha:: = p\mid \bot \mid \alpha\vee \alpha\mid\alpha\wedge \alpha \mid\neg\alpha\mid \Diamond_{\geq}\alpha.\]
Just like intuitionistic logic, formulas of co-intuitionistic logic can be interpreted on partial orders $\mathbb{F} = (W,\leq)$ with persistent valuations. Here we only report on the interpretation of $\Diamond_{\geq}$-formulas in $\mathcal{L}_{S4\Diamond}$ and  $\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}$-formulas in $\mathcal{L}_C$:
\begin{center}
\begin{tabular}{l c l}
$\mathbb{F}, w, U \Vdash^* \Diamond_{\geq}\phi$ &$\quad$& iff   $\ \mathbb{F}, v, U \Vdash^* \phi\ $ for some $v\in w{\downarrow}$.\\
$\mathbb{F}, w, V \Vdash \phi \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \psi$ &$\quad$& iff    $\ \mathbb{F}, v, V \not\Vdash \phi\ $ and  $\ \mathbb{F}, v, V \Vdash \psi$ for some $v\in w{\downarrow}$.\\
\end{tabular}
\end{center}
The language $\mathcal{L}_C$ is naturally interpreted in co-Heyting algebras. The connective $\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}$ is interpreted as the left residual of $\vee$.
The co-GMT translation is the map $\sigma\colon \mathcal{L}_C\rightarrow \mathcal{L}_{S4\Diamond}$ defined by the following recursion:
\begin{center}
\begin{tabular}{r c l}
$\sigma (p)$ &  = & $\Diamond_{\geq} p$\\
$\sigma (\bot)$ &  = & $\bot$ \\
$\sigma (\top)$ &  = & $\top$ \\
$\sigma (\phi\wedge \psi)$ &  = & $\sigma (\phi)\wedge \sigma(\psi)$  \\
$\sigma (\phi\vee \psi)$ &  = & $\sigma(\phi)\vee \sigma(\psi)$  \\
$\sigma (\phi \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \psi)$ &  = & $\Diamond_{\geq}(\neg\sigma (\phi) \wedge \sigma(\psi))$  \\
\end{tabular}
\end{center}

\begin{comment}
The language of co-intuitionistic logic is given by
\[\mathcal{L}_C\ni\phi:: = p\mid \bot\mid \top\mid \phi\wedge \phi\mid \psi\vee\psi\mid \phi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \phi\]
The language of the normal modal logic S4 is alternatively given by\marginnote{this we probably need to explain better}
\[\mathcal{L}_{S4\Diamond}\ni\alpha:: = p\mid \bot \mid \alpha\vee \alpha\mid \alpha\wedge \alpha\mid \alpha- \alpha\mid \neg\alpha\mid \Diamond_{\geq}\alpha\]
where $\alpha - \beta$ is equivalent to $\alpha \wedge \neg \beta$. The co-GMT translation is the map $\sigma\colon \mathcal{L}_C\rightarrow \mathcal{L}_{S4\Diamond}$ defined by the following recursion:
\begin{center}
\begin{tabular}{r c l}
$\sigma (p)$ &  = & $\Diamond_{\geq} p$\\
$\sigma (\bot)$ &  = & $\bot$ \\
$\sigma (\top)$ &  = & $\top$ \\
$\sigma (\phi\wedge \psi)$ &  = & $\sigma (\phi)\wedge \sigma(\psi)$  \\
$\sigma (\phi\vee \psi)$ &  = & $\sigma(\phi)\vee \sigma(\psi)$  \\
$\sigma (\phi \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \psi)$ &  = & $\Diamond_{\geq}(\sigma (\psi) - \sigma(\phi))$  \\
\end{tabular}
\end{center}
The dual account of the GMT translation applies to the {\em co-implication}  (or {\em subtraction}) operation $\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}$ in co-intuitionistic logic.\marginnote{This needs to be defined. Essentially it is the BDL logic plus $\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}$, axiomatized to be the left residual of $\vee$.}
Let us start by recalling the definition of the interpretation of $\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}$ on S4 Kripke models $\mathbb{M}=(\mathbb{F}, V)$, where $\mathbb{F}= (W,\leq)$ is a partially ordered set, and $V\colon \mathsf{Prop}\to \mathcal{P}^{\uparrow}(W)$ is a {\em persistent} valuation:
\[
\mathbb{M},w \Vdash p \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} q \quad \mbox{ iff } \quad \mbox{ there exists some } v \in W \mbox{ s.t.\ } v \leq w \mbox{ and } \mathbb{M}, v \Vdash q \mbox{ and } \mathbb{M}, v \not\Vdash p
\]

This translates on the complex algebra of $\mathbb{F}$ as the following defining clause for the corresponding extension map
\[
\val{p \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} q}_V := ( \val{p}_V^c \cap \val{q}_V){\uparrow} =  \langle\geq\rangle(\val{q}_V - \val{p}_V),
\]
where $-$ denotes the semantic interpretation of the Boolean subtraction.

Observe that $V$ being persistent implies that the following chain of identities holds for every $p$ in $\mathsf{Prop}$:
\begin{equation}\label{eq:cofrominttoboolp}
\val{\Diamond_{\geq} p}_V = \val{p}_V{\uparrow} =\val{p}_V
\end{equation}
Hence we can prolong the first chain of identities as follows:

\begin{equation}\label{eq:cofrominttobool}
\val{p \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} q}_V :=  \langle\geq\rangle(\val{q}_V - \val{p}_V) = \langle\geq\rangle(\langle\geq\rangle \val{q}_V - \langle\geq\rangle\val{p}_V) .
\end{equation}

The chain of identities above provides the first half of the semantic justification for the definition of the following clause of the {\em co-GMT translation}:
\[
\sigma (p \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} q):= \Diamond_{\geq}(\Diamond_{\geq} q - \Diamond_{\geq} p).
\]
The second half is provided as follows: consider the frame $\mathbb{F}$ with a non persistent valuation $U$. A persistent valuation $^{\uparrow}U$ \marginnote{the notation $^{\uparrow}U$ might not be as brilliant as I initially thought...} can be associated with $U$ defined by the assignment $p \mapsto U(p){\uparrow}$.

Then clearly, for every $p \in \mathsf{Prop}$,
\begin{equation}\label{eq:cofrombooltointp}
\val{p}_{^{\uparrow}U} =\ ^{\uparrow}\!U (p) = U(p){\uparrow}= \val{\Diamond_{\geq}p}_U.
\end{equation}

Moreover,
\begin{align}\label{eq:cofrombooltoiint}
\begin{split}
\val{p \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} q}_{^{\uparrow}U}
& = (^{\uparrow}\!U (q) \cap\  ^{\uparrow}\!U(p)^c  ) {\uparrow}\\
&= (U(q) {\uparrow} \cap U(p){\uparrow}^c){\uparrow}\\
& = \val{\Diamond_{\geq}(\Diamond_{\geq} q - \Diamond_{\geq} p )}_U.
\end{split}
\end{align}

The identities \eqref{eq:cofrominttoboolp}, \eqref{eq:cofrominttobool}, \eqref{eq:cofrombooltointp} and \eqref{eq:cofrombooltoiint}  provide the base case and the crucial inductive steps in the proof of the following fact:
\begin{fact}\label{fact: main property cogoedel transl}
For every co-intuitionistic formula $\phi$ and every S4 Kripke frame $\mathbb{F} $,
\[
\mathbb{F} \Vdash \phi \quad \mbox{ iff } \quad \mathbb{F} \Vdash^* \sigma(\phi),
\]
where $\Vdash$ and $\Vdash^*$ respectively denote the (co-)intuitionistic and classical satisfaction relations on $\mathbb{F}$.
\end{fact}

Key to the result above is the interplay between persistent and nonpersistent valuations. In the next section we are going to analyze this interplay more in general and abstractly in the framework of closure operators.

\subsubsection{Closure operator analysis}
\begin{comment} Let $\mathcal{L}_1$ and $\mathcal{L}_2$ be  propositional languages over the set $X$, and let $\mathbb{A}$ and $\mathbb{B}$ be ordered $\mathcal{L}_1$- and $\mathcal{L}_2$-  algebras, respectively, such that an order-embedding
$e \colon \mathbb{A} \hookrightarrow \mathbb{B}$ exists.

That is, for all $a \in \mathbb{A} $ and $b \in \mathbb{B}$,
\[
c(b)\leq a  \quad \mbox{ iff } \quad b \leq e(a).
\]
Then the adjunction $c \dashv e$ lifts to the adjunction $c \circ (-)\dashv e \circ (-) $ between the partially ordered sets of valuations over $\mathbb{A}$ and $\mathbb{B}$: $ e \circ (-) \colon \mathbb{A}^X \to \mathbb{B}^X$ and $c \circ (-) \colon \mathbb{B}^X \to \mathbb{A}^X.$ That is, for every $V \in \mathbb{A}^X$, every $U \in \mathbb{B}^X$ and every $x \in X$,
\[
c(U(x))\leq V(x) \quad \mbox{ iff } \quad   U(x)\leq e (V(x)).
\]
\marginnote{Conjecture: if the adjunction $c \dashv e$ is a closure operator adjunction, then it lifts to a corresponding interior operator adjunction $c \circ (-) \dashv e \circ (-)$.}
\begin{prop}\label{prop: main prop of coGodel tarski algebraically}
Let $\sigma \colon \mathcal{L}_1 \to \mathcal{L}_2$ be a map such that the following conditions hold for every $\phi \in \mathcal{L}_1$, any $V \in \mathbb{A}^X$ and any $U \in \mathbb{B}^X$:

\begin{enumerate}
\item[(c)] $e(\val{ \phi}_V) = \val{\sigma(\phi)}_{e \circ V}$
\item[(d)] $\val{ \sigma (\phi) }_U = e(\val{\phi}_{c \circ U})$.
\end{enumerate}
Then
\[
\mathbb{A} \models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models \sigma(\phi)\leq \sigma(\psi).
\]
\end{prop}\marginnote{since we are not using any property of $c$, this proposition is probably redundant and can be removed (we use only Prop \ref{prop: main prop of Godel tarski algebraically})}
\begin{proof}
From left to right, suppose contrapositively that $(\mathbb{B},U) \not\models \sigma(\phi)\leq \sigma(\psi)$ for some $U \in \mathbb{B}^X$, that is, $\val{\sigma(\phi)}_U\not\subseteq \val{\sigma(\psi)}_U$.  By item (d) above,  this non-inclusion is equivalent to $e(\val{\phi}_{c\circ U})\not\subseteq e(\val{\psi}_{c\circ U})$, which, by the monotonicity of $e$, implies that $\val{\phi}_{c\circ U}\not\subseteq \val{\psi}_{c\circ U}$, that is,  $(\mathbb{A}, c \circ U) \not\models \phi\leq \psi$, as required. Conversely, if $(\mathbb{A},V) \not\models \phi\leq \psi$ for some $V \in \mathbb{A}^X$, then $\val{\phi}_{V}\not\subseteq \val{\psi}_{V}$, and hence, since $e$ is an order-embedding and item (c) above, $\val{\sigma(\phi)}_{e \circ V} = e(\val{\phi}_{V})\not\subseteq e(\val{\psi}_{V}) = \val{\sigma(\psi)}_{e \circ V}$, that is   $(\mathbb{B}, e \circ V) \not\models \sigma(\phi)\leq \sigma(\psi)$, as required.
\end{proof}
Notice that in the proof above we have only made use of the assumption that $e$ is an order-embedding, but  not of  $e$ and $c$ being adjoints.

Notice also that the proposition above is independent of the logical/algebraic signature of choice.
\end{comment}

Next, we show that Proposition \ref{prop: main prop of Godel tarski algebraically} applies to the co-GMT translation.
We let $X: = \mathsf{Prop}$, $\mathcal{L}_1: = \mathcal{L}_C$, and $\mathcal{L}_2: = \mathcal{L}_{S4\Diamond}$. Moreover, we let $\mathbb{A}$ be a  co-Heyting algebra,  and $\mathbb{B}$  a Boolean algebra  such that an order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is  also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$, and has  a left adjoint\footnote{That is, $c(b)\leq a$ iff $b\leq e(a)$ for every $a\in \mathbb{A}$ and $b\in \mathbb{B}$. By well known order-theoretic facts (cf.\ \cite{DaPr90}), $e\circ c$ is an {\em interior operator}, that is, for every $b, b'\in \mathbb{B}$, \begin{enumerate}
  \item[c1.] $b\leq (e\circ c)(b)$;
  \item[c2.] if $b\leq b'$ then $(e\circ c)(b)\leq (e\circ c)(b')$;
  \item[c3.] $(e\circ c)((e\circ c)(b))\leq (e\circ c)(b)$.
  \end{enumerate}Moreover, $e\circ c\circ e = e$ and $c = c\circ e \circ c$ (cf.\ \cite[Lemma 7.26]{DaPr90}).} $c\colon \mathbb{B}\to \mathbb{A}$ such that for all $a, b\in \mathbb{A}$,
  \begin{equation}
  \label{eq: pdra minus e and c}
  a\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}^\mathbb{A} b = c(\neg^\mathbb{B} e(a) \wedge^\mathbb{B} e(b)).\end{equation}
   Then $\mathbb{B}$ can be endowed with a natural structure of Boolean algebra expansion (BAE) by defining $\Diamond^\mathbb{B}\colon \mathbb{B}\to \mathbb{B}$ by the assignment $b\mapsto (e\circ c)(b)$.
The following is the dual of Proposition \ref{prop:BAE is s4} and its proof is omitted.
\begin{prop}\label{prop:BAE dia is s4}
The BAE $(\mathbb{B}, \Diamond^\mathbb{B})$, with $\Diamond^\mathbb{B}$ defined above, is  normal  and is also an $S4\Diamond$-modal algebra.
\end{prop}
Finally, we let $r: \mathbb{B}^X\to \mathbb{A}^X$ be defined by the assignment $U\mapsto (c\circ U)$. The proof of the following proposition is similar to that of Proposition \ref{prop:tau verifies a and b}, and its proof is omitted.

\begin{prop}
\label{prop:sigma verifies a and b}
Let $\mathbb{A}$, $\mathbb{B}$, $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ and $r\colon \mathbb{B}^X\to \mathbb{A}^X$ be as above.\footnote{The assumption that  $e$ is a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ is needed for the inductive steps relative to $\bot, \top, \wedge, \vee$  in the proof this proposition, while condition \eqref{eq: pdra minus e and c} is needed for the step relative to $\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}$.} Then the co-GMT translation $\sigma$ satisfies conditions (a) and (b) of Proposition \ref{prop: main prop of Godel tarski algebraically} for any formula $\phi\in \mathcal{L}_C$.
\end{prop}

The following corollary immediately follows from Propositions \ref{prop: main prop of Godel tarski algebraically} and \ref{prop:sigma verifies a and b}:
\begin{cor}\label{cor:main property sigma}
Let $\mathbb{A}$ be a co-Heyting algebra and $\mathbb{B}$ a Boolean algebra such that an order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is  a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$, and has  a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ such that condition \eqref{eq: pdra minus e and c} holds for all $a, b\in \mathbb{A}$. Then for all $\phi,\psi\in \mathcal{L}_C$,
\[
\mathbb{A} \models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models \sigma(\phi)\leq \sigma(\psi),
\]
where $\sigma$ is the co-GMT translation.
\end{cor}

As in the previous subsection, we conclude by giving a version of \cite[Theorem 1.15]{mckinsey1946closed} which we need to instantiate Proposition \ref{prop: main prop of Godel tarski algebraically} and for the analysis of canonicity via translation in Section \ref{sec:canonicity}. The proof is dual to that of Proposition \ref{prop:existence of algebras and adjoints:Heyting}.

\begin{prop}\label{prop:existence of algebras and adjoints:coHeyting}
For every co-Heyting algebra $\mathbb{A}$, there exists a Boolean algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ which is  a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$, and has a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ verifying condition \eqref{eq: pdra minus e and c}. Finally, these facts lift to the canonical extensions of $\mathbb{A}$ and $\mathbb{B}$ as in the following diagram:
\begin{center}
\begin{tikzpicture}[node/.style={circle, draw, fill=black}, scale=1]

\node (A) at (-1.5,-1.5) {$\mathbb{A}$};
\node (A delta) at (-1.5,1.5) {$\mathbb{A}^{\delta}$};
\node (B) at (1.5,-1.5) {$\mathbb{B}$};
\node (B delta) at (1.5,1.5) {$\mathbb{B}^{\delta}$};

\draw [right hook->] (A) to  (A delta);
\draw [right hook->] (B)  to (B delta);
\draw [right hook->] (A)  to node[above] {$e$}  (B);
\draw [right hook->] (A delta)  to node[above] {$e^{\delta}$}  (B delta);

\draw [->] (B delta) to [out=225,in=-45, looseness=0.5]  node[above] {\rotatebox[origin=c]{270}{$\vdash$}} node[below] {$c^{\sigma}$}  (A delta);
\draw [->] (B) to [out=225,in=-45, looseness=0.5]  node[above] {\rotatebox[origin=c]{270}{$\vdash$}} node[below] {$c$}  (A);
\draw [->] (B delta) to [out=135,in=45, looseness=1]  node[below] {\rotatebox[origin=c]{270}{$\vdash$}} node[above] {$\iota$}  (A delta);
\end{tikzpicture}
\end{center}
\end{prop}

\begin{comment}
+++++++++++++++

  Let $\mathbb{A}$ be a  co-Heyting algebra  and $\mathbb{B}$ be a Boolean algebra  such that $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ is an order-embedding and a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$. \marginnote{mention somewhere that these extra assumptions on $e$ are needed for the $\bot, \top, \wedge, \vee$ steps in the proof of proposition \ref{prop:tau verifies a and b}.  Notice that \eqref{eq: pdra minus e and c} is exactly the commutativity of the diagram  Zhiguang and I were discussing today! :-)}
  If  $e$ has  a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ such that for all $a, b\in \mathbb{A}$,
  \begin{equation}
  \label{eq: pdra minus e and c}
  a\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}^\mathbb{A} b = c(e(b) -^\mathbb{B} e(a))\end{equation}
   then $\mathbb{B}$ can be endowed with a natural structure of modal S4-algebra by defining $\Diamond^\mathbb{B}\colon \mathbb{B}\to \mathbb{B}$ by the assignment $b\mapsto (e\circ c)(b)$.
 \begin{fact}
 The BAE $(\mathbb{B}, \Diamond^\mathbb{B})$, with $\Diamond^\mathbb{B}$  defined as above, is  normal  and is also an S4-modal algebra.
 \end{fact}\marginnote{add sketch of proof of this fact, namely: $\Diamond \bot = \bot, \Diamond (x \vee y) = \Diamond x \vee \Diamond y, x \leq \Diamond x, \Diamond \Diamond x \leq \Diamond x $}
\begin{prop}
\label{prop:sigma verifies a and b}
Let $\mathbb{A}$, $\mathbb{B}$, $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ and $r = c\colon \mathbb{B}\to \mathbb{A}$ be as above. Then the co-GMT translation $\sigma$ satisfies conditions (a) and (b) of Proposition \ref{prop: main prop of Godel tarski algebraically}.
\end{prop}
\begin{proof}\marginnote{this proof can either be removed altogether or be relegated in the appendix}
Fix $U\colon \mathsf{Prop}\to \mathbb{B}$ and   $V\colon \mathsf{Prop}\to \mathbb{A}$. By induction on $\phi$. If $\phi: = p\in \mathsf{Prop}$,
\begin{center}
\begin{tabular}{r c l c r c l l}
$e(\val{p}_{c\circ U})$ & = & $e((c\circ U)(p))$ &\quad\quad &$\val{\sigma(p)}_{e\circ V}$ & = & $\val{\Diamond_{\geq} p}_{e\circ V}$ \\
& = & $(e\circ c)(\val{p}_U)$ &assoc.\ of $\circ$ && = & $\Diamond^\mathbb{B}(\val{p}_{e\circ V})$ \\
& = & $\Diamond^\mathbb{B}(\val{p}_U)$ &\quad\quad && = & $\Diamond^\mathbb{B}((e\circ V)(p))$ \\
& = & $\val{\Diamond_{\geq} p}_U$ &\quad\quad && = & $(e\circ c)((e\circ V)(p))$ \\
& = & $\val{\sigma( p)}_U$. &\quad\quad && = & $e((c \circ e)(V(p)))$ & assoc.\ of $\circ$\\
&&&&& = & $e(V(p))$ & $c\circ e = id_{\mathbb{A}}$\\
&&&&& = & $e(\val{p}_V)$. \\
\end{tabular}
\end{center}
If $\phi: = \psi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \chi$,
\begin{center}
\begin{tabular}{r c l  l}
$e(\val{\psi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \chi}_{c\circ U})$ & = & $e(\val{\psi}_{c\circ U}\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}^\mathbb{A} \val{ \chi}_{c\circ U})$ \\
& = & $e(c(e(\val{\chi}_{c\circ U})-^\mathbb{B} e(\val{ \psi}_{c\circ U})))$ & assumption \eqref{eq: pdra minus e and c} \\
& = & $e(c(\val{\sigma(\chi)}_{U}-^\mathbb{B} \val{ \sigma(\psi)}_{U}))$ & IH\\
& = & $(e\circ c)(\val{\sigma(\chi)}_{U}-^\mathbb{B} \val{ \sigma(\psi)}_{U})$ & \\
& = & $\Diamond^\mathbb{B}(\val{\sigma(\chi)}_{U}-^\mathbb{B} \val{ \sigma(\psi)}_{U})$ & \\
& = & $\val{\Box_\leq(\sigma(\chi) - \sigma(\psi))}_{U}$ & \\
& = & $\val{\sigma(\psi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}\chi)}_{U}$. & \\
\end{tabular}
\end{center}

\begin{center}
\begin{tabular}{r c l  l}
$e(\val{\psi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \chi}_{V})$ & = & $e(\val{\psi}_{V}\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}^\mathbb{A} \val{ \chi}_{V})$ \\
& = & $e(c(e(\val{\psi}_{V}) -^\mathbb{B} e(\val{ \chi}_{V})))$ & assumption \eqref{eq: pdra minus e and c} \\
& = & $e(c(\val{\sigma(\chi)}_{e\circ V} -^\mathbb{B} \val{ \sigma(\psi)}_{e\circ V}))$ & IH\\
& = & $(e\circ c)(\val{\sigma(\chi)}_{e\circ V} -^\mathbb{B} \val{ \sigma(\psi)}_{e\circ V})$ & \\
& = & $\Diamond^\mathbb{B}(\val{\sigma(\chi)}_{e\circ V} -^\mathbb{B} \val{ \sigma(\psi)}_{e\circ V})$ & \\
& = & $\val{\Diamond_\geq(\sigma(\chi)-\sigma(\psi))}_{e\circ V}$ & \\
& = & $\val{\sigma(\psi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}\chi)}_{e\circ V}$. & \\
\end{tabular}
\end{center}
The remaining cases are straightforward, and are left to the reader.
\end{proof}

\begin{remark}
\label{rem:no interaction cogodel}
In the induction step of the proof of condition (b), the specific definition of the valuation $c\circ U$ does not play any role, besides that of enabling the application of the induction hypothesis. In particular, the valuation $c\circ U$ does not interact in any way with  the role of $c$ in the definition of $\sigma$. This observation will be used in the proof of Proposition \ref{prop: sigma prime tau prime satisfy a and b}.
\end{remark}

Fact \ref{fact: main property cogoedel transl} can be obtained as a consequence of Proposition \ref{prop: main prop of Godel tarski algebraically} and the proposition above, by taking $\mathbb{A}: = \mathcal{P}^{\uparrow}(W)$, $\mathbb{B}: = \mathcal{P}(W)$, the map $e\colon \mathcal{P}^{\uparrow}(W)\hookrightarrow \mathcal{P}(W)$ as the natural embedding, and $r = c\colon \mathcal{P}(W)\twoheadrightarrow \mathcal{P}^{\uparrow}(W)$ being defined by the assignment $Y\mapsto Y{\uparrow}$. It is straightforward to see that these maps verify the assumptions of Proposition \ref{prop:sigma verifies a and b}.\marginnote{however, this same proposition will be useful in the proof of canonicity via translation, since the algebras in Proposition \ref{prop:sigma verifies a and b} do not need to be perfect.}
\end{comment}

\subsubsection{Extending the GMT and co-GMT translations to bi-intuitionistic logic}
\label{sssec: non parametric bi}
In the present subsection we consider the extensions of the GMT and co-GMT translations to  bi-intuitionistic logic (aka Heyting-Brouwer logic according to the terminology of Rauszer \cite{rauszer1974semi} who introduced this logic in the same paper, see also \cite{rauszer1974formalization, rauszer1980algebraic}). The extension $\tau'$ of the GMT translation considered below coincides with the one introduced by Wolter in \cite{wolter1998CoImplication} restricted to the language of bi-intuitionistic logic. The paper \cite{wolter1998CoImplication} considers a modal expansion of bi-intuitionistic logic with box and diamond operators where the extended GMT translation is used to establish a Blok-Esakia result and to transfer properties such as completeness, finite model property and decidability.

The language of bi-intuitionistic logic is given by
\[\mathcal{L}_B\ni\phi:: = p\mid \bot\mid \top\mid \phi\wedge \phi\mid \phi\vee\phi\mid\phi\rightarrow \phi\mid \phi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \phi\]
The language of the normal bi-modal logic S4 is  given by
\[\mathcal{L}_{S4B}\ni\alpha:: = p\mid \bot \mid \alpha\vee \alpha\mid \neg\alpha\mid \Box_{\leq} \alpha\mid \Diamond_{\geq}\alpha\]
The GMT and the co-GMT translations $\tau$ and $\sigma$ can be extended to the bi-intuitionistic language as the maps $\tau', \sigma'\colon \mathcal{L}_B\rightarrow \mathcal{L}_{S4B}$ defined by the following recursions:
\begin{center}
\begin{tabular}{r c l c r c l}
$\tau' (p)$ &  = & $\Box_{\leq} p$ & $\qquad$ & $\sigma' (p)$ &  = & $\Diamond_{\geq} p$\\
$\tau' (\bot)$ &  = & $\bot$ & & $\sigma' (\bot)$ &  = & $\bot$ \\
$\tau' (\top)$ &  = & $\top$ && $\sigma' (\top)$ &  = & $\top$ \\
$\tau' (\phi\wedge \psi)$ &  = & $\tau' (\phi)\wedge \tau'(\psi)$ && $\sigma (\phi\wedge \psi)$ &  = & $\sigma' (\phi)\wedge \sigma'(\psi)$  \\
$\tau' (\phi\vee \psi)$ &  = & $\tau' (\phi)\vee \tau'(\psi)$ && $\sigma' (\phi\vee \psi)$ &  = & $\sigma'(\phi)\vee \sigma'(\psi)$  \\
$\tau' (\phi \rightarrow \psi)$ &  = & $\Box_{\leq}(\neg \tau' (\phi)\vee \tau'(\psi))$ && $\sigma' (\phi \rightarrow \psi)$ &  = & $\Box_{\leq}(\neg \sigma' (\phi)\vee \sigma'(\psi))$.\\
$\tau' (\phi \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \psi)$ &  = & $\Diamond_{\geq}(\neg \tau' (\phi) \wedge \tau'(\psi))$ &&$\sigma' (\phi \mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$} \psi)$ &  = & $\Diamond_{\geq}(\neg\sigma' (\phi) \wedge\sigma'(\psi))$.  \\
\end{tabular}
\end{center}
Notice that $\tau'$ and $\sigma'$ agree on each defining clause but those relative to the proposition variables.
 Let $\mathbb{A}$ be a  bi-Heyting algebra  and $\mathbb{B}$  a Boolean algebra  such that $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ is an order-embedding and a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$. Suppose that $e$ has both a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ and a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ such that identities \eqref{eq: rightarrow Rightarrow e and iota} and \eqref{eq: pdra minus e and c} hold for every $a, b\in \mathbb{A}$. Then $\mathbb{B}$ can be endowed with a natural structure of bi-modal S4-algebra by defining $\Box^\mathbb{B}\colon \mathbb{B}\to \mathbb{B}$ by the assignment $b\mapsto (e\circ \iota)(b)$   and $\Diamond^\mathbb{B}\colon \mathbb{B}\to \mathbb{B}$ by the assignment $b\mapsto (e\circ c)(b)$.
 \begin{prop}
 The BAE $(\mathbb{B}, \Box^\mathbb{B}, \Diamond^\mathbb{B})$, with $\Box^\mathbb{B}, \Diamond^\mathbb{B}$ defined as above, is normal and  an S4-bimodal algebra.
 \end{prop}
The following proposition show that Proposition \ref{prop: main prop of Godel tarski algebraically} applies to $\tau'$ and $\sigma'$. We let $X:= \mathsf{Prop}$. The proof is similar to those of Propositions \ref{prop:tau verifies a and b}  and \ref{prop:sigma verifies a and b}, and is omitted.
\begin{prop}
\label{prop: sigma prime tau prime satisfy a and b}
The translation $\tau'$ (resp.\ $\sigma'$) defined above satisfies conditions (a) and (b)  of Proposition \ref{prop: main prop of Godel tarski algebraically} relative to $r: \mathbb{B}^X\to \mathbb{A}^X$ defined by $U\mapsto (\iota\circ U)$ (resp.\ defined by $U\mapsto (c\circ U)$).
\end{prop}

Thanks to the proposition above,  Proposition \ref{prop: main prop of Godel tarski algebraically} applies to both $\tau'$ and $\sigma'$ provided suitable embeddings of bi-Heyting algebras into Boolean algebras exist. The existence of such  embeddings is proven by Rauszer in \cite[Section 4]{rauszer1974semi}. We now give a reformulation of this result in the format required to instantiate Proposition \ref{prop: main prop of Godel tarski algebraically} and highlighting the compatibility of this embedding with canonical extensions --- as well as a duality-based proof.
\begin{prop}\label{prop:existence of algebras and adjoints:biHeyting}
	For every bi-Heyting algebra $\mathbb{A}$, there exists a Boolean algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ and has both a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ and a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ verifying conditions \eqref{eq: rightarrow Rightarrow e and iota} and \eqref{eq: pdra minus e and c}. Finally, all these facts lift to the canonical extensions of $\mathbb{A}$ and $\mathbb{B}$ as in the following diagram:
	\begin{center}
		\begin{tikzpicture}[node/.style={circle, draw, fill=black}, scale=1]

		\node (A) at (-1.5,-1.5) {$\mathbb{A}$};
		\node (A delta) at (-1.5,1.5) {$\mathbb{A}^{\delta}$};
		\node (B) at (1.5,-1.5) {$\mathbb{B}$};
		\node (B delta) at (1.5,1.5) {$\mathbb{B}^{\delta}$};

		\draw [right hook->] (A) to  (A delta);
		\draw [right hook->] (B)  to (B delta);
		\draw [right hook->] (A)  to node[above] {$e$}  (B);
		\draw [right hook->] (A delta)  to node[above] {$e^{\delta}$}  (B delta);

		\draw [->] (B delta) to [out=135,in=45, looseness=1]  node[below] {\rotatebox[origin=c]{270}{$\vdash$}} node[above] {$\iota^{\pi}$}  (A delta);
		\draw [->] (B) to [out=135,in=45, looseness=1]  node[below] {\rotatebox[origin=c]{270}{$\vdash$}} node[above] {$\iota$}  (A);
		\draw [->] (B delta) to [out=225,in=-45, looseness=1]  node[above] {\rotatebox[origin=c]{270}{$\vdash$}} node[below] {$c^{\sigma}$}  (A delta);
		\draw [->] (B) to [out=225,in=-45, looseness=1]  node[above] {\rotatebox[origin=c]{270}{$\vdash$}} node[below] {$c$}  (A);
		\end{tikzpicture}
	\end{center}
\end{prop}
\begin{proof}
	Via  Esakia-type duality \cite{Es75, wolter1998CoImplication}, the bi-Heyting algebra $\mathbb{A}$ can be identified  with the algebra of clopen up-sets of its associated dual space $\mathbb{X}_\mathbb{A}$  (referred to here as a a bi-Esakia space), which is a Priestley space, hence a Stone space. Let $\mathbb{B}$ be the Boolean algebra of the clopen sub{\em sets} of $\mathbb{X}_\mathbb{A}$. Since any clopen up-set is in particular a clopen subset,  a natural order embedding $e: \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is also a lattice homomorphism between $\mathbb{A}$ and $\mathbb{B}$. This shows the first part of the claim. As to the second part, bi-Esakia spaces are Priestley spaces such that both  the upward-closure and the downward-closure of a clopen set is a clopen set.

	Therefore, we can define the maps  $c\colon \mathbb{B}\to \mathbb{A}$  and $\iota\colon \mathbb{B}\to \mathbb{A}$ by the assignments $b\mapsto  b{\uparrow}$ and $b\mapsto  \neg((\neg b){\downarrow})$ respectively, where $b$ is identified with its corresponding clopen set in $\mathbb{X}_\mathbb{A}$, $\neg b$ is defined as the relative complement of $b$ in $\mathbb{X}_\mathbb{A}$, and  $b{\uparrow}$ and $(\neg b){\downarrow}$ are defined using the order in $\mathbb{X}_\mathbb{A}$. It can be readily verified that $c$ and $\iota$ are the left and right adjoints of $e$ respectively, and that moreover  conditions \eqref{eq: rightarrow Rightarrow e and iota} and \eqref{eq: pdra minus e and c} hold.

	Finally, $e:\mathbb{A}\rightarrow\mathbb{B}$ being also a homomorphism between the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ implies that $e$ is smooth and its canonical extension $e^\delta\colon \mathbb{A}^{\delta}\to \mathbb{B}^{\delta}$, besides being an order-embedding, is a complete homomorphism between the lattice reducts of $\mathbb{A}^{\delta}$ and $\mathbb{B}^{\delta}$ (cf.\  \cite[Corollary 4.8]{GeHa01}), and hence is endowed with both a left and a right adjoint. Furthermore, the left (resp.\ right) adjoint of $e^\delta$ coincides with $c^\sigma$ (resp.\ with $\iota^\pi$) (cf.\  \cite[Proposition 4.2]{GePr07}). Hence, $\mathbb{B}^{\delta}$ can be naturally endowed with the structure of an S4 bi-modal algebra by defining $\Box_{\leq}^{\mathbb{B}^{\delta}}\colon \mathbb{B}^{\delta}\to \mathbb{B}^{\delta}$ by the assignment $u\mapsto (e^\delta\circ \iota^\pi)(u)$, and $\Diamond_{\geq}^{\mathbb{B}^{\delta}}\colon \mathbb{B}^{\delta}\to \mathbb{B}^{\delta}$ by the assignment $u\mapsto (e^\delta\circ c^\sigma)(u)$.
\end{proof}

\subsection{Parametric GMT translations}\label{Sec:ParamGMTTrans}

In this section we extend the previous translations to a parametric set of GMT translations for each normal DLE- and bHAE-logic (cf.~Section \ref{sec:preliminaries}).
Parametric GMT translations were already considered in \cite{GeNaVe05} in the context of one specific DLE signature, namely that of Distributive Modal Logic, where they are used to prove the transfer of correspondence results for $\epsilon$-Sahlqvist inequalities in every order-type $\epsilon$ (cf.~Definition \ref{Inducive:Ineq:Def}). We generalize this idea to arbitrary DLE-logics, and explore the additional properties of GMT translations in the setting of bHAE-logics.

\subsubsection{Parametric GMT translations for normal DLE-logics}\label{sssection:parametric DLE}
In the present section we consider parametric GMT translations for the general DLE-setting. We will use the following notation: for every Boolean algebra $\mathbb{B}$, $n$-tuple $\overline{b}$ of elements of $\mathbb{B}$ and every order-type $\eta$ on $n$, we let $\overline{b}^\eta: = (b'_i)_{i = 1}^n$ where $b'_i = b_i$ if $\eta(i) = 1$ and $b'_i = \neg b_i$ if $\eta(i) = \partial$. Let us fix a normal DLE-signature $\mathcal{L}_{\mathrm{DLE}} = \mathcal{L}_{\mathrm{DLE}}(\mathcal{F}, \mathcal{G})$. We first identify the target language for these translations.  This is the  normal BAE-signature $\mathcal{L}^{\circ}_{\mathrm{BAE}} = \mathcal{L}_{\mathrm{BAE}}(\mathcal{F}^{\circ}, \mathcal{G}^{\circ})$ associated with $\mathcal{L}_{\mathrm{DLE}}$, where $\mathcal{F}^{\circ}: = \{\Diamond_\geq\}\cup
\{f^{\circ}\mid f\in \mathcal{F}\}$, and $\mathcal{G}^{\circ}: = \{\Box_\leq\}\cup
\{g^{\circ}\mid g\in \mathcal{G}\}$, and for every $f\in \mathcal{F}$ (resp.\ $g\in \mathcal{G}$), the  connective $f^{\circ}$ (resp.\ $g^{\circ}$) is such that $n_{f^{\circ}} = n_{f}$ (resp.\ $n_{g^{\circ}} = n_{g}$) and $\epsilon_{f^{\circ}}(i) = 1$ for each $1\leq i\leq n_f$ (resp.\ $\epsilon_{g^{\circ}}(i) = 1$ for each $1\leq i\leq n_g$).

We assume that an order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is a homomorphism of the lattice reducts of  $\mathbb{A}$ and $\mathbb{B}$, such that  both the left and right adjoint $c \colon \mathbb{B}\to\mathbb{A}$ and $\iota\colon \mathbb{B}\to \mathbb{A}$ exist
 and moreover the following diagrams commute for every $f\in \mathcal{F}$ and $g\in \mathcal{G}$:\footnote{Notice that equations \eqref{eq: rightarrow Rightarrow e and iota} and \eqref{eq: pdra minus e and c} encode the special cases of the commutativity of the diagrams \eqref{eq: e and c and iota and f and g} for $f(\phi, \psi): = \phi\mbox{$\,>\mkern-8mu\raisebox{-0.065ex}{\aol}\,$}\psi$ (in which case, $f^\circ(\neg\alpha, \beta): = \neg\alpha\wedge \beta$) and $g(\phi, \psi): = \phi\rightarrow\psi$ (in which case, $g^\circ(\neg \alpha, \beta): = \neg \alpha\vee \beta$).}
\begin{equation}\label{eq: e and c and iota and f and g}
\begin{array}{ccc}

\begin{CD}
\mathbb{A}^{n_f} @>e^{\epsilon_f}>> \mathbb{B}^{n_f}\\
@VVf^{\mathbb{A}}V @VV{f^\circ}^{\mathbb{B}}V\\
\mathbb{A} @<c<< \mathbb{B}
\end{CD}
&\quad&

\begin{CD}
\mathbb{A}^{n_g} @>e^{\epsilon_g}>> \mathbb{B}^{n_g}\\
@VVg^{\mathbb{A}}V @VV{g^\circ}^{\mathbb{B}}V\\
\mathbb{A} @<\iota<< \mathbb{B}
\end{CD}
\\
\end{array}
\end{equation}
where $e^{\epsilon_f}(\overline{a}): = \overline{e(a)}^{\epsilon_f}$ and $e^{\epsilon_g}(\overline{a}): = \overline{e(a)}^{\epsilon_g}$.
Then, as discussed early on, the Boolean reduct of $\mathbb{B}$ can be endowed with a natural structure of bi-modal S4-algebra by defining $\Box^\mathbb{B}\colon \mathbb{B}\to \mathbb{B}$ by the assignment $b\mapsto (e\circ \iota)(b)$   and $\Diamond^\mathbb{B}\colon \mathbb{B}\to \mathbb{B}$ by the assignment $b\mapsto (e\circ c)(b)$.

The target language  for the parametrized GMT translations over $\mathsf{Prop}$ is given by
\[\mathcal{L}^\circ_{BAE}\ni\alpha:: = p\mid \bot \mid \alpha\vee \alpha\mid\alpha\wedge \alpha \mid\neg\alpha\mid f^\circ(\overline{\alpha}) \mid g^\circ(\overline{\alpha})\mid \Diamond_{\geq}\alpha\mid \Box_{\leq}\alpha.\]

Let $X: = \mathsf{Prop}$. For any order-type $\epsilon$ on $X$, define the translation $\tau_\epsilon : \mathcal{L}_{\mathrm{DLE}}\to \mathcal{L}^\circ_{\mathrm{BAE}}$ by the following recursion:

\begin{center}
\begin{tabular}{c c c}
$
\tau_\epsilon(p) = \begin{cases} \Box_{\leq}  p &\mbox{if } \epsilon(p) = 1 \\
\Diamond_{\geq} p & \mbox{if } \epsilon(p) = \partial, \end{cases}
$
 & $\quad$ &

\begin{tabular}{r c l}
$\tau_\epsilon (\bot)$ &  = & $\bot$ \\
$\tau_\epsilon (\top)$ &  = & $\top$ \\
$\tau_\epsilon (\phi\wedge \psi)$ &  = & $\tau_\epsilon (\phi)\wedge \tau_\epsilon(\psi)$  \\
$\tau_\epsilon (\phi\vee \psi)$ &  = & $\tau_\epsilon (\phi)\vee \tau_\epsilon(\psi)$  \\
$\tau_\epsilon (f(\overline{\phi}))$ &  = & $\Diamond_{\geq}f^\circ(\overline{\tau_\epsilon (\phi)}^{\epsilon_f})$  \\
$\tau_\epsilon (g(\overline{\phi}))$ &  = & $\Box_{\leq}g^\circ(\overline{\tau_\epsilon (\phi)}^{\epsilon_g})$  \\
\end{tabular}
\\
\end{tabular}
\end{center}
where for each order-type $\eta$ on $n$ and any $n$-tuple $\overline{\psi}$ of $\mathcal{L}^\circ_{\mathrm{BAE}}$-formulas,  $\overline{\psi}^\eta$ denotes the $n$-tuple $(\psi'_i)_{i = 1}^n$, where $\psi_i' = \psi_i$  if $\eta(i) = 1$ and $\psi_i' = \neg \psi_i$  if $\eta(i) = \partial$.\label{notation:polarity bookkeeping}

Let $\mathbb{A}$ be a $\mathcal{L}_{\mathrm{DLE}}$-algebra and $\mathbb{B}$ be a  $\mathcal{L}^\circ_{\mathrm{BAE}}$-algebra such that an order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is a homomorphism of the lattice-reducts of $\mathbb{A}$ and $\mathbb{B}$, is endowed with  both  right and left adjoints, and satisfies the commutativity of the diagrams \eqref{eq: e and c and iota and f and g}  for every $f\in \mathcal{F}$ and $g\in \mathcal{G}$. For every order-type $\epsilon$ on $X$, consider the map $r_\epsilon: \mathbb{B}^X\to \mathbb{A}^X$ defined, for any $U\in \mathbb{B}^X$ and $p\in X$, by:
\[
r_\epsilon (U)(p) = \begin{cases}
(\iota\circ U) (p) & \mbox{if } \epsilon(p) = 1\\
(c\circ U) (p) & \mbox{if } \epsilon(p) = \partial\\
\end{cases}
\]
\begin{prop}
\label{prop:  tau epsilon for DLE satisfies a and b}
For every order-type $\epsilon$ on $X$, the translation $\tau_\epsilon$  defined above satisfies conditions (a) and (b)  of Proposition \ref{prop: main prop of Godel tarski algebraically} relative to $r_\epsilon$.
\end{prop}

\begin{proof}
By induction on $\phi$. As for the base case, let $\phi: = p\in \mathsf{Prop}$. If $\epsilon(p) = \partial$, then  for any $U\in \mathbb{B}^X$ and   $V\in\mathbb{A}^X$,
\begin{center}
\begin{tabular}{r c l l r c l l}
$e(\val{p}_{r_\epsilon(U)})$ & = & $e((c\circ U)(p))$ &(def.\ of $r_\epsilon$) &$\valb{\tau_\epsilon(p)}_{\overline{e}(V)}$ & = & $\valb{\Diamond_{\geq} p}_{\overline{e}(V)}$ & (def.\ of $\tau_\epsilon$) \\
& = & $(e\circ c)\valb{p}_U$    &(assoc.\ of $\circ$) && = & $\Diamond^\mathbb{B}\valb{p}_{\overline{e}(V)}$ & (def.\ of $\valb{\cdot}_U$)\\
& = & $\Diamond^\mathbb{B}\valb{p}_U$ & (def.\ of $\Diamond^\mathbb{B}$) && = & $\Diamond^\mathbb{B}((e\circ V)(p))$ & (def.\ of $\overline{e}(V)$) \\
& = & $\valb{\Diamond_{\geq} p}_U$ & (def.\ of $\valb{\cdot}_U$) && = & $(e\circ c)((e\circ V)(p))$ & (def.\ of $\Diamond^\mathbb{B}$) \\
& = & $\valb{\tau_\epsilon( p)}_U$. &(def.\ of $\tau_\epsilon$) && = & $e((c \circ e)(V(p)))$ & (assoc.\ of $\circ$)\\
&&&&& = & $e(V(p))$ & ($e\circ(c\circ e) = e$)\\
&&&&& = & $e(\val{p}_V)$. & (def.\ of $\val{\cdot}_V$) \\
\end{tabular}
\end{center}
If  $\epsilon(p) = 1$, then for any $U\in \mathbb{B}^X$ and   $V\in\mathbb{A}^X$,
\begin{center}
\begin{tabular}{r c l l r c l l}
$e(\val{p}_{r_\epsilon(U)})$ & = & $e((\iota\circ U)(p))$ &(def.\ of $r_\epsilon$) &$\valb{\tau_\epsilon(p)}_{\overline{e}(V)}$ & = & $\valb{\Box_{\leq} p}_{\overline{e}(V)}$ & (def.\ of $\tau_\epsilon$) \\
& = & $(e\circ \iota)\valb{p}_U$    &(assoc.\ of $\circ$) && = & $\Box^\mathbb{B}\valb{p}_{\overline{e}(V)}$ & (def.\ of $\valb{\cdot}_U$)\\
& = & $\Box^\mathbb{B}\valb{p}_U$ & (def.\ of $\Box^\mathbb{B}$) && = & $\Box^\mathbb{B}((e\circ V)(p))$ & (def.\ of $\overline{e}(V)$) \\
& = & $\valb{\Box_{\leq} p}_U$ & (def.\ of $\valb{\cdot}_U$) && = & $(e\circ \iota)((e\circ V)(p))$ & (def.\ of $\Box^\mathbb{B}$) \\
& = & $\valb{\tau_\epsilon( p)}_U$. &(def.\ of $\tau_\epsilon$) && = & $e((\iota \circ e)(V(p)))$ & (assoc.\ of $\circ$)\\
&&&&& = & $e(V(p))$ & ($e\circ(\iota\circ e) = e$)\\
&&&&& = & $e(\val{p}_V)$. & (def.\ of $\val{\cdot}_V$) \\
\end{tabular}
\end{center}
Let $\phi: = f(\overline{\phi})$. Then  for any $U\in \mathbb{B}^X$ and   $V\in\mathbb{A}^X$,
\begin{center}
	\begin{tabular}{r c l l r c l l}
		&   &$e(\val{f(\overline{\phi})}_{r_\epsilon(U)})$  &                                         & &   & $\valb{\tau_\epsilon(f(\overline{\phi}))}_{\overline{e}(V)}$ \\
		& = & $e(f(\overline{\val{\phi}_{r_\epsilon(U)}}))$ &(def.\ of $\val{\cdot}_{r_\epsilon(U)}$) & & = & $\valb{\Diamond_{\geq}f^\circ(\overline{\tau_\epsilon(\phi)}^{\epsilon_f})}_{\overline{e}(V)}$ & (def.\ of $\tau_\epsilon$) \\
		& = & $e(c\circ f^\circ(\overline{e(\val{\phi}_{r_\epsilon(U)})}^{\epsilon_f})$    &(assump.\ \eqref{eq: e and c and iota and f and g}) && = & $\Diamond^{\mathbb{B}}f^\circ(\overline{\valb{\tau_\epsilon(\phi)}_{\overline{e}(V)}}^{\epsilon_f})$ & (def.\ of $\valb{\cdot}_{\overline{e}(V)}$)\\
		& = & $\Diamond^{\mathbb{B}}f^\circ(\overline{\valb{\tau_\epsilon(\phi)}_{U}}^{\epsilon_f})$  & (IH \& def.~ of $\Diamond^{\mathbb{B}}$) && = & $\Diamond^{\mathbb{B}}f^\circ(\overline{e(\val{\phi}_V)}^{\epsilon_f})$ & (IH) \\
		& = & $\valb{\Diamond_{\geq}f^\circ(\overline{\tau_\epsilon(\phi)}^{\epsilon_f})}_U$ & (def.\ of $\valb{\cdot}_U$) && = &
		$e (c \circ f^\circ(\overline{e(\val{\phi}_V)}^{\epsilon_f}))$ & (def.\ of $\Diamond^{\mathbb{B}}$)\\
		& = & $\valb{\tau_\epsilon(f(\overline{\phi}))}_U$. &(def.\ of $\tau_\epsilon$) && = &
		$e(f(\overline{\val{\phi}_V}))$ & (assump.\ \eqref{eq: e and c and iota and f and g}) \\
		& & & && = &
		$e(\val{f(\overline{\phi})}_V)$ & (def.\ of $\val{\cdot}_V$)\\
	\end{tabular}
\end{center}

The remaining cases are analogous and are omitted.
\end{proof}
As a consequence of the proposition above, Proposition \ref{prop: main prop of Godel tarski algebraically} applies to  $\tau_\epsilon$ for any order-type $\epsilon$ on $X$. Hence:
\begin{cor}\label{cor:main theorem for tau epsilon DLE}
Let $\mathbb{A}$ be a $\mathcal{L}_{\mathrm{DLE}}$-algebra. If an embedding $e:\mathbb{A}\hookrightarrow\mathbb{B}$ exists into a  $\mathcal{L}^\circ_{\mathrm{BAE}}$-algebra $\mathbb{B}$ which is a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$, and $e$ has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ satisfying the commutativity of the  diagrams \eqref{eq: e and c and iota and f and g} for every $f\in \mathcal{F}$ and $g\in \mathcal{G}$, then for any $\mathcal{L}_{\mathrm{DLE}}$-inequality $\phi \leq \psi$,
\[
\mathbb{A}\models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models\tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi).
\]
\end{cor}

We finish this subsection by showing that every {\em perfect} $\mathcal{L}_{\mathrm{DLE}}$-algebra $\mathbb{A}$ (cf.~Definition \ref{def:DLE}) embeds into a {\em perfect} $\mathcal{L}^\circ_{\mathrm{BAE}}$-algebra $\mathbb{B}$ in the way described in Corollary \ref{cor:main theorem for tau epsilon DLE}:

\begin{prop}\label{prop:existence of algebras and adjoints:perfectDLEs}
For every perfect $\mathcal{L}_{\mathrm{DLE}}$-algebra $\mathbb{A}$, there exists a perfect  $\mathcal{L}^\circ_{\mathrm{BAE}}$--algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ and has both a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ and a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ satisfying the commutativity of the  diagrams \eqref{eq: e and c and iota and f and g}.
\end{prop}
\begin{proof}
Via expanded Birkhoff's  duality (cf.~e.g.~\cite{DaPr90, sofronie2000duality})  the  perfect $\mathcal{L}_{\mathrm{DLE}}$-algebra $\mathbb{A}$ can be identified  with the algebra of up-sets of its associated prime element $\mathcal{L}_{\mathrm{DLE}}$-frame $\mathbb{X}_\mathbb{A}$, which is based on a poset. Let $\mathbb{B}$ be the powerset algebra of the universe of $\mathbb{X}_\mathbb{A}$. Since any  up-set is in particular a subset,  a natural order embedding $e: \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is also a complete lattice homomorphism between $\mathbb{A}$ and $\mathbb{B}$. This shows the first part of the claim.

As to the second part, because $e$ is a complete homomorphism between complete lattices, it has both a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ and a right adjoint  $\iota\colon \mathbb{B}\to \mathbb{A}$, respectively defined by the assignments $b\mapsto  b{\uparrow}$ and $b\mapsto  \neg((\neg b){\downarrow})$, where $b$ is identified with its corresponding  subset in $\mathbb{X}_\mathbb{A}$, $\neg b$ is defined as the relative complement of $b$ in $\mathbb{X}_\mathbb{A}$, and  $b{\uparrow}$ and $(\neg b){\downarrow}$ are defined using the order in $\mathbb{X}_\mathbb{A}$.

Finally, notice that any $\mathcal{L}_{\mathrm{DLE}}$-frame $\mathbb{F}$ is also an $\mathcal{L}^\circ_{\mathrm{BAE}}$-frame by interpreting the $f$-type connective $\Diamond_{\geq}$ by means of the binary relation  $\geq$, the $g$-type connective $\Box_{\leq}$ by means of the binary relation $\leq$,  each $f^\circ\in \mathcal{F}^\circ$ by means of $R_f$ and each $g^\circ\in \mathcal{G}^\circ$ by means of $R_g$. Moreover, the additional properties \eqref{eq:compatibility Rf} and \eqref{eq:compatibility Rg} of the relations $R_f$ and $R_g$ guarantee that the  diagrams \eqref{eq: e and c and iota and f and g} commute for every $f\in \mathcal{F}$ and $g\in \mathcal{G}$.
\end{proof}
\begin{remark}
\label{rmk: mix sufficient but not necessary}
The parametric GMT translations defined in this section do not just  generalize  those of \cite{GeNaVe05} w.r.t.~the signature, but also differ from them in terms of their definition, and the assumptions each of which  requires. Specifically,  the parametric translations of $f$-formulas (resp.~$g$-formulas)   add an extra $\Diamond_{\geq}$ (resp.~a $\Box_{\leq}$) on top of the corresponding $f^\circ$ (resp.~$g^\circ$) connective, while in \cite{GeNaVe05}, the extra $\Diamond_{\geq}$ and $\Box_{\leq}$ are not used in the definition of the translation of formulas with a modal operator as main connective. This simpler definition is sound  only w.r.t.~semantic settings, such as that of \cite{GeNaVe05}, in which the relations interpreting the modal connectives satisfy the additional properties \eqref{eq:compatibility Rf} and \eqref{eq:compatibility Rg}. This corresponds algebraically to the operations interpreting the classical modal connectives restricting nicely to the algebra of targets of persistent valuations, and corresponds syntactically to the {\em mix axioms} (e.g.~$\Box_{\leq}\Box^\circ\Box_{\leq} p\leftrightarrow \Box^\circ p$ and $\Diamond_{\geq}\Diamond^\circ\Diamond_{\geq} p\leftrightarrow \Diamond^\circ p$, cf.~\cite[Section 6]{wolter1998CoImplication}) being valid. The particular algebras and maps picked in the proof of Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs}  happen to validate also the mix axioms. However, the mix axioms are not a necessary condition for satisfying Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs},
as the following example shows.
\begin{center}
\begin{tikzpicture}
\filldraw[black] (1,5.5) circle (3 pt) node {$\top$};
\filldraw[black] (1,4.5) circle (3 pt);
\filldraw[black] (-0.5,3.5) circle (3 pt);
\filldraw[black] (2.5,3.5) circle (3 pt);
\filldraw[black] (1,2.5) circle (3 pt);
\draw[very thick] (1, 5.5) -- (1, 4.5) --
	(-0.5, 3.5) -- (1, 2.5) -- (2.5, 3.5) -- (1, 4.5);
\draw[very thick, red, <-] (0.9, 2.4)  .. controls (0.3, 1.7) and  (1.7, 1.7)  .. (1.1, 2.4);
\draw[very thick, red, ->] (-0.65, 3.5)  .. controls (-1.4, 3.1) and  (-0.5, 2.7)  .. (-0.5, 3.4);
\draw[very thick, red, <-] (0.9, 5.6)  .. controls (0.3, 6.3) and  (1.7, 6.3)  .. (1.1, 5.6);
\draw[very thick, red, ->] (2.65, 3.5)  .. controls (3.4, 3.1) and  (2.5, 2.7)  .. (2.5, 3.4);
\draw[very thick, red, ->] (0.8, 4.5)  .. controls (0.5, 4.7) and  (0.5, 5.3)  .. (0.8, 5.5);
\draw (1, 2.2) node {$\bot$};
\draw (-0.7, 3.3) node {$b$};
\draw (1, 5.8) node {$\top$};
\draw (2.7, 3.3) node {$c$};
\draw (1, 4.2) node {$y$};

\draw[very thick] (7.5, 2.5) -- (6, 3.5) --
	(6, 4.5) -- (7.5, 5.5) -- (9, 4.5) -- (9, 3.5) -- (7.5, 4.5) -- (6, 3.5);
	\draw[very thick] (7.5, 5.5) -- (7.5, 4.5);
	\draw[very thick] (7.5, 2.5) -- (9, 3.5);
    \draw[very thick] (7.5, 2.5) -- (7.5, 3.5);
    \draw[very thick] (6, 4.5) -- (7.5, 3.5) -- (9, 4.5);
	\filldraw[black] (7.5,2.5) circle (3 pt);
	\filldraw[black] (6,3.5) circle (3 pt);
	\filldraw[black] (6,4.5) circle (3 pt);
	\filldraw[black] (7.5,5.5) circle (3 pt);
	\filldraw[black] (9,4.5) circle (3 pt);
    \filldraw[black] (7.5,3.5) circle (3 pt);
	\filldraw[black] (9,3.5) circle (3 pt);
	\filldraw[black] (7.5,4.5) circle (3 pt);
	\draw (7.5, 2.2) node {$\bot$};
	\draw (5.8, 3.3) node {$b$};
	\draw (6, 4.8) node {$a$};
	\draw (7.5, 5.8) node {$\top$};
	\draw (9, 4.8) node {$d$};
	\draw (9.2, 3.3) node {$c$};
	\draw (7.5, 4.2) node {$y$};
	\draw (7.5, 3.8) node {$x$};

\draw[very thick, red, ->] (5.8, 3.5)  .. controls (5.5, 3.7) and  (5.5, 4.3)  .. (5.8, 4.5);
\draw[very thick, red, ->] (9.2, 3.5)  .. controls (9.5, 3.7) and  (9.5, 4.3)  .. (9.2, 4.5);
\draw[very thick, red, <-] (7.4, 5.6)  .. controls (6.8, 6.3) and  (8.2, 6.3)  .. (7.6, 5.6);
\draw[very thick, red, ->] (7.3, 4.5)  .. controls (7, 4.7) and  (7, 5.3)  .. (7.3, 5.5);
\draw[very thick, red, ->] (7.3, 2.5)  .. controls (7, 2.7) and  (7, 3.3)  .. (7.3, 3.5);
\draw[very thick, red, <-] (7.4, 3.6)  .. controls (6.8, 4.3) and  (8.2, 4.3)  .. (7.6, 3.6);
\draw[very thick, red, <-] (5.9, 4.6)  .. controls (5.3, 5.3) and  (6.7, 5.3)  .. (6.1, 4.6);
\draw[very thick, red, <-] (8.9, 4.6)  .. controls (8.3, 5.3) and  (9.7, 5.3)  .. (9.1, 4.6);

\end{tikzpicture}
\end{center}

The (finite, hence perfect) distributive lattice with $\Box$ on the left embeds as a complete lattice into the (finite, hence perfect) Boolean algebra with $\Box^\circ$ on the right. Hence, the corresponding embedding $e$ has  both a right adjoint $\iota$ and a left adjoint $c$. The composition $e\circ\iota$ gives rise to the S4-operation $\Box_{\leq}: = e\circ\iota$ which by construction  maps $a$ to $b$, $d$ to $c$, $x$ to $\bot$, and every other element to itself.   It it easy to check that $\Box$ and $\Box^\circ$ verify the commutativity of diagram \eqref{eq: e and c and iota and f and g}. However, $\Box_{\leq}\Box^\circ\Box_{\leq} b  = b\neq a  = \Box^\circ b$, which shows that the mix axiom is not valid.
\end{remark}
\noindent Notice that Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs} has a more restricted scope than analogous propositions such as Propositions \ref{prop:existence of algebras and adjoints:biHeyting} or \ref{prop:existence of algebras and adjoints:Heyting}. Indeed, via expanded Priestley duality (cf.~e.g.~\cite{sofronie2000duality}), any  DLE $\mathbb{A}$ is isomorphic to the DLE of clopen up-sets of its dual (relational) Priestley space $\mathbb{X}_\mathbb{A}$, which is a Stone space in particular, and this yields a natural embedding of $\mathbb{A}$ into the BAE of the clopen subsets of $\mathbb{X}_\mathbb{A}$. However, this embedding  has in general neither a right nor a left adjoint. In Section \ref{sec:Corresp:Via:Trans}, we will see  that Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs} is enough to obtain the  correspondence theorem for inductive $\mathcal{L}_{\mathrm{DLE}}$-inequalities via translation from the correspondence theorem for inductive $\mathcal{L}_{\mathrm{BAE}}$-inequalities. However, we will see in Section \ref{sec:canonicity} that canonicity cannot be straightforwardly obtained in the same way, precisely due to the restriction on Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs}.
As we show next, this restriction can be removed if we confine ourselves setting to arbitrary normal bHAEs. In this setting, we are going to show a strengthened version of Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs}  which will be key for the transfer of canonicity of Section \ref{ssec:canonicity bHAE}.

\subsubsection{Parametric GMT translations for bHAE-logics}\label{sec:ParamGMTbHAE}

The considerations collected in Section \ref{sssection:parametric DLE} apply to the more restricted setting of bHAEs (cf.~Section \ref{ssec: DLEs}). Let us fix a bHAE-signature $\mathcal{L}_{\mathrm{bHAE}} = \mathcal{L}_{\mathrm{bHAE}}(\mathcal{F}, \mathcal{G})$ and let $\mathcal{L}^\circ_{\mathrm{BAE}}$ denote its corresponding target signature (cf.~Section \ref{sssection:parametric DLE}). Then, Corollary \ref{cor:main theorem for tau epsilon DLE} specializes as follows:

\begin{cor}\label{cor:main theorem for tau epsilon bi}
Let $\mathbb{A}$ be an $\mathcal{L}_{\mathrm{bHAE}}$-algebra. If an embedding $e:\mathbb{A}\rightarrow\mathbb{B}$ exists into an  $\mathcal{L}^\circ_{\mathrm{BAE}}$-algebra $\mathbb{B}$ which is a homomorphism of their lattice reducts and $e$ has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ satisfying \eqref{eq: rightarrow Rightarrow e and iota}, \eqref{eq: pdra minus e and c} and \eqref{eq: e and c and iota and f and g}, then for any $\mathcal{L}_{\mathrm{bHAE}}$-inequality $\phi \leq \psi$,

\[
\mathbb{A}\models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models\tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi).
\]
\end{cor}

As discussed above, the present setting is characterized  by the fact that, for any $\mathcal{L}_{\mathrm{bHAE}}$-algebras $\mathbb{A}$, the right and left adjoints of the embedding map $e: \mathbb{A} \hookrightarrow\mathbb{B}$ exist, as shown by the following proposition.
\begin{prop}\label{prop:existence of algebras and adjoints:bHAE}
For every  $\mathcal{L}_{\mathrm{bHAE}}$-algebra $\mathbb{A}$, there exists an   $\mathcal{L}^\circ_{\mathrm{BAE}}$-algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ and has both a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ and a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ satisfying \eqref{eq: rightarrow Rightarrow e and iota}, \eqref{eq: pdra minus e and c} and \eqref{eq: e and c and iota and f and g}.
	 Finally, all these facts lift to the canonical extensions of $\mathbb{A}$ and $\mathbb{B}$ as in the following diagram:
	\begin{center}
		\begin{tikzpicture}[node/.style={circle, draw, fill=black}, scale=1]

		\node (A) at (-1.5,-1.5) {$\mathbb{A}$};
		\node (A delta) at (-1.5,1.5) {$\mathbb{A}^{\delta}$};
		\node (B) at (1.5,-1.5) {$\mathbb{B}$};
		\node (B delta) at (1.5,1.5) {$\mathbb{B}^{\delta}$};

		\draw [right hook->] (A) to  (A delta);
		\draw [right hook->] (B)  to (B delta);
		\draw [right hook->] (A)  to node[above] {$e$}  (B);
		\draw [right hook->] (A delta)  to node[above] {$e^{\delta}$}  (B delta);

		\draw [->] (B delta) to [out=135,in=45, looseness=1]  node[below] {\rotatebox[origin=c]{270}{$\vdash$}} node[above] {$\iota^{\pi}$}  (A delta);
		\draw [->] (B) to [out=135,in=45, looseness=1]  node[below] {\rotatebox[origin=c]{270}{$\vdash$}} node[above] {$\iota$}  (A);
		\draw [->] (B delta) to [out=225,in=-45, looseness=1]  node[above] {\rotatebox[origin=c]{270}{$\vdash$}} node[below] {$c^{\sigma}$}  (A delta);
		\draw [->] (B) to [out=225,in=-45, looseness=1]  node[above] {\rotatebox[origin=c]{270}{$\vdash$}} node[below] {$c$}  (A);
		\end{tikzpicture}
	\end{center}
\end{prop}
\begin{proof}
By Proposition \ref{prop:existence of algebras and adjoints:biHeyting}, to complete the proof of the first part of the statement, we  need to address the claims regarding the expansions. This is done by using a   version of the  duality in \cite{sofronie2000duality} restricted to those Priestley spaces which are also bi-Esakia spaces. As to the second part, notice that the commutativity of the diagrams \eqref{eq: e and c and iota and f and g} can be written in the form of pairs of  inequalities (i.e.~$f = cf^\circ e^{\epsilon_f}$ and $g = \iota g^\circ e^{\epsilon_g}$) which are Sahlqvist and hence lift to the upper part of the diagram above.
\end{proof}
\begin{comment}
\marginnote{edit this corollary and make it compatible with the editing in the canonicity section.\\ A: edited a bit, please check, but perhaps it is better to reformulate it, and discuss not a proof, but at least where it comes from...}
\begin{cor}\label{cor:main theorem for tau epsilon bi}
Let $\mathbb{A}$ be a bHAE-algebra. If an embedding $e:\mathbb{A}\rightarrow\mathbb{B}$ exists into a Boolean algebra $\mathbb{B}$ which is a homomorphism of the lattice reducts and $e$ has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ satisfying \eqref{eq: rightarrow Rightarrow e and iota}, \eqref{eq: pdra minus e and c} and \eqref{eq: e and c and iota and f and g}, then for any bi-intuitionistic inequality $\phi \leq \psi$,

\[
\mathbb{A}\models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models\tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi).
\]
\end{cor}

\end{comment}
\begin{comment}
Let $X: = \mathsf{Prop}$. For any order-type $\epsilon$ on $X$, define the translation $\tau_\epsilon : \mathcal{L}_B\to \mathcal{L}_{S4B}$ by the following recursion:
\[
\tau_\epsilon(p) = \begin{cases} \Box_{\leq}  p &\mbox{if } \epsilon(p) = 1 \\
\Diamond_{\geq} p & \mbox{if } \epsilon(p) = \partial
\end{cases}.
\]
The remaining defining clauses for $\tau_\epsilon$ are analogous to those for $\tau'$ (cf.~Section \ref{sssec: non parametric bi}).\footnote{Dually, we could also define the parametric generalization $\sigma_\epsilon$ of $\sigma$. Since   $\sigma_\epsilon  = \tau_{\epsilon^\partial}$,  this definition would be redundant.} Clearly, $\tau' = \tau_\epsilon$ for  $\epsilon$ constantly $1$, and  $\sigma' = \tau_\epsilon$ for  $\epsilon$ constantly $\partial$.

Let $\mathbb{A}$ be a bi-Heyting algebra and $\mathbb{B}$ be a Boolean algebra such that an order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is a homomorphism of the lattice-reducts of $\mathbb{A}$ and $\mathbb{B}$, is endowed with  both  right and left adjoints, and satisfies \eqref{eq: rightarrow Rightarrow e and iota} and \eqref{eq: pdra minus e and c}  for every $a, b\in \mathbb{A}$ as described in Section \ref{sssec: non parametric bi}. For every order-type $\epsilon$ on $X$, consider the map $r_\epsilon: \mathbb{B}^X\to \mathbb{A}^X$ defined, for any $U\in \mathbb{B}^X$ and $p\in X$, by:\label{page:map r epsilon}
\[
r_\epsilon (U)(p) = \begin{cases}
(\iota\circ U) (p) & \mbox{if } \epsilon(p) = 1\\
(c\circ U) (p) & \mbox{if } \epsilon(p) = \partial\\
\end{cases}
\]
\begin{prop}
\label{prop:  tau epsilon satisfies a and b}
For every order-type $\epsilon$ on $X$, the translation $\tau_\epsilon$  defined above satisfies conditions (a) and (b)  of Proposition \ref{prop: main prop of Godel tarski algebraically} relative to $r_\epsilon$.
\end{prop}
\begin{proof}
By induction on $\phi$. As for the base case, let $\phi: = p\in \mathsf{Prop}$. If $\epsilon(p) = \partial$, then  for any $U\in \mathbb{B}^X$ and   $V\in\mathbb{A}^X$,
\begin{center}
\begin{tabular}{r c l l r c l l}
$e(\val{p}_{r_\epsilon(U)})$ & = & $e((c\circ U)(p))$ &(def.\ of $r_\epsilon$) &$\valb{\tau_\epsilon(p)}_{\overline{e}(V)}$ & = & $\valb{\Diamond_{\geq} p}_{\overline{e}(V)}$ & (def.\ of $\tau_\epsilon$) \\
& = & $(e\circ c)\valb{p}_U$    &(assoc.\ of $\circ$) && = & $\Diamond^\mathbb{B}\valb{p}_{\overline{e}(V)}$ & (def.\ of $\valb{\cdot}_U$)\\
& = & $\Diamond^\mathbb{B}\valb{p}_U$ & (def.\ of $\Diamond^\mathbb{B}$) && = & $\Diamond^\mathbb{B}((e\circ V)(p))$ & (def.\ of $\overline{e}(V)$) \\
& = & $\valb{\Diamond_{\geq} p}_U$ & (def.\ of $\valb{\cdot}_U$) && = & $(e\circ c)((e\circ V)(p))$ & (def.\ of $\Diamond^\mathbb{B}$) \\
& = & $\valb{\tau_\epsilon( p)}_U$. &(def.\ of $\tau_\epsilon$) && = & $e((c \circ e)(V(p)))$ & (assoc.\ of $\circ$)\\
&&&&& = & $e(V(p))$ & ($e\circ(c\circ e) = e$)\\
&&&&& = & $e(\val{p}_V)$. & (def.\ of $\val{\cdot}_V$) \\
\end{tabular}
\end{center}
If  $\epsilon(p) = 1$, then for any $U\in \mathbb{B}^X$ and   $V\in\mathbb{A}^X$,
\begin{center}
\begin{tabular}{r c l l r c l l}
$e(\val{p}_{r_\epsilon(U)})$ & = & $e((\iota\circ U)(p))$ &(def.\ of $r_\epsilon$) &$\valb{\tau_\epsilon(p)}_{\overline{e}(V)}$ & = & $\valb{\Box_{\leq} p}_{\overline{e}(V)}$ & (def.\ of $\tau_\epsilon$) \\
& = & $(e\circ \iota)\valb{p}_U$    &(assoc.\ of $\circ$) && = & $\Box^\mathbb{B}\valb{p}_{\overline{e}(V)}$ & (def.\ of $\valb{\cdot}_U$)\\
& = & $\Box^\mathbb{B}\valb{p}_U$ & (def.\ of $\Box^\mathbb{B}$) && = & $\Box^\mathbb{B}((e\circ V)(p))$ & (def.\ of $\overline{e}(V)$) \\
& = & $\valb{\Box_{\leq} p}_U$ & (def.\ of $\valb{\cdot}_U$) && = & $(e\circ \iota)((e\circ V)(p))$ & (def.\ of $\Box^\mathbb{B}$) \\
& = & $\valb{\tau_\epsilon( p)}_U$. &(def.\ of $\tau_\epsilon$) && = & $e((\iota \circ e)(V(p)))$ & (assoc.\ of $\circ$)\\
&&&&& = & $e(V(p))$ & ($e\circ(\iota\circ e) = e$)\\
&&&&& = & $e(\val{p}_V)$. & (def.\ of $\val{\cdot}_V$) \\
\end{tabular}
\end{center}
The remainder of the proof is similar to that of  Proposition \ref{prop: sigma prime tau prime satisfy a and b}  for $\tau'$, and is omitted.
\end{proof}
\noindent As a consequence of the proposition above, Proposition \ref{prop: main prop of Godel tarski algebraically} applies to  $\tau_\epsilon$ for any order-type $\epsilon$ on $X$. We therefore have the following corollary. Notice that, by Proposition \ref{prop:existence of algebras and adjoints:biHeyting}, suitable maps $e$, $\iota$ and $c$ exist.

\begin{cor}\label{cor:main theorem for tau epsilon bi}
Let $\mathbb{A}$ be a bi-Heyting algebra. If an embedding $e:\mathbb{A}\rightarrow\mathbb{B}$ exists into a Boolean algebra $\mathbb{B}$ which is a homomorphism of the lattice reducts and $e$ has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ satisfying \eqref{eq: rightarrow Rightarrow e and iota} and \eqref{eq: pdra minus e and c}  for every $a, b\in \mathbb{A}$, then for any bi-intuitionistic inequality $\phi \leq \psi$,

\[
\mathbb{A}\models \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B} \models\tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi).
\]
\end{cor}
\end{comment}

\section{Correspondence via translation}\label{sec:Corresp:Via:Trans
The theory developed so far puts us in a position to meaningfully formulate and prove the transfer of first-order correspondence to Sahlqvist and inductive DLE-inequalities from suitable classical poly-modal cases. These general results specialize to the logics mentioned above, e.g. those mentioned in Example \ref{ex:various DLE-languages}.

In what follows, we let $\mathcal{L}$ denote an arbitrary but fixed DLE-language and $\mathcal{L}^\circ$ its associated  target language (cf.~Section \ref{sssection:parametric DLE}).
The general definition of inductive inequalities (cf.\ Definition \ref{Inducive:Ineq:Def}) applies both $\mathcal{L}$ and $\mathcal{L}^\circ$. In particular, the Boolean negation in $\mathcal{L}^\circ$ enjoys both the order-theoretic properties of a unary $f$-type connective and of a unary $g$-type connective. Hence, Boolean negation occurs unrestricted in inductive $\mathcal{L}^\circ$-inequalities. Moreover, the algebraic interpretations of the  S4-connectives $\Box_\leq$ and $\Diamond_\geq$ enjoy the order-theoretic properties of normal unary $f$-type and $g$-type connectives respectively. Hence,  the occurrence of $\Box_\leq$ and $\Diamond_\geq$ in inductive $\mathcal{L}^\circ$-inequalities is subject to the same restrictions applied to any connective pertaining to the same class to which they belong.

The following correspondence theorem is a straightforward extension to the $\mathcal{L}^\circ$-setting of the correspondence result for classical normal modal logic in \cite{CoGoVa06}:
\begin{prop}\label{prop:correspondence theorem in lstar}
Every inductive $\mathcal{L}^\circ$-inequality has a first-order correspondent over its class of $\mathcal{L}^\circ$-frames.
\end{prop}

In what follows, we aim to transfer the correspondence theorem for inductive $\mathcal{L}^{\circ}$-inequalities as stated in the proposition  above to inductive $\mathcal{L}$-inequalities. The next proposition is the first step towards this goal. As before, let $X := \mathsf{Prop}$.
\begin{prop}\label{prop:preservation of inductive structure}
The following are equivalent for any order-type $\epsilon$ on $X$, and any  $\mathcal{L}$-inequality $\phi\leq \psi$:
  \begin{enumerate}
   \item $\phi\leq \psi$ is an $(\Omega, \epsilon)$-inductive $\mathcal{L}$-inequality;
    \item  $\tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$ is an $(\Omega, \epsilon)$-inductive $\mathcal{L}^\circ$-inequality.
    \end{enumerate}
\end{prop}
\begin{proof
By induction on the shape of $\phi\leq \psi$. In a nutshell: the definitions involved guarantee that: (1) PIA nodes are introduced immediately above $\epsilon$-critical occurrences of proposition variables;  (2) Skeleton nodes are translated as (one or more) Skeleton nodes; (3) PIA nodes are translated as (one or more) PIA nodes. Moreover, this translation does not disturb the dependency order $\Omega$. Hence, from item 1 to item 2, the translation does not introduce any violation on $\epsilon$-critical branches, and, from item 2 to item 1, the translation does not amend any violation.
\end{proof}

\begin{theorem}[Correspondence via translation]\label{theor:corr via transl}
The correspondence theorem for inductive $\mathcal{L}^{\circ}$-inequalities transfers to inductive $\mathcal{L}$-inequalities.
\end{theorem}
\begin{proof}
Let $\phi\leq \psi$ be an $(\Omega, \epsilon)$-inductive $\mathcal{L}$-inequality, and $\mathbb{F}$ be an $\mathcal{L}$-frame such that $\mathbb{F}\Vdash \phi\leq \psi$. By the discrete duality between perfect $\mathcal{L}$-algebras and $\mathcal{L}$-frames, this assumption is equivalent to $\mathbb{A}\models \phi\leq \psi$, where $\mathbb{A}$ denotes the complex $\mathcal{L}$-algebra of $\mathbb{F}$. Since $\mathbb{A}$ is a perfect $\mathcal{L}$-algebra, by Proposition
\ref{prop:existence of algebras and adjoints:perfectDLEs}, a perfect $\mathcal{L}^\circ$-algebra $\mathbb{B}$ exists with a natural embedding $e:\mathbb{A}\rightarrow\mathbb{B}$  which is a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ and  has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ such that diagrams \eqref{eq: e and c and iota and f and g} commute. Hence, Corollary
\ref{cor:main theorem for tau epsilon DLE} is applicable and yields $\mathbb{A}\models \phi\leq \psi$ iff $\mathbb{B}\models \tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$, which is equivalent to $\mathbb{F}\Vdash^*\tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$  by the discrete duality between perfect $\mathcal{L}^\circ$-algebras and $\mathcal{L}^\circ$-frames.

  By Proposition \ref{prop:preservation of inductive structure}, $\tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$ is an $(\Omega, \epsilon)$-inductive $\mathcal{L}^\circ$-inequality, and hence, by Proposition \ref{prop:correspondence theorem in lstar}, $\tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$ has a first-order correspondent $\mathsf{FO}(\phi)$ on $\mathcal{L}^\circ$-frames. Therefore $\mathbb{F}\Vdash^* \tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$ iff $\mathbb{F}\models\mathsf{FO}(\phi)$. Since the first-order frame correspondence languages of $\mathcal{L}$ and $\mathcal{L}^\circ$ are the same, it follows that $\mathsf{FO}(\phi)$ is also the first-order correspondent of $\phi\leq \psi$.

 The steps of this argument are summarized in  the following chain of equivalences:
\begin{center}
\begin{tabular}{r l r}
&$\mathbb{F}\Vdash\phi\leq \psi$&\\
iff &$\mathbb{A}\models\phi\leq \psi$& (discrete duality for $\mathcal{L}$-frames)\\
iff &$\mathbb{B} \models\tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi)$&(Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs}, Corollary
\ref{cor:main theorem for tau epsilon DLE})\\
iff &$\mathbb{F}\Vdash^*\tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi)$&(discrete duality for $\mathcal{L}^\circ$-frames)\\
iff &$\mathbb{F}\models\mathsf{FO}(\phi)$&(Proposition \ref{prop:correspondence theorem in lstar})
\end{tabular}
\end{center}
\end{proof}

\begin{remark}
In Example \ref{ex:various DLE-languages}, we showed that the languages of  Rauszer's bi-intuitionistic logic, Fischer Servi's intuitionistic modal logic, Wolter's bi-intuitionistic modal logic, Bezhanishvili's MIPC with universal modalities, Dunn's positive modal logic and Gehrke Nagahashi and Venema's Distributive Modal Logic are specific instances of DLE-logics. Hence, Theorem \ref{theor:corr via transl}, applied to each of these settings, enables one to transfer generalized Sahlqvist correspondence theorems to each of these logics. In all these settings but the latter two, this transferability is a new result which can be added to the list of known transfer results for these logics (cf.~e.g.~\cite[Section 4.1]{chagrov1992modal}). In positive modal logic and distributive modal logic, \cite[Theorem 3.7]{GeNaVe05} proves the transfer of Sahlqvist correspondence. Our result strengthens this to the transfer of correspondence for the larger class of inductive formulas.\footnote{In \cite{GorankoV06} it is shown that inductive formulas exist which are not semantically equivalent to any Sahlqvist formula.}
\end{remark}

\section{Canonicity via translation}\label{sec:canonicity}

In this section we apply the results of Section \ref{sec:instantiations}, and in particular those of Section \ref{sec:ParamGMTbHAE}, to show that the canonicity of the inductive $\mathcal{L}_{\mathrm{bHAE}}$-inequalities transfers from classical multi-modal logic via parametrized GMT translations. The proof strategy of this result does not generalize successfully to DLE-logics or, indeed, to intuitionistic or co-intuitionistic modal logics. We discuss the reasons for this and propose possible alternative strategies.

\subsection{Canonicity transfer to inductive bHAE-inequalities}\label{ssec:canonicity bHAE}

Throughout the present section, let us fix a bHAE-signature $\mathcal{L}_{\mathrm{bHAE}} = \mathcal{L}_{\mathrm{bHAE}}(\mathcal{F}, \mathcal{G})$, and let   $\mathcal{L}^\circ_{\mathrm{BAE}} =  \mathcal{L}_{\mathrm{BAE}}(\mathcal{F}^\circ, \mathcal{G}^\circ)$ be the target language for the parametric GMT translations for $\mathcal{L}_{\mathrm{bHAE}}$ (cf.~Section \ref{sssection:parametric DLE}). The following canonicity theorem is a straightforward algebraic reformulation of the canonicity result for classical normal polyadic modal logic in \cite{GorankoUnleashed} and \cite{ConGorVakSQEMA2}:
\begin{prop}\label{prop:canonicity theorem in lstar}
For every inductive $\mathcal{L}^\circ_{\mathrm{BAE}}$-inequality $\alpha\leq\beta$ and every $\mathcal{L}^\circ_{\mathrm{BAE}}$-algebra $\mathbb{B}$,
\[\mbox{if } \mathbb{B}\models \alpha\leq\beta \ \mbox{ then } \mathbb{B}^\delta\models \alpha\leq\beta.\]
\end{prop}

In what follows, we show that the canonicity of inductive $\mathcal{L}^\circ_{\mathrm{BAE}}$-inequalities, given by the proposition above, transfers to inductive $\mathcal{L}_{\mathrm{bHAE}}$-inequalities via suitable parametrized GMT translations.

\begin{theorem}[Canonicity  via translation]\label{theor:canon via transl bi HAE}
	The canonicity theorem for inductive $\mathcal{L}^\circ_{\mathrm{BAE}}$-inequalities transfers to inductive  $\mathcal{L}_{\mathrm{bHAE}}$-inequalities.
\end{theorem}
\begin{proof}
Fix an $\mathcal{L}_{\mathrm{bHAE}}$-algebra $\mathbb{A}$ and let $\phi\leq\psi$ be an inductive $\mathcal{L}_{\mathrm{bHAE}}$-inequality such that $\mathbb{A}\models \phi\leq \psi$. We show $\mathbb{A}^\delta\models \phi\leq \psi$. By Proposition \ref{prop:existence of algebras and adjoints:bHAE},  an $\mathcal{L}^\circ_{\mathrm{BAE}}$-algebra $\mathbb{B}$ exists with a natural embedding $e:\mathbb{A}\hookrightarrow\mathbb{B}$  which is a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ and  has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$ such that conditions \eqref{eq: rightarrow Rightarrow e and iota}, \eqref{eq: pdra minus e and c}, and \eqref{eq: e and c and iota and f and g} hold. Hence, Corollary \ref{cor:main theorem for tau epsilon bi} is applicable, which yields $\mathbb{A}\models \phi\leq \psi$ iff $\mathbb{B}\models \tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$.

  By Proposition \ref{prop:preservation of inductive structure}, $\tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$ is an $(\Omega, \epsilon)$-inductive $\mathcal{L}^\circ_{\mathrm{BAE}}$-inequality, and hence, by Proposition \ref{prop:canonicity theorem in lstar}, $\mathbb{B}^\delta\models\tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$. By the last part of the statement of Proposition \ref{prop:existence of algebras and adjoints:bHAE}, Corollary \ref{cor:main theorem for tau epsilon bi} applies also to $\mathbb{A}^\delta$ and $\mathbb{B}^\delta$, and thus $\mathbb{A}^\delta\models \phi\leq \psi$, as required.
 The steps of this argument are summarized in  the following U-shaped diagram:
\begin{center}
\begin{tabular}{l c l}\label{table:U:shape:algebra}

$\mathbb{A}\models\phi\leq\psi$ & & $\mathbb{A}^{\delta}\models \phi\leq\psi$ \\
$\ \ \ \ \Updownarrow$ (Prop \ref{prop:existence of algebras and adjoints:bHAE}, Cor \ref{cor:main theorem for tau epsilon bi})& & $\ \ \ \ \ \Updownarrow $ (Prop \ref{prop:existence of algebras and adjoints:bHAE}, Cor \ref{cor:main theorem for tau epsilon bi})\\
$\mathbb{B}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$ &\ \ \ $\Leftrightarrow$ \ \ \  &  $\mathbb{B}^{\delta}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$\\
\end{tabular}
\end{center}
\end{proof}
\begin{comment}
The argument above can be immediately generalized so as to obtain canonicity of inductive inequalities  for logics algebraically captured by classes of normal bi-Heyting algebra expansions (cf.\ Section \ref{sec:preliminaries}). We state the theorem omitting its proof.\marginnote{of course this theorem needs an existence of embedding theorem for bHAEs. Proposal: rewrite the current parametric bi intuitionistic to include modal expansions}

\begin{theorem}[Canonicity  via translation for bi-intuitionistic modal expansions]\label{theor:canon via transl bi HAE}
For any bHAE signature $\mathcal{L}$, every inductive $\mathcal{L}$-inequality $\phi\leq\psi$ and every HAE $\mathbb{A}$ of compatible signature,
\[\mbox{if } \mathbb{A}\models \phi\leq \psi \ \mbox{ then } \mathbb{A}^\delta\models \phi\leq \psi.\]
\end{theorem}

\end{comment}

\begin{remark}
\label{rmk: comparison canonicity}
Theorem \ref{theor:canon via transl bi HAE} applies to both  Rauszer's bi-intuitionistic logic\footnote{As discussed in Example \ref{ex: non inductive}, not all axioms in Rauszer's axiomatization of bi-intuitionistic logic are inductive. However, in \cite{gore2000dual}, Gor\'e introduces a proper display calculus for bi-intuitionistic logic, which implies, by the characterization given in \cite{GrMaPaTzZh15}, that an axiomatization for bi-intuitionistic logic exists which consists only of inductive formulas.}  \cite{rauszer1974semi} and  Wolter's bi-intuitionistic modal logic \cite{wolter1998CoImplication}. Hence,   transfer of generalized Sahlqvist canonicity theorems is available for each of these logics.  This transferability is a new result for these settings, and is different  from the transfer of d-persistence as was shown e.g.~in \cite[Theorem 12]{WoZa98} in the context of intuitionistic modal logic, in at least two respects; first, it hinges specifically on the preservation and reflection of the shape of inductive formulas; second, it does not rely on any assumptions about the interaction between the S4 and other modalities in the target logic such as those captured by the mix axiom (cf.~Remark \ref{rmk: mix sufficient but not necessary}).
\end{remark}

\begin{comment}
In the present subsection we are going to use the results in the Section \ref{semantic environment} to show the canonicity of $\epsilon$-inductive inequalities in intuitionistic (resp.\ co-intuitionistic, bi-intuitionistic) logics via $\epsilon$-parametric GMT type translation method.

\subsection{Canonicity of inductive bi-intuitionistic inequalities}

For bi-intuitionistic logic, the methodology can be summarized by the following U-shaped argument:

\begin{center}
\begin{tabular}{l c l}\label{table:U:shape:algebra}

$\mathbb{A}\models\phi\leq\psi$ & & $\mathbb{A}^{\delta}\models \phi\leq\psi$ \\
$\ \ \ \ \Updownarrow$ (Cor \ref{cor:main theorem for tau epsilon bi})& & $\ \ \ \ \ \Updownarrow $ (Cor \ref{cor:main theorem for tau epsilon bi})\\
$\mathbb{B}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$ &\ \ \ $\Leftrightarrow$ \ \ \  &  $\mathbb{B}^{\delta}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$\\
\end{tabular}
\end{center}
\marginnote{Edit this. The argument should go as follows: If $\mathbb{A}$ satisfies the hypothesis of Corollary 37 with respect to $\mathbb{B}$, then so does $\mathbb{A}^{\delta}$ w.r.t. $\mathbb{B}^{\delta}$.}
The left and right equivalences hold because the $\epsilon$-parametric GMT type translation preserves validity both for the complete algebras $\mathbb{A}^{\delta}, \mathbb{B}^{\delta}$ and for the original algebra $\mathbb{A}, \mathbb{B}$ (Corollary \ref{cor:main theorem for tau epsilon bi}). The bottom equivalence is due to $\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$ being $(\Omega, \epsilon)$-inductive (Proposition \ref{prop:preservation of inductive structure}) for S4 bi-modal logic and the fact that $(\Omega, \epsilon)$-inductive S4 bi-modal inequalities are canonical (Corollary \ref{bi-intuitionistic-canonicity}).

Let $\mathbb{A}$ be a bi-Heyting algebra. Let $\mathbb{B}$ be a Boolean algebra such that an order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists which is a homomorphism between the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$, and is endowed with both a left and a right adjoint $c\colon \mathbb{B}\to \mathbb{A}$ and $\iota\colon \mathbb{B}\to \mathbb{A}$ respectively. By Proposition \ref{prop:existence of algebras and adjoints:biHeyting}, such a Boolean algebra $\mathbb{B}$ and adjoints $c$, $\iota$ exist. Since $e:\mathbb{A}\rightarrow\mathbb{B}$ is an order-embedding which is also a homomorphism between the lattice reducts, it follows that (see \cite{???}, Proposition ???, \marginnote{references to be checked}) $e$ is smooth and its canonical extension $e^\delta\colon \mathbb{A}^{\delta}\to \mathbb{B}^{\delta}$ is an order embedding, and is a complete homomorphism between the lattice reducts of $\mathbb{A}^{\delta}$ and $\mathbb{B}^{\delta}$, and hence is endowed with both a left and a right adjoint. Furthermore, can be shown that (see \cite{???}, Proposition ???)\marginnote{references to be checked} $c^\sigma\dashv e^{\delta}\dashv\iota^\pi$. Hence, $\mathbb{B}^{\delta}$ can be endowed with a natural structure of S4 bi-modal algebra by defining $\Box_{\leq}^{\mathbb{B}^{\delta}}\colon \mathbb{B}^{\delta}\to \mathbb{B}^{\delta}$ by the assignment $u\mapsto (e^\delta\circ \iota^\pi)(u)$, and $\Diamond_{\geq}^{\mathbb{B}^{\delta}}\colon \mathbb{B}^{\delta}\to \mathbb{B}^{\delta}$ by the assignment $u\mapsto (e^\delta\circ c^\sigma)(u)$.\\

\begin{prop}\label{prop:existence of algebras and adjoints:biHeyting}
For every bi-Heyting algebra $\mathbb{A}$, there exists a Boolean algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$. Moreover, $e$ has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$.
\end{prop}

\begin{proof}

By the bi-Esakia duality between bi-Heyting algebras and bi-Esakia spaces (see \cite{Es75}), $\mathbb{A}$ can be identified with the distributive lattice of the clopen up-sets of its associated bi-Esakia space $\mathbb{X}_\mathbb{A}$, which is a Priestley space, hence a Stone space. Let $\mathbb{B}$ be the Boolean algebra of the clopen sub{\em sets} of $\mathbb{X}_\mathbb{A}$. Since any clopen up-set is in particular a clopen subset,  a natural order embedding $e: \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is also a lattice homomorphism between $\mathbb{A}$ and $\mathbb{B}$. This shows the first part of the claim.

As to the second part, notice that bi-Esakia spaces can be characterized within Priestley spaces as those Priestley spaces such that the upward- and downward-closure of a clopen set is a clopen set (see Definition \ref{def:Esakia}).

Therefore, we can define an interior operator $\iota\colon \mathbb{B}\to \mathbb{A}$ by the assignment $b\mapsto \neg((\neg b){\downarrow})$ where $b$ is identified with its corresponding clopen set in $\mathbb{X}_\mathbb{A}$, $\neg b$ is identified with the relative complement of the clopen set $b$, and $(\neg b){\downarrow}$ is defined using the order in $\mathbb{X}_\mathbb{A}$. It can be proved that $\iota$ is the right adjoint of $e$ (Lemma \ref{lemma:adjunction:iota}).

Similarly, we can define the closure operator $c\colon \mathbb{B}\to \mathbb{A}$ by the assignment $b\mapsto b{\uparrow}$, where $b$ is identified with its corresponding clopen set in $\mathbb{X}_\mathbb{A}$, and $b{\uparrow}$ is defined using the order in $\mathbb{X}_\mathbb{A}$. It can be proved that $c $ is the left adjoint of $e$ (Lemma \ref{lemma:adjunction:c}).
\end{proof}

\begin{cor}\label{bi-intuitionistic-canonicity}
$(\Omega, \epsilon)$-inductive bi-intuitionistic inequalities are canonical.
\end{cor}

\begin{proof}
Let $\phi\leq\psi$ be an $(\Omega, \epsilon)$-inductive $\mathcal{L}_{B}$-inequality and $\mathbb{A}$ be a bi-Heyting algebra such that $\mathbb{A}\models\phi\leq\psi$, which is equivalent to $\mathbb{A}^{\delta}\models_{\mathbb{A}}\phi\leq\psi$. By Proposition \ref{prop:existence of algebras and adjoints:biHeyting}, there exists a Boolean algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$. Moreover, $e$ has both a right adjoint $\iota\colon \mathbb{B}\to \mathbb{A}$ and a left adjoint $c\colon \mathbb{B}\to \mathbb{A}$. Then by Corollary \ref{cor:main theorem for tau epsilon bi}, $\mathbb{B}^{\delta}\models_{\mathbb{B}}\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$. By Proposition \ref{prop:preservation of inductive structure}, $\tau_\epsilon(\phi)\leq \tau_\epsilon(\psi)$ is an $(\Omega, \epsilon)$-inductive $\mathcal{L}_{S4B}$-inequality. Then by the canonicity of $(\Omega, \epsilon)$-inductive $\mathcal{L}_{S4B}$-inequalities (see \cite{CoGoVa06}), we get $\mathbb{B}^{\delta}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$. Then by Corollary \ref{cor:main theorem for tau epsilon bi} again, $\mathbb{A}^{\delta}\models\phi\leq\psi$.
\end{proof}
\end{comment}

\subsection{Generalizing the canonicity-via-translation argument}\label{ssec:Gen:Canon:Does:Not:Work}

In the present subsection, we discuss the extent to which the  proof pattern described in the previous subsection can be applied  to the settings of normal Heyting and co-Heyting algebra expansions (HAEs, cHAEs), and to normal DLEs. In the setting of  bHAEs, the order embedding $e$ has both a left and a right adjoint, the existence of which is shown in Proposition \ref{prop:existence of algebras and adjoints:bHAE}, while for HAEs, cHAEs and DLEs
at most one of the two adjoints was shown to exist  in general (cf.\ Propositions \ref{prop:existence of algebras and adjoints:Heyting} and  \ref{prop:existence of algebras and adjoints:coHeyting}), while both adjoints exist if the algebra is perfect (cf.~Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs}).

This implies that the  the U-shaped argument discussed in the proof of Theorem \ref{theor:canon via transl bi HAE}
is not straightforwardly applicable to HAEs, cHAEs and DLEs. Indeed, in each of these settings, the  equivalence  on the side of the perfect algebras can still be argued using Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs} and Corollary \ref{cor:main theorem for tau epsilon DLE},
but the one on the side of general algebras  (left-hand side of the diagram) cannot, precisely because Proposition \ref{prop:existence of algebras and adjoints:perfectDLEs} does not generalize to arbitrary DLEs (resp.~HAEs, cHAEs).

\begin{center}
\begin{tabular}{l c l}

$\mathbb{A}\models\phi\leq\psi$ & & $\mathbb{A}^{\delta}\models \phi\leq\psi$ \\
$\ \ \ \ \Updownarrow$ ?  & & $\ \ \ \ \ \Updownarrow $ (Prop \ref{prop:existence of algebras and adjoints:perfectDLEs}, Cor \ref{cor:main theorem for tau epsilon DLE})\\
$\mathbb{B}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$ &\ \ \ $\Leftrightarrow$ \ \ \  &  $\mathbb{B}^{\delta}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$\\
\end{tabular}
\end{center}
In what follows, we employ a more refined argument to show that the left-hand side equivalence holds. That is, the question mark in the U-shaped diagram above can be replaced by Proposition \ref{prop: main prop of Godel tarski topologically} below. We work in the setting of $\mathcal{L}$-algebras for an arbitrarily fixed DLE-signature $\mathcal{L}$, with $\mathcal{L}^\circ$ its associated target signature.
Recall that the canonical extension $e^\delta: \mathbb{A}^{\delta}\to \mathbb{B}^{\delta}$ of the embedding $e: \mathbb{A}\hookrightarrow \mathbb{B}$ is a complete lattice homomorphism, and hence both its left and right adjoints exist, which we respectively denote $c: \mathbb{B}^{\delta}\to \mathbb{A}^{\delta}$ and $\iota: \mathbb{B}^{\delta}\to \mathbb{A}^{\delta}$.
It is well known from the theory of canonical extensions that  $c(b)\in K(\mathbb{A}^{\delta})$ and $\iota(b)\in O(\mathbb{A}^{\delta})$ for every $b\in \mathbb{B}$ (cf.~\cite[Lemma 10.3]{ConPal13}).
Hence, if $r_\epsilon: (\mathbb{B}^{\delta})^X\to (\mathbb{A}^{\delta})^X$ is the map defined for any $U\in (\mathbb{B}^{\delta})^X$ and $p\in X$ by:
\[
r_\epsilon (U)(p) = \begin{cases}
(\iota\circ U) (p) & \mbox{if } \epsilon(p) = 1\\
(c\circ U) (p) & \mbox{if } \epsilon(p) = \partial\\
\end{cases}
\]

\noindent then  $(r_{\epsilon}(U)) (p) \in K(\mathbb{A}^\delta) $ if $\epsilon(p) = \partial$ and $ (r_{\epsilon}(U))(p) \in O(\mathbb{A}^\delta)$ if $\epsilon(p) = 1$
for any `admissible valuation' $U\in \mathbb{B}^X$ and $p\in X$.

\begin{lemma}\label{lemma:(a) and (b) hold refined version}
Let  $\mathbb{A}$ be an $\mathcal{L}$-algebra, and $e:\mathbb{A}\hookrightarrow\mathbb{B}$ be an embedding of $\mathbb{A}$ into an $\mathcal{L}^\circ$-algebra $\mathbb{B}$ which is a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$  such that the left and right adjoints of $e^\delta: \mathbb{A}^{\delta}\to \mathbb{B}^{\delta}$ make the diagrams \eqref{eq: e and c and iota and f and g} commute.
Then, for every order-type $\epsilon$ on $X$,
the following conditions hold for every $\phi \in \mathcal{L}$:
\begin{enumerate}
\item[(a)] $e(\val{ \phi}_V) = \valb{\tau_\epsilon(\phi)}_{\overline{e}(V)}$ for every $V \in \mathbb{A}^X$;
\item[(b)] $\valb{ \tau_\epsilon (\phi) }_U = e^\delta(\val{\phi}_{r_\epsilon(U)})$ for every $U \in \mathbb{B}^X$.
\end{enumerate}
\end{lemma}
\begin{proof}
The statement immediately follows from Proposition \ref{prop:  tau epsilon for DLE satisfies a and b} applied to  $e^\delta: \mathbb{A}^{\delta}\to \mathbb{B}^{\delta}$.
\end{proof}

\begin{prop}\label{prop: main prop of Godel tarski topologically}
Let  $\mathbb{A}$ be an $\mathcal{L}$-algebra, and $e:\mathbb{A}\hookrightarrow\mathbb{B}$ be an embedding of $\mathbb{A}$ into an $\mathcal{L}^\circ$-algebra $\mathbb{B}$ which is a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$ such that the left and right adjoints of $e^\delta: \mathbb{A}^{\delta}\to \mathbb{B}^{\delta}$ make the diagrams \eqref{eq: e and c and iota and f and g} commute.
Then,
for every $(\Omega, \epsilon)$-inductive $\mathcal{L}$-inequality $\phi \leq \psi$,
\[
\mathbb{A}^\delta \models_\mathbb{A} \phi\leq \psi \quad \mbox{ iff } \quad \mathbb{B}^\delta \models_\mathbb{B} \tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi).
\]
\end{prop}
\begin{proof}[Sketch of proof]
From right to left, if $(\mathbb{A}^\delta,V) \not\models \phi\leq \psi$ for some $V \in \mathbb{A}^X$, then $\val{\phi}_{V}\not\leq \val{\psi}_{V}$. By Lemma \ref{lemma:(a) and (b) hold refined version} (a),
this implies that $\valb{\tau_{\epsilon}(\phi)}_{\overline{e}(V)} = e(\val{\phi}_{V})\not\leq e(\val{\psi}_{V}) = \valb{\tau_{\epsilon}(\psi)}_{\overline{e}(V)}$, that is $(\mathbb{B}^\delta, \overline{e}(V)) \not\models \tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi)$, as required.

Conversely,  assume contrapositively that $(\mathbb{B}^\delta,U) \not\models \tau_{\epsilon}(\phi)\leq \tau_{\epsilon}(\psi)$ for some $U \in \mathbb{B}^X$, that is, $\valb{\tau_{\epsilon}(\phi)}_U\not\leq \valb{\tau_{\epsilon}(\psi)}_U$. By Lemma \ref{lemma:(a) and (b) hold refined version}  (b), this  is equivalent to $e^\delta(\val{\phi}_{r_\epsilon(U)})\not\leq e^\delta(\val{\psi}_{r_\epsilon(U)})$, which, by the monotonicity of $e^\delta$, implies that $\val{\phi}_{r_{\epsilon}(U)}\not\leq \val{\psi}_{r_{\epsilon}(U)}$, that is,  $(\mathbb{A}, r_{\epsilon}(U)) \not\models \phi\leq \psi$. This is not enough to finish the proof, since $r_{\epsilon}(U)$ is not guaranteed to belong in $\mathbb{A}^X$; however, as observed above, $(r_{\epsilon}(U)) (p) \in K(\mathbb{A}^\delta) $ if $\epsilon(p) = \partial$ and $ (r_{\epsilon}(U))(p) \in O(\mathbb{A}^\delta)$ if $\epsilon(p) = 1$ for each proposition variable $p$. To finish the proof, we need to show that an admissible valuation $V' \in\mathbb{A}^X$ can be manufactured from $r_{\epsilon}(U)$ and $\phi\leq\psi$ in such a way that $(\mathbb{A}^\delta, V') \not\models\phi \leq \psi$.
In what follows, we provide a sketch of the proof of the existence of the required $V'$.
Assume that $\epsilon(q)=\partial$  for some proposition variable $q$  occurring in $\phi\leq\psi$ (the case of $\epsilon(q)=1$ is analogous and is omitted). Then

 we define $V'(q)\in\mathbb{A}$
 as follows. We run ALBA on $\phi\leq\psi$ according to the dependency order $<_\Omega$, up to the point when we solve for the negative occurrences of $q$, which by assumption are $\epsilon$-critical. Notice that ALBA preserves truth under assignments.\footnote{In \cite{ConPal12} it is proved that ALBA steps preserve validity of quasi-inequalities. In fact,  something stronger is ensured, namely that truth under assignments is preserved, modulo the values of introduced and eliminated variables. This notion of equivalence is studied in e.g.\ \cite{conradie:SQEMA4}. We are therefore justified in our assumption that the value of $q$ is held constant as are the values of all variables occurring in $\phi \leq \psi$ which have not yet been eliminated up to the point where $q$ is solved for.} Then the inequality providing the minimal valuation of $q$ is of the form $q\leq\alpha$, where $\alpha$ is {\em pure} (i.e.\ no proposition variables occur in $\alpha$). By  \cite[Lemma 9.5]{ConPal12}, every inequality in the antecedent of the quasi-inequality obtained by applying first approximation to an inductive inequality is of the form $\gamma\leq\delta$ with $\gamma$ syntactically closed and $\delta$ syntactically open. Hence, $\alpha$ is pure and syntactically open, which means that the interpretation of $\alpha$ is an element in $O(\mathbb{A}^\delta)$. Therefore, by compactness, there exists some $a\in\mathbb{A}$ such that $r_{\epsilon}(U)(q)\leq a\leq\alpha$. Then we define $V'(q)=a$. Finally, it remains to be shown that $(\mathbb{A}^\delta, V')\not\models\phi \leq \psi$. This immediately follows from the fact that ALBA steps preserves truth under assignments, and that all the inequalities in the system are preserved in the change from  $r_{\epsilon}(U)$ to $V'$.
\end{proof}

However,  Proposition \ref{prop: main prop of Godel tarski topologically} is still not enough for the U-shaped argument above to go through. Indeed,
notice that, whenever $e: \mathbb{A}\to \mathbb{B}$ misses one of the two adjoints (e.g.~the left adjoint),  for any $(\Omega, \epsilon)$-inductive $\mathcal{L}$-inequality $\phi\leq\psi$ containing some $q$ with $\epsilon(q)=\partial$, its translation $\tau_{\epsilon}(\phi)\leq\tau_{\epsilon}(\psi)$ contains occurrences of the connective $\Diamond_{\geq}$, the algebraic interpretation of which in $\mathbb{B}^{\delta}$ is based on the left adjoint $c$ of $e^\delta$, which, as discussed above, maps elements in $\mathbb{B}$ to elements in $K(\mathbb{B}^{\delta})$. Hence, the canonicity of $\tau_{\epsilon}(\phi)\leq\tau_{\epsilon}(\psi)$, understood as  the preservation of its validity from $\mathbb{B}$ to $\mathbb{B}^\delta$, cannot be argued by appealing to  Proposition \ref{prop:canonicity theorem in lstar}: indeed, Proposition \ref{prop:canonicity theorem in lstar}  holds under the assumption that $\mathbb{B}$ is an $\mathcal{L}^\circ$-subalgebra of $\mathbb{B}^{\delta}$, while, as discussed above, $\mathbb{B}$ is not in general closed under $\Diamond_{\geq}$.

In order to be able to adapt the canonicity-via-translation argument to the case of HAEs, cHAEs and DLEs, we would need to  strengthen Proposition \ref{prop:canonicity theorem in lstar} so as  to obtain
the following equivalence for any
inductive $\mathcal{L}^\circ$-inequality $\alpha\leq \beta$:
 \begin{equation}\label{eq:generalized canonicity}
 \mathbb{B}^\delta\models_{\mathbb{B}} \alpha\leq\beta\ \mbox{ iff }\ \mathbb{B}^\delta\models \alpha\leq\beta\end{equation} in a setting in which the interpretations of $\Diamond_{\geq}$ and $\Box_{\leq}$ exist only in $\mathbb{B}^{\delta}$ and all we have in general for $b \in \mathbb{B}$ is that $\Diamond^{\mathbb{B}^{\delta}}(b)\in K(\mathbb{B}^\delta)$  and $\Box^{\mathbb{B}^{\delta}}(b)\in O(\mathbb{B}^\delta)$.

 Such a  strengthening cannot be straightforwardly obtained with the tools provided by the present state-of-the-art in canonicity theory.
 To see where the problem lies, let us try and apply  ALBA/SQEMA in an attempt to prove the left-to-right direction of \eqref{eq:generalized canonicity} for the `Sahlqvist' inequality $\Box_{\leq}  p\leq  \Diamond_\geq \Box_{\leq} p$, assuming that $\Diamond_\geq$ is left adjoint to $\Box_\leq$, and  $\valb{\Box_{\leq}  p}_U\in O(\mathbb{B}^{\delta})$ and $\valb{\Diamond_\geq  p}_U\in K(\mathbb{B}^{\delta})$ for any admissible valuation $U\in \mathbb{B}^X$:
 \begin{center}
 \begin{tabular}{cll}
 & $\mathbb{B}^{\delta}\models_\mathbb{B}\forall p[\Box_{\leq}  p\leq  \Diamond_\geq \Box_{\leq} p]$\\
 iff & $\mathbb{B}^{\delta}\models_\mathbb{B}\forall p\forall \mathbf{i}\forall\mathbf{m}[(\mathbf{i}\leq  \Box_{\leq}  p \ \&\ \Diamond_\geq \Box_{\leq}  p\leq \mathbf{m})\Rightarrow \mathbf{i}\leq\mathbf{m}]$\\

  iff & $\mathbb{B}^{\delta}\models_\mathbb{B}\forall p\forall \mathbf{i}\forall\mathbf{m}[(\Diamond_\geq\mathbf{i}\leq   p \ \&\ \Diamond_\geq \Box_{\leq}  p\leq \mathbf{m})\Rightarrow \mathbf{i}\leq\mathbf{m}]$\\
 \end{tabular}
 \end{center}
The minimal valuation term  $\Diamond_\geq\mathbf{j}$, computed by ALBA/SQEMA when solving for the negative occurrence of $p$, is closed. However, substituting this minimal valuation  into $\Diamond_\geq \Box_{\leq}  p\leq \mathbf{m}$ would get us $\Diamond_\geq \Box_{\leq}   \Diamond_\geq\mathbf{j}\leq \mathbf{m}$ with $\Diamond_\geq \Box_{\leq}   \Diamond_\geq\mathbf{j}$  neither closed nor open.
Hence, we cannot anymore appeal to the Esakia lemma in order to prove the following equivalence:\footnote{In other words, if $\mathbb{B}$ is not closed under $\Diamond_\geq$ or $\Box_\leq$,  the soundness of the application of the Ackermann rule under admissible assignments cannot be argued  anymore by appealing to the Esakia lemma, and hence, to the topological Ackermann lemma.}
\begin{center}
 \begin{tabular}{cll}
 & $\mathbb{B}^{\delta}\models_\mathbb{B}\forall p\forall \mathbf{i}\forall\mathbf{m}[(\Diamond_\geq\mathbf{i}\leq   p \ \&\ \Diamond_\geq \Box_{\leq}  p\leq \mathbf{m})\Rightarrow \mathbf{i}\leq\mathbf{m}]$\\
 iff & $\mathbb{B}^{\delta}\models_\mathbb{B} \forall \mathbf{i}\forall\mathbf{m}[\Diamond_\geq \Box_{\leq}\Diamond_\geq\mathbf{i}\leq \mathbf{m}\Rightarrow \mathbf{i}\leq\mathbf{m}]$\\
 \end{tabular}
 \end{center}

An analogous situation arises when solving for the positive occurrence of $p$. Other techniques for proving canonicity, such as J\'onsson-style canonicity \cite{Jonsson94,PaSoZh15a}, display the same problem, since they also rely on an Esakia lemma which is not available if $\mathbb{B}$ is not closed under $\Box_{\leq}$ and $\Diamond_\geq$.

\begin{comment}
 does not account straightfo for the canonicity of terms  although the inequality $\tau_{\epsilon}(\phi)\leq\tau_{\epsilon}(\psi)$ has the shape of an $(\Omega,\epsilon)$-inductive inequality, it does not have the order-theoretic properties which guarantee the bottom horizontal equivalence of the following U-shaped argument:

\begin{center}
\begin{tabular}{l c l}

$\mathbb{B}^{\delta}\models_{\mathbb{B}}\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$ & & $\mathbb{B}^{\delta}\models\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi)$ \\
$\ \ \ \ \Updownarrow$ & \ \ \ $\lightning$\ \ \ & $\ \ \ \ \ \Updownarrow $\\
$\mathbb{B}^{\delta}\models_{\mathbb{B}}\mathsf{SQEMA}(\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi))$ &\ \ \ $\Leftrightarrow$ \ \ \  &  $\mathbb{B}^{\delta}\models\mathsf{SQEMA}(\tau_\epsilon(\phi)\leq\tau_\epsilon(\psi))$\\
\end{tabular}
\end{center}

 In what follows, we present the  example of an inequality  in which the `topological shape' mentioned above is not preserved under ALBA manipulations  given that the interpretation of $\Diamond_{\geq}$ sends elements in $\mathbb{B}$ to elements in $K(\mathbb{B}^{\delta})$.

\begin{example}
The inequality $p\rightarrow(q\lor r)\leq(p\rightarrow q)\lor(p\rightarrow r)$ is $(\Omega, \epsilon)$-inductive for the order-type $(\partial, \partial, \partial)$ and the dependency order $q<_{\Omega}p$, $r<_{\Omega}p$. Therefore, its $\tau_{\epsilon}$-translation is

$\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\leq\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\lor\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)$. Running ALBA on the translated inequality yields:

\begin{center}
\begin{tabular}{l l r}

& $\forall p\forall q\forall r[\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\leq\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\lor\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)]$\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[\mathbf{i}\leq\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\ \ \&\ \ $\\
& $\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\lor\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)\leq\mathbf{m}\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (First approximation)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[\Diamond_{\geq}\mathbf{i}\leq\Diamond_{\geq}p\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r)\ \ \&\ \ $\\
& $\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\lor\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)\leq\mathbf{m}\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Adjunction)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[\Diamond_{\geq}\mathbf{i}\land\Diamond_{\geq}p\leq\Diamond_{\geq}q\lor\Diamond_{\geq}r\ \ \&\ \ $\\
& $\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\lor\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)\leq\mathbf{m}\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Adjunction)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[\Diamond_{\geq}p\leq\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r)\ \ \&\ \ $\\
& $\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\lor\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)\leq\mathbf{m}\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Adjunction)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[p\leq\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\ \ \&\ \ $\\
& $\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\lor\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)\leq\mathbf{m}\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Adjunction)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[p\leq\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\ \ \&\ \ $\\
& $\Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q)\leq\mathbf{m}\ \ \&\ \ \Box_{\leq}(\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r)\leq\mathbf{m}\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Splitting)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[p\leq\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}\leq\mathbf{m}\ \ \&\ \
\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}q\leq\mathbf{n}\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}'\leq\mathbf{m}\ \ \&\ \
\Diamond_{\geq}p\rightsquigarrow\Diamond_{\geq}r\leq\mathbf{n}'\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Approximation)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[p\leq\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}''\leq\mathbf{n}\ \ \&\ \ \mathbf{j}\leq\Diamond_{\geq}p\ \ \&\ \ \Diamond_{\geq}q\leq\mathbf{n}''\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}'\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}'''\leq\mathbf{n}'\ \ \&\ \ \mathbf{j}'\leq\Diamond_{\geq}p\ \ \&\ \ \Diamond_{\geq}r\leq\mathbf{n}'''
\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Approximation)\\

iff & $\forall p\forall q\forall r\forall\mathbf{i}\forall\mathbf{m}[p\leq\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}q\lor\Diamond_{\geq}r))\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}''\leq\mathbf{n}\ \ \&\ \ \mathbf{j}\leq\Diamond_{\geq}p\ \ \&\ \ q\leq\Box_{\leq}\mathbf{n}''\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}'\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}'''\leq\mathbf{n}'\ \ \&\ \ \mathbf{j}'\leq\Diamond_{\geq}p\ \ \&\ \ r\leq\Box_{\leq}\mathbf{n}'''
\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Adjunction)\\

iff & $\forall p\forall\mathbf{i}\forall\mathbf{m}[p\leq\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}\Box_{\leq}\mathbf{n}''\lor\Diamond_{\geq}\Box_{\leq}\mathbf{n}'''))\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}''\leq\mathbf{n}\ \ \&\ \ \mathbf{j}\leq\Diamond_{\geq}p\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}'\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}'''\leq\mathbf{n}'\ \ \&\ \ \mathbf{j}'\leq\Diamond_{\geq}p
\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Ackermann)\\

iff & $\forall\mathbf{i}\forall\mathbf{m}[\Box_{\leq}\mathbf{n}\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}''\leq\mathbf{n}\ \ \&\ \ \mathbf{j}\leq\Diamond_{\geq}\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}\Box_{\leq}\mathbf{n}''\lor\Diamond_{\geq}\Box_{\leq}\mathbf{n}'''))\ \ \&\ \ $\\
& $\Box_{\leq}\mathbf{n}'\leq\mathbf{m}\ \ \&\ \ \mathbf{j}\rightsquigarrow\mathbf{n}'''\leq\mathbf{n}'\ \ \&\ \ \mathbf{j}'\leq\Diamond_{\geq}\Box_{\leq}(\Diamond_{\geq}\mathbf{i}\rightsquigarrow(\Diamond_{\geq}\Box_{\leq}\mathbf{n}''\lor\Diamond_{\geq}\Box_{\leq}\mathbf{n}'''))
\ \ \Rightarrow\ \ \mathbf{i}\leq\mathbf{m}]$ & (Ackermann)
\end{tabular}
\end{center}
\end{example}

From the execution of the algorithm on the input inequality, it is easy to see that Lemma 9.5 in \cite{ConPal12}, which says that after first approximation, for all non-pure inequalities, the left-handside is syntactically closed and the right-handside is syntactically open, does not hold anymore for the current setting. Since this is the crucial condition for the topological Ackermann lemma to be applied which justifies the soundness of the Ackermann step on admissible valuations, we cannot guarantee that ALBA in the current setting is sound for admissible valuations, so success of ALBA cannot guarantee canonicity.

\begin{comment}
\section{Correspondence and canonicity(?) via translation in normal DLEs}
\subsection{Canonicity }
In \cite[Section 7]{GeNaVe05}, it is observed:
\begin{quote}
 a reduction to the classical result for canonicity seems to
be much harder than for correspondence, due to the following reason. In the correspondence
case, where we are working with perfect DMAs, there is an obvious way to connect with
boolean algebras with operators, namely by taking the (boolean) complex algebra of the dual
frame. In the canonicity case however, we would need to embed arbitrary DMAs into BAOs
in a way that would interact nicely with taking canonical extensions, and we do not see a
natural, general way for doing so.
\end{quote}
Actually such embedding always exists. Any distributive lattice $\mathbb{A}$ can be identified via Priestley duality with the distributive lattice of the clopen up-sets of its  dual space $\mathbb{X}_\mathbb{A}$, which is a Priestley space, hence a Stone space. Let $\mathbb{B}$ be the Boolean algebra of the clopen sub{\em sets} of $\mathbb{X}_\mathbb{A}$. Since any clopen up-set is in particular a clopen subset,  a natural order embedding $e: \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is also a lattice homomorphism between $\mathbb{A}$ and the lattice-reduct of $\mathbb{B}$. Since it is a homomorphism, $e$ is smooth (the best-behaved type of map for canonical extensions), and  its canonical extension $e^\delta: \mathbb{A}^{\delta}\hookrightarrow\mathbb{B}^{\delta}$ is an order-embedding and a complete lattice homomorphism. Up to now, the picture is exactly the same as the one in the case of Heyting algebras. The difference, and the actual source of difficulty, concerns the existence of the {\em adjoints} of $e$. This difference is encoded in the characterization of Esakia spaces within Priestley spaces. Namely, Esakia spaces are precisely  those Priestley spaces such that the upward (or equivalently downward) closure of a clopen set is a clopen set. This defines the closure operator $c\colon \mathbb{B}\to \mathbb{A}$, which is key to the unfolding of the canonicity via translation argument. This closure operator always exists in the setting of {\em perfect} DLEs (since they are naturally endowed with a bi-Heyting algebra structure), but not for arbitrary DLEs.

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++

\subsubsection{J\'onsson-style canonicity.}\marginnote{This part also needs to be expanded.}

In the previous paragraph, we observed that the canonicity via correspondence methodology does not work to prove the canonicity of inductive-S4B inequalities when the logical conenctives in the original language do not map clopen terms to clopen terms. However, in principle, another methodology exists, pioneered by J\'onsson \cite{Jonsson94}, who employed it to prove the canonicity of Sahlqvist inequalities of classical normal modal logic. In \cite{PaSoZh15a},
J\'onsson's methodology was generalized from Sahlqvist to inductive inequalities. In what follows, we explore the possibility of applying the methodology of \cite{PaSoZh15a} to prove the missing canonicity result and discuss why it also fails.

\paragraph{J\'onsson-style canonicity: a brief summary}

For inductive inequalities, we need to run the algorithm ALBA substantially, and as we observed from the previous part, the Ackermann step is not sound on the admissible valuation side, so we cannot apply the J\'onsson-style canonicity method to inductive inequalities. For Sahlqvist inequalities, there is another possibility, namely using the $\mathbf{n}$-trick proposed in \cite{GeNaVe05} and further analysed in \cite{van-gool:thesis}. However, we are going to show that we cannot apply it either.

Recall that, for any BAE $\mathbb{B}$, the interpretation of the connective $\mathbf{n}$ is the map $\mathbf{n}^\mathbb{B} : \mathbb{B}\times\mathbb{B}^{\partial}\rightarrow \mathbb{B}$ defined as follows:
\[ \mathbf{n}^\mathbb{B} (a, b) :=\left\{
                                    \begin{array}{ll}
                                                               \bot & \mbox{ if } a\leq b\\
                                                              \top & \mbox { if } a\nleq b.\\
                                  \end{array}
\right.\]

It is easy to check that $\mathbf{n}^\mathbb{B} : \mathbb{B}\times\mathbb{B}\rightarrow \mathbb{B}$ is join-preserving in the first coordinate and meet-reversing in the second coordinate.

In what follows, for a given term $\alpha$, a subterm $s\prec \alpha$, and a fresh variable $z$, we will abuse notation and let the symbol $\alpha(z/s)$ denote the term obtained by replacing the given {\em occurrence} of $s$ in $\alpha$ with the fresh variable $z$. The desired equivalent transformation step relies on the following conjecture:

\begin{conj}[$\mathbf{n}$-\textbf{trick}]\label{lem:n:trick:1st}
Let $\alpha, \beta, s\in\mathcal{L}_{S4B}$, and $z$ be a new variable not occurring in $\alpha$ or $\beta$, such that $\alpha\leq\beta$ is $\epsilon$-Sahlqvist, and $s$ is a subterm of $\alpha$ or $\beta$ such that $s$ consists only of non-critical branches.
\begin{enumerate}
\item if $+s\prec+\alpha$ and $+s\prec -\beta$, then $\mathbb{B}^{\delta}\models_\mathbb{B} \alpha\leq \beta $ iff $\mathbb{B}^{\delta}\models_\mathbb{B} \alpha(z/s)\leq \beta(z/s) \lor\mathbf{n}(z,s)$;
\item if $-s\prec+\alpha$ and $-s\prec -\beta$, then $\mathbb{B}^{\delta}\models_\mathbb{B} \alpha\leq \beta$ iff $\mathbb{B}^{\delta}\models_\mathbb{B} \alpha(z/s)\leq \beta(z/s) \lor \mathbf{n}(s,z)$.
\end{enumerate}
\end{conj}

However, we cannot guarantee this conjecture to hold.

\begin{proof}[Attempt at proof]

We take (1) as an example. Consider a variable $p$ with order-type $\partial$, therefore the connective in front of $p$ would be $\Diamond_{\geq}$. Then take a non-critical occurence of $p$, and let $s$ be $\Diamond_{\geq}p$ such that $s$ is labelled with $+$, so $+s\prec+\alpha$ or $+s\prec-\beta$. Then for the direction from right to left, it become problematic. Without loss of generality, we suppose that $s$ only occur in $\alpha$.

First of all, we consider an equivalent form of the right hand side:
$$\mathbb{B}^{\delta}\models_{\mathbb{B}} z\leq s\Rightarrow\alpha(z/s)\leq \beta.$$

Consider any admissible valuation $V$ on $\mathbb{B}^{\delta}$. Then we cannot use the same strategy as in \cite{van-gool:thesis}, since we cannot define the value of $z$ to be the same as $s$, due to $V(s)\in K(\mathbb{B}^{\delta})$ instead of $V(s)\in\mathbb{B}$. Another possibility is to approximate $V(s)$ by elements in $\mathbb{B}$. The sketchy idea is given as follows:

Consider any admissible valuation $V$ on $\mathbb{B}^{\delta}$. In order to show that $V(\alpha)\leq V(\beta)$, it suffices to show that $V'(\alpha(z/s))\leq V(\beta)$ for all $V'\sim_z V$ such that $V'(z)\leq V(s)$, which follows from $\mathbb{B}^{\delta}\models_{\mathbb{B}} z\leq s\Rightarrow\alpha(z/s)\leq \beta$. Then $V(\alpha)=\bigvee V'(\alpha(z/s))\leq V(\beta)$.

However, $V(\alpha)=\bigvee V'(\alpha(z/s))$ is the step that we cannot guarantee, because we cannot guarantee the Esakia property for $\alpha$, since it is neither syntactically open nor closed (due to the position of $\Diamond_{\geq}$).
\end{proof}

\begin{comment}

\begin{proof}

\begin{proof}

\end{proof}

Idea: $\mathbb{A}$ can be identified via Esakia (resp.\ co-Esakia, bi-Esakia) duality with the distributive lattice of the clopen up-sets of its  associated Esakia (resp.\ co-Esakia, bi-Esakia) space $\mathbb{X}_\mathbb{A}$, which is a Priestley space, hence a Stone space. Let $\mathbb{B}$ be the Boolean algebra of the clopen sub{\em sets} of $\mathbb{X}_\mathbb{A}$. Since any clopen up-set is in particular a clopen subset,  a natural order embedding $e: \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is also a lattice homomorphism between $\mathbb{A}$ and the lattice-reduct of $\mathbb{B}$. This shows the first part of the claim. \marginnote{maybe not a bad idea to verify that $e$ is indeed a lattice homomorphism?} As to the second part, notice that Esakia (resp.\ co-Esakia, bi-Esakia) spaces  can be characterized within Priestley spaces as those Priestley spaces such that the downward-closure (resp.\ upward-closure, upward- and downward-closure) of a clopen set is a clopen set.\marginnote{add reference? add proof in appendix?} For the Esakia case this defines an interior operator $\iota\colon \mathbb{B}\to \mathbb{A}$ by the assignment $b\mapsto \neg((\neg b){\downarrow})$ where $b$ is identified with its corresponding clopen set in $\mathbb{X}_\mathbb{A}$, $\neg b$ is identified with the relative complement of the clopen set $b$, and $(\neg b){\downarrow}$ is defined using the order in $\mathbb{X}_\mathbb{A}$ and $\iota $ is the right adjoint of $e$. Similarly, for the co-Esakia case this defines the closure operator $c\colon \mathbb{B}\to \mathbb{A}$ by the assignment $b\mapsto b{\uparrow}$, where $b$ is identified with its corresponding clopen set in $\mathbb{X}_\mathbb{A}$, and $b{\uparrow}$ is defined using the order in $\mathbb{X}_\mathbb{A}$. $c $ is the left adjoint of $e$. For the bi-Esakia case, both $c $ and $\iota $ are well defined and $c \dashv \iota$. \\

However, for the Esakia case we cannot always guarantee the existence of the closure operator $c \colon \mathbb{B} \to \mathbb{A}$ by the assignment $b \mapsto b \uparrow$ because the upward closure of a clopen set in an Esakia space is not always clopen. It is the case that $b \uparrow $ is closed when $b$ is clopen, so we can still consider the adjunction pair $ c \dashv e$ in a generalized setting. For a co-Esakia space, the situation is similar.

\begin{center}
\begin{tabular}{| c | c |}
\hline
Polarity & Skeleton\\
\hline
\begin{tabular}{c}
$+$\\
$-$\\
\end{tabular}
&
\begin{tabular}{c c c c c  }
$\land$ &$\lor$ &$\Diamond_\geq$ &$\neg$  & \\
$\lor$ &$\land$ &$\Box_\leq$ &$\neg$ & $\to$ \\
\end{tabular}
\\
\hline
&Inner Structure\\
\hline
\begin{tabular}{c}
$\phantom{+}$\\
$\phantom{+}$\\
$+$\\
$-$\\
\end{tabular}
&
\begin{tabular}{c | c c c  |  c c }
\multicolumn{4}{c}{Adjoints} & \multicolumn{2}{c}{Residuals}\\
\hline\\
$\land$ &$\Box_\leq$ &  $\neg$& &$\to$  &$\lor$\\
$\lor$ &$\Diamond_\geq$  & $\neg$& &  &$\land$\\
\end{tabular}\\
\hline
\end{tabular}
\end{center}

\section{GMT-type translations for normal DLEs}
Throughout the present section, let us fix a normal DLE signature $\mathcal{L}_{\mathrm{DLE}} = \mathcal{L}_{\mathrm{DLE}}(\mathcal{F}, \mathcal{G})$.
\begin{definition}
\label{def:DLE frame}
An $\mathcal{L}_{\mathrm{DLE}}$-{\em frame} is a tuple $\mathbb{F} = (\mathbb{X}, \mathcal{R}_{\mathcal{F}}, \mathcal{R}_{\mathcal{G}})$ such that $\mathbb{X} = (W, \leq)$ is a poset, $\mathcal{R}_{\mathcal{F}} = \{R_f\mid f\in \mathcal{F}\}$, and $\mathcal{R}_{\mathcal{G}} = \{R_g\mid g\in \mathcal{G}\}$ such that  for each $f\in \mathcal{F}$, the symbol $R_f$  denotes an $(n_f+1)$-ary  relation on $W$ such that
for all $\overline{w}, \overline{v}\in  \mathbb{X}^{\eta_f}$,
\[ \mbox{if } R_f(\overline{w})\ \mbox{ and }\ \overline{w}\geq^{\eta_f} \overline{v},\ \mbox{ then }\  R_f(\overline{v}),\]
where $\eta_f$ is the order-type on $n_f+1$ defined as follows: $\eta_f(1) = 1$ and $\eta_f(i+1) = \epsilon^\partial_f(i)$ for each $1\leq i\leq n_f$.\marginnote{Is it correct? Please check this}

Likewise, for each $g\in \mathcal{G}$, the symbol  $R_g$ denotes an $(n_g+1)$-ary relation on $W$ such that
for all $\overline{w}, \overline{v}\in  \mathbb{X}^{\eta_g}$,
\[ \mbox{if } R_g(\overline{w})\   \mbox{ and }\  \overline{w}\leq^{\eta_g} \overline{v},\ \mbox{ then }\ R_g(\overline{v}),\]
where $\eta_g$ is the order-type on $n_g+1$ defined as follows: $\eta_g(1) = 1$ and $\eta_g(i+1) = \epsilon_g^\partial(i)$ for each $1\leq i\leq n_g$.

An $\mathcal{L}_{\mathrm{DLE}}$-{\em model} is a tuple $\mathbb{M} = (\mathbb{F}, V)$ such that $\mathbb{F}$ is an $\mathcal{L}_{\mathrm{DLE}}$-frame, and $V:\mathsf{Prop}\to \mathcal{P}^{\uparrow}(W)$ is a persistent valuation.
\end{definition}

One important difference between the setting of normal DLEs and the bi-intuitionistic setting is that the defining clauses for the interpretation of each $f\in \mathcal{F}$ and $g\in \mathcal{G}$ is the same both in the DLE and in the Boolean setting:
\[
\mathbb{M},w \Vdash f(\overline{\phi}) \quad \mbox{ iff } \quad \mbox{ there exists some } \overline{v} \in W^{n_f} \mbox{ s.t. } R_f(w, \overline{v}) \mbox{ and } \mathbb{M}, v_i \Vdash \phi_i \mbox{ for each } 1\leq i\leq n_f.
\]
\[
\mathbb{M},w \Vdash g(\overline{\phi}) \quad \mbox{ iff } \quad \mbox{ for any } \overline{v} \in W^{n_g}, \mbox{ if } R_g(w, \overline{v}) \mbox{ then } \mathbb{M}, v_i \Vdash \phi_i \mbox{ for each } 1\leq i\leq n_g.
\]
Let us consider the normal BAE signature $\overline{\mathcal{L}}_{\mathrm{BAE}} = \mathcal{L}_{\mathrm{BAE}}(\overline{\mathcal{F}}, \overline{\mathcal{G}})$, where $\overline{\mathcal{F}}: = \{\Diamond_\geq\}\cup \{\overline{f}\mid f\in \mathcal{F}\}$, and $\overline{\mathcal{G}}: = \{\Box_\leq\}\cup \{\overline{g}\mid g\in \mathcal{G}\}$ and for every $f\in \mathcal{F}$ (resp.\ $g\in \mathcal{G}$), the  connective $\overline{f}$ (resp.\ $\overline{g}$) is such that $n_{\overline{f}} = n_{f}$ (resp.\ $n_{\overline{g}} = n_{g}$) and $\epsilon_{\overline{f}}(i) = 1$ for each $1\leq i\leq n_f$ (resp.\ $\epsilon_{\overline{g}}(i) = \partial$ for each $1\leq i\leq n_g$).
 Then any $\mathrm{DLE}$-frame $\mathbb{F}$ is also a $\overline{\mathcal{L}}_{\mathrm{BAE}}$-frame by interpreting the $f$-type connective $\Diamond_{\geq}$ by means of the binary relation  $\geq$, the $g$-type connective $\Box_{\leq}$ by means of the binary relation $\leq$,  each $\overline{f}\in \overline{\mathcal{F}}$ by means of $R_f$ and each $\overline{g}\in \overline{\mathcal{G}}$ by means of $R_g$. Let $\mathbb{A}$ and $\mathbb{B}$ be, respectively, the complex algebra of $\mathbb{F}$ as a $\mathrm{DLE}$-frame, and the complex algebra of $\mathbb{F}$ as a $\overline{\mathcal{L}}_{\mathrm{BAE}}$-frame. As discussed in the previous section, an order embedding $e\colon \mathbb{A}\hookrightarrow\mathbb{B}$ exists which is a complete homomorphism of the lattice reducts of  $\mathbb{A}$ and $\mathbb{B}$ and has both the left and right adjoint $c \colon \mathbb{B}\to\mathbb{A}$ and $\iota\colon \mathbb{B}\to \mathbb{A}$.

\begin{prop}
Let $bbA$ and $\mathbb{B}$ be as above. For every $f\in \mathcal{F}$ and $g\in \mathcal{G}$, the following diagrams commute:
\begin{center}
\begin{tabular}{ccc}
$
\begin{CD}
\mathbb{A}^{\epsilon_f} @>e^{\epsilon_f}>> \mathbb{B}^{\epsilon_{\overline{f}}}\\
@VVf^{\mathbb{A}}V @VV\overline{f}^{\mathbb{B}}V\\
\mathbb{A} @<c<< \mathbb{B}
\end{CD}
$
&$\quad$&
$
\begin{CD}
\mathbb{A}^{\epsilon_g} @>e^{\epsilon_g}>> \mathbb{B}^{\epsilon_{\overline{g}}}\\
@VVg^{\mathbb{A}}V @VV\overline{g}^{\mathbb{B}}V\\
\mathbb{A} @<\iota<< \mathbb{B}
\end{CD}
$\\
\end{tabular}
\end{center}
\end{prop}

\begin{proof}
\marginnote{Add proof!}
\end{proof}

For any order-type $\epsilon \colon \mathsf{Prop}\to \{1, \partial\}$, define the translation $\tau_\epsilon : \mathcal{L}_{\mathrm{DLE}}\to \mathcal{L}_{\mathrm{BAE}}$ by the following recursion:

\begin{center}
\begin{tabular}{c c c}
$
\tau_\epsilon(p) = \begin{cases} \Box_{\leq}  p &\mbox{if } \epsilon(p) = 1 \\
\Diamond_{\geq} p & \mbox{if } \epsilon(p) = \partial, \end{cases}
$
 & $\quad$ &

\begin{tabular}{r c l}
$\tau_\epsilon (\bot)$ &  = & $\bot$ \\
$\tau_\epsilon (\top)$ &  = & $\top$ \\
$\tau_\epsilon (\phi\wedge \psi)$ &  = & $\tau_\epsilon (\phi)\wedge \tau_\epsilon(\psi)$  \\
$\tau_\epsilon (\phi\vee \psi)$ &  = & $\tau_\epsilon (\phi)\vee \tau_\epsilon(\psi)$  \\
$\tau_\epsilon (f(\overline{\phi}))$ &  = & $\overline{f}(\overline{\tau_\epsilon (\phi)}^{\epsilon_f})$  \\
$\tau_\epsilon (g(\overline{\phi}))$ &  = & $\overline{g}(\overline{\tau_\epsilon (\phi)}^{\epsilon_g})$  \\
\end{tabular}
\\
\end{tabular}
\end{center}
where for each order-type $\eta$ on $n$ and any $n$-tuple $\overline{\psi}$ of $\mathcal{L}_{\mathrm{BAE}}$-formulas,  $\overline{\psi}^\eta$ denotes the $n$-tuple $(\psi'_i)_{i = 1}^n$, where $\psi_i' = \psi_i$  if $\eta(i) = 1$ and $\psi_i' = \neg \psi_i$  if $\eta(i) = \partial$.

\section{Correspondence and canonicity(?) via translation in normal DLEs}
\subsection{Canonicity }
In \cite[Section 7]{GeNaVe05}, it is observed:
\begin{quote}
 a reduction to the classical result for canonicity seems to
be much harder than for correspondence, due to the following reason. In the correspondence
case, where we are working with perfect DMAs, there is an obvious way to connect with
boolean algebras with operators, namely by taking the (boolean) complex algebra of the dual
frame. In the canonicity case however, we would need to embed arbitrary DMAs into BAOs
in a way that would interact nicely with taking canonical extensions, and we do not see a
natural, general way for doing so.
\end{quote}
Actually such embedding always exists. Any distributive lattice $\mathbb{A}$ can be identified via Priestley duality with the distributive lattice of the clopen up-sets of its  dual space $\mathbb{X}_\mathbb{A}$, which is a Priestley space, hence a Stone space. Let $\mathbb{B}$ be the Boolean algebra of the clopen sub{\em sets} of $\mathbb{X}_\mathbb{A}$. Since any clopen up-set is in particular a clopen subset,  a natural order embedding $e: \mathbb{A}\hookrightarrow\mathbb{B}$ exists, which is also a lattice homomorphism between $\mathbb{A}$ and the lattice-reduct of $\mathbb{B}$. Since it is a homomorphism, $e$ is smooth (the best-behaved type of map for canonical extensions), and  its canonical extension $e^\delta: \mathbb{A}^{\delta}\hookrightarrow\mathbb{B}^{\delta}$ is an order-embedding and a complete lattice homomorphism. Up to now, the picture is exactly the same as the one in the case of Heyting algebras. The difference, and the actual source of difficulty, concerns the existence of the {\em adjoints} of $e$. This difference is encoded in the characterization of Esakia spaces within Priestley spaces. Namely, Esakia spaces are precisely  those Priestley spaces such that the upward (or equivalently downward) closure of a clopen set is a clopen set. This defines the closure operator $c\colon \mathbb{B}\to \mathbb{A}$, which is key to the unfolding of the canonicity via translation argument. This closure operator always exists in the setting of {\em perfect} DLEs (since they are naturally endowed with a bi-Heyting algebra structure), but not for arbitrary DLEs.
\end{comment}

\section{Conclusions and further directions}\label{Sec:Conclusions}

\paragraph{Contributions.} In the present paper, we have laid the groundwork for a general and uniform theory of  transfer of generalized Sahlqvist correspondence and canonicity from normal BAE-logics to normal DLE-logics. Towards this goal, we have introduced  a unifying template for GMT translations, of which the GMT translations in the literature can be recognized as instances. We have proved that generalized Sahlqvist correspondence transfers for all DLE-logics, while generalized Sahlqvist canonicity transfers for the more restricted setting of bHAE-logics. The formulation of these results has been made possible by the recent introduction of a general mechanism for identifying Sahlqvist and inductive classes for any normal DLE-signature \cite{ConPal13}. Consequently, there are not many transfer results in the literature to which these results can be compared, the only exceptions being the transfer of Sahlqvist correspondence for DML-inequalities of \cite[Theorem 3.7]{GeNaVe05}, and  the transfer of canonicity in the form of d-persistence for intuitionistic modal formulas of \cite[Theorem 12]{WoZa98}. The transfer of correspondence shown in this paper generalizes \cite[Theorem 3.7]{GeNaVe05} both as regards the setting (from DML to general normal DLE-logics) and the scope (from Sahlqvist to inductive inequalities). As discussed in Remark \ref{rmk: comparison canonicity}, the transfer of canonicity shown in the present paper is neither subsumed by, nor  does it subsume  \cite[Theorem 12]{WoZa98}.

Regarding insights, we have also gained a better understanding of the nature  of the difficulties in the transfer of (generalized) Sahlqvist canonicity via GMT translations. These difficulties were discussed as follows in the conclusions  of \cite{GeNaVe05}: \begin{quote}[...] a reduction to
the classical result for canonicity seems to be much harder than for correspondence, due
to the following reason. In the correspondence case, where we are working with perfect
DMAs, there is an obvious way to connect with Boolean algebras with operators, namely
by taking the (Boolean) complex algebra of the dual frame. In the canonicity case however,
we would need to embed arbitrary DMAs into BAOs in a way that would interact nicely with
taking canonical extensions, and we do not see a natural, general way for doing so.
 \end{quote}
Our analysis shows that, actually,  the problem does not lie in the interaction between the embedding and the canonical extensions,  but rather in the fact that the embedding $e: \mathbb{A}\hookrightarrow  \mathbb{B}$ of an arbitrary DLE into a suitable BAE lacks the required adjoint maps, and that while the role of these adjoints can be played to a certain extent by the adjoints of $e^\delta: \mathbb{A}^\delta\hookrightarrow  \mathbb{B}^\delta$ (cf.~Proposition \ref{prop: main prop of Godel tarski topologically}), we would need to develop a much stronger theory of algebraic (generalized) Sahlqvist canonicity in the BAE setting to be able to reduce (generalized) Sahlqvist canonicity for DLEs to the Boolean setting.

\paragraph{Further directions.} As  mentioned above,  our analysis suggests a way  to obtain the transfer of generalized Sahlqvist canonicity for arbitrary DLE-logics, namely   to develop a generalized canonicity theory in the setting of BAEs which relies on the order-theoretic properties of maps $\mathbb{A}\to \mathbb{B}^\delta$. The way to this theory has already been paved in \cite{PaSoZh15a}, where  a generalization of the standard theory of  canonical extensions of maps is developed, accounting for maps $f^{\mathbb{A}}:\mathbb{A}\to\mathbb{B}^{\delta}$   such that the value of $f^{\mathbb{A}}$ is not restricted to clopen elements in $\mathbb{B}$.

\begin{comment}
\paragraph{Unified correspondence and GMT translations} We saw that, where applicable, the translation method has
an extraordinary synthesizing power.
However, as already mentioned at various points early on, we do not believe that the translation approach can provide autonomous  foundations to correspondence theory for non-classical logics, and this for two reasons.
First, in Section \ref{sec:canonicity} we saw  that,
outside of the bi-intuitionistic setting, it is not clear how the canonicity-via-translation argument could be made to work. To make it work, one would likely need techniques which import novel order-theoretic and topological insights which go well beyond the scope of the translation method itself.  The existing canonicity techniques therefore remain the most straightforward route toward the result.
Second, as argued in Remark \ref{rem:final remarks on correspondence via translation}, unified correspondence is also needed to provide the right background framework in which correspondence-via-translation can be meaningfully investigated.

 \medskip
\end{comment}
\paragraph{Blok-Esakia theorem for DLE-logics.} The uniform perspective on GMT translations developed in this paper can perhaps be useful to systematically explore the possible variants of the notion of `modal companion' of a given intuitionistic modal logic, and extend the Blok-Esakia theorem uniformly to DLE-logics.
\paragraph{Methodology: generalization through algebras via duality.} The generalized canonicity-via-translation result for the bi-intuitionistic setting comes from embracing the full extent of the algebraic analysis. Specifically, canonicity-via-translation hinges upon the fact that the  interplay of persistent and non-persistent valuations on frames can be understood and reformulated in terms of an adjunction situation between two complex algebras of the same frame.  In its turn, this adjunction situation generalizes to arbitrary algebras. The same modus operandi, which achieves generalization through algebras via duality, has been fruitfully employed by some of the authors also for very different purposes, such as the definition of the non-classical counterpart of a given logical framework (cf.\  \cite{KurzPalmiLMCS2013, MaPaSa14, CoFrPaTz15}).

\begin{comment}
\section{Generalized canonical extensions of maps}\label{sec: gen can ext maps}

The main technical difficulty we face when trying to employ the expanded language manipulated by ALBA for the J\'onsson strategy is that DMAs are not in general closed under the additional operations (i.e.\ under the adjoints and residuals of the operations interpreting the connectives of the original signature). This is the reason why  a generalization of the standard theory of  canonical extensions of maps is needed, accounting for maps $f^{\mathbb{A}}:\mathbb{A}\to\mathbb{B}^{\delta}$   such that the value of $f^{\mathbb{A}}$ is not restricted to clopen elements in $\mathbb{B}$. Providing this treatment is the aim of the present section.

Specifically,  building on  \cite[Section 2.3]{GeJo04},  we consider primitive maps $f^{A^{\delta}}:A^{\delta}\to\mathbb{B}^{\delta}$, then consider their restrictions  $f^{\mathbb{A}}:\mathbb{A}\to\mathbb{B}^{\delta}$ to $\mathbb{A}$, and then define the {\em generalized} $\lambda$-extensions   $(f^{\mathbb{A}})^{\lambda}:A^{\delta}\to\mathbb{B}^{\delta}$ (for $\lambda\in \{\sigma, \pi\}$) of these restrictions. Comparing these generalized extensions to the original maps $f^{A^{\delta}}$ gives rise to associated definitions of $\lambda$-contracting or expanding maps. This theory can be applied to the adjoints and residuals of the operations interpreting the connectives of the original DML signature.

The intuition behind these generalized extensions of maps is based e.g.\ on the similarity with the way in which the value of a continuous real variable function on an irrational real number can be taken as a limit of its values on rational numbers.

In \cite{GeJo04}, canonical extensions are fully discussed only for functions $f^{\mathbb{A}}:\mathbb{A}\to\mathbb{B}$, and not for functions $f^{\mathbb{A}}:\mathbb{A}\to\mathbb{B}^{\delta}$.  In the present section  we fill this gap.

\subsection{Generalized canonical extensions of maps and their basic properties}\label{subsec:gce:basic:property}

In what follows, we use superscripts to indicate the domain of the function. For instance, the symbol $f^{\mathbb{A}}$ indicates the restriction of $f^{A^\delta}$ to $\mathbb{A}$ or to ${\mathbb{A}}^{\epsilon}$, depending on the context. Abusing notation, we extend this convention also to operation symbols. For instance, instead of denoting an operation on $\mathbb{A}$, the symbol $\Diamondblack^{\mathbb{A}}$ denotes a map from $\mathbb{A}$ to $A^\delta$, which is the restriction of the map $\Diamondblack^{A^\delta}:A^\delta\toA^\delta$ to $\mathbb{A}$. Throughout the present section, $\mathbb{A}$, $\mathbb{B}, \mathbb{C}$ denote BDLs.

\begin{definition}[\textbf{Generalized canonical extensions of maps}]\label{def:gcem:chap:6}
For any order-preserving map $f^{\mathbb{A}}:\mathbb{A}\rightarrow\mathbb{B}^{\delta}$ and any $u\in \mathbb{A}^\delta$, we let:
\[(f^{\mathbb{A}})^\sigma (u) =\bigvee \{ \bigwedge \{f^{\mathbb{A}}(a): x\leq a\in \mathbb{A}\}: u \geq x \in K (A^\delta)\}\]
\[(f^{\mathbb{A}})^\pi (u) =\bigwedge \{ \bigvee \{f^{\mathbb{A}}(a): y\geq a\in \mathbb{A}\}: u \leq y \in O (A^\delta)\}.\]
\end{definition}
For example, for a given DMA $\mathbb{A}$, consider the left adjoint $\Diamondblack^{A^\delta}:A^\delta\toA^\delta$ of $\Box^{A^\delta}:A^\delta\toA^\delta$. Let $\Diamondblack^{\mathbb{A}}:\mathbb{A}\toA^\delta$ be its restriction to $\mathbb{A}$. Let the generalized canonical extension of $\Diamondblack^{\mathbb{A}}$ be $(\Diamondblack^{\mathbb{A}})^{\lambda}$, where $\lambda\in\{\sigma, \pi\}$. We will show that $(\Diamondblack^{\mathbb{A}})^{\sigma}=(\Diamondblack^{\mathbb{A}})^{\pi}=\Diamondblack^{A^\delta}$ (see Section \ref{sec:propty:DMLplusplus}).

Many properties of $\sigma$- and $\pi$-extensions still hold in the generalized setting. Here we state some of them without proof.

\begin{prop}\label{prop:gce}
For any order-preserving map $f^{\mathbb{A}}:\mathbb{A}\rightarrow\mathbb{B}^{\delta}$,
\begin{enumerate}
\item Both $(f^{\mathbb{A}})^\sigma$ and $(f^{\mathbb{A}})^\pi$ are order-preserving;
\item $(f^{\mathbb{A}})^\sigma(x)= \bigwedge \{f^{\mathbb{A}}(a): x\leq a\in \mathbb{A}\}$ for any $x\inK(\mathbb{A}^\delta)$;
\item $(f^{\mathbb{A}})^\pi(y)= \bigvee \{f^{\mathbb{A}}(a): y\geq a\in \mathbb{A}\}$ for any $y\inO(\mathbb{A}^\delta)$;
\item $(f^{\mathbb{A}})^\sigma(a)=(f^{\mathbb{A}})^\pi(a)=f^{\mathbb{A}}(a)$ for any $a\in\mathbb{A}$;
\item\label{5} $(f^{\mathbb{A}})^\sigma(u)\leq(f^{\mathbb{A}})^\pi(u)$ for any $u\inA^\delta$, and the equality holds if $u\inK(\mathbb{A}^\delta)\cupO(\mathbb{A}^\delta)$.
\end{enumerate}
\end{prop}

The next proposition extends to the generalized setting a fundamental property of canonical extensions, and will play a crucial role in Section \ref{sec:diffi}.

\begin{prop}\label{prop:largestUC}
Given any order-preserving map $f^{\mathbb{A}}:\mathbb{A}\rightarrow\mathbb{B}^{\delta}$,
\begin{enumerate}
\item $(f^{\mathbb{A}})^{\sigma}$ is the largest order-preserving UC extension of $f^{\mathbb{A}}$ to $A^\delta$.
\item $(f^{\mathbb{A}})^{\pi}$ is the smallest order-preserving LC extension of $f^{\mathbb{A}}$ to $A^\delta$.
\end{enumerate}
\end{prop}

Below, we generalize the definition of stable, expanding, and contracting maps to this new setting:

\begin{definition}[\textbf{Generalized stable, expanding and contracting maps}]
For any order-preserving map $f^{A^{\delta}}:A^{\delta}\to{\mathbb{B}}^{\delta}$, and for $\lambda\in\{\sigma, \pi\}$,
\begin{itemize}
\item $f^{A^{\delta}}$ is \emph{$\lambda$-stable}, if $f^{A^{\delta}} = (f^\mathbb{A})^\lambda$;
\item $f^{A^{\delta}}$ is \emph{$\lambda$-expanding}, if $f^{A^{\delta}} \leq (f^\mathbb{A})^\lambda$;
\item $f^{A^{\delta}}$ is \emph{$\lambda$-contracting}, if $f^{A^{\delta}}\geq(f^\mathbb{A})^\lambda$).
\end{itemize}
\end{definition}
\subsection{Generalized $\sigma$-contracting and $\pi$-expanding maps, and Esakia conditions}\label{sec:gen:sgma:contr}
As mentioned at the end of Section \ref{subsec:chara:Esakia}, Proposition \ref{Esa:equi} can be generalized to the present setting. In the present subsection, we characterize $\sigma$-contracting and $\pi$-expanding maps in terms of the generalized Esakia conditions (cf.\ Theorem \ref{thm:Esa:equi}) and also in terms of the intersection conditions (cf.\ Lemma \ref{lem:Esa:inter}).
\begin{definition}[\textbf{Generalized Esakia conditions}]\label{Def:Esa}
For any order-preserving map $f^{A^\delta}:A^\delta\to{\mathbb{B}}^{\delta}$,
\begin{enumerate}
\item $f^{A^\delta}$ is \emph{closed Esakia} if for any non-empty downward-directed collection $\mathcal{C}=\{c_i : i\in I\}\subseteq K(\mathbb{A}^\delta)$, $f^{A^\delta}(\bigwedge\{c_i : i\in I\})=\bigwedge f^{A^\delta}(\{c_i : i\in I\})$;
\item $f^{A^\delta}$ is \emph{open Esakia} if for any non-empty upward-directed collection $\mathcal{O}=\{o_i : i\in I\}\subseteq O(\mathbb{A}^\delta)$, $f^{A^\delta}(\bigvee\{o_i : i\in I\})=\bigvee f^{A^\delta}(\{o_i : i\in I\})$.
\end{enumerate}
\end{definition}
\begin{theorem}\label{thm:6:7}
For any order-preserving map $f^{A^\delta}:A^\delta\to{\mathbb{B}}^{\delta}$, both $(f^{\mathbb{A}})^{\sigma}$ and $(f^{\mathbb{A}})^{\pi}$ are both open and closed Esakia.
\end{theorem}

\begin{theorem}\label{thm:Esa:equi}
For any order-preserving map $f^{A^\delta}:A^\delta\to{\mathbb{B}}^{\delta}$,
\begin{enumerate}
\item $f^{A^\delta}$ is $\sigma$-contracting iff $f^{A^\delta}$ is closed Esakia;
\item $f^{A^\delta}$ is $\pi$-expanding iff $f^{A^\delta}$ is open Esakia.
\end{enumerate}
\end{theorem}

In fact, for $n$-ary order-preserving maps, we can also show that the Esakia conditions of Definition \ref{Def:Esa} are equivalent to the following much more manageable intersection conditions, which will be used in the discussion about the comparison between the two approaches to canonicity.

In what follows, we will represent a given map $f^{A^\delta}:(A^\delta)^{\epsilon}\to{\mathbb{B}}^{\delta}$ by grouping together the monotone and the antitone coordinates. Hence, we will write $f^{A^\delta}$ as $f^{A^\delta}(\vec u, \vec v):(A^\delta)^{\epsilon}\to{\mathbb{B}}^{\delta}$, and assume that the function $f^{A^\delta}(\vec u, \vec v)$ is monotone in its $\vec u$ coordinates and antitone in its $\vec v$ coordinates. Moreover, we use the variable $w$ to select a given coordinate in $\vec u$ or $\vec v$, and, abusing notation, we write the function $f^{A^\delta}(\vec u, \vec v)$ as $f^{A^\delta}(\vec u, \vec v, w)$. Also, symbols such as $\vec c\inK(\mathbb{A}^\delta)$ indicate that every element in the array $\vec c$ belongs to $K(\mathbb{A}^\delta)$.

\begin{definition}[\textbf{Intersection conditions}]\label{Def:intprop}
For any order-preserving map $f^{A^\delta}(\vec u, \vec v):(A^\delta)^{\epsilon}\to{\mathbb{B}}^{\delta}$,
\begin{enumerate}
\item the map $f^{A^\delta}$ satisfies the \emph{closed intersection condition} if the following holds for any coordinate $w$, for all $\vec c\inK(\mathbb{A}^\delta), \vec o\inO(\mathbb{A}^\delta)$, any non-empty downward-directed (resp.\ upward-directed) collection $\{c_i : i\in I\}\subseteq K(\mathbb{A}^\delta)$ (resp.\ $\{o_i : i\in I\}\subseteq O(\mathbb{A}^\delta)$):
\begin{itemize}
\item if the order type of $f$ in the coordinate $w$ is $1$, then \[f^{A^\delta}(\vec c, \vec o, \bigwedge\{c_i : i\in I\})=\bigwedge\{f^{A^\delta}(\vec c, \vec o, c_i):i\in I\};\]
\item if the order type of $f$ in the coordinate $w$ is $\partial$, then \[f^{A^\delta}(\vec c, \vec o, \bigvee\{o_i : i\in I\})=\bigwedge\{f^{A^\delta}(\vec c, \vec o, o_i):i\in I\}.\]
\end{itemize}

\item the map $f^{A^\delta}$ satisfies the \emph{open intersection condition} if the following holds for any coordinate $w$, for all $\vec c\inK(\mathbb{A}^\delta), \vec o\inO(\mathbb{A}^\delta)$, any non-empty downward-directed (resp.\ upward-directed) collection $\{c_i : i\in I\}\subseteq K(\mathbb{A}^\delta)$ (resp.\ $\{o_i : i\in I\}\subseteq O(\mathbb{A}^\delta)$):
\begin{itemize}
\item if the order type of $f$ in the coordinate $w$ is $1$, then \[f^{A^\delta}(\vec o, \vec c, \bigvee\{o_i : i\in I\})=\bigvee\{f^{A^\delta}(\vec o, \vec c, o_i):i\in I\};\]
\item if the order type of $f$ in the coordinate $w$ is $\partial$, then \[f^{A^\delta}(\vec o, \vec c, \bigwedge\{c_i : i\in I\})=\bigvee\{f^{A^\delta}(\vec o, \vec c, c_i):i\in I\}.\]
\end{itemize}
\end{enumerate}
\end{definition}
Clearly, the intersection conditions above are the coordinatewise versions of the Esakia conditions. In the following lemma, we show that the Esakia conditions and their coordinatewise counterparts are equivalent.

We remind our notational convention that the function $f^{A^\delta}(\vec u, \vec v)$ is monotone in its $\vec u$ coordinates and antitone in its $\vec v$ coordinates.

\begin{lemma}\label{lem:Esa:inter}
For any order-preserving map $f^{A^\delta}(\vec u, \vec v):(A^\delta)^{\epsilon}\to{\mathbb{B}}^{\delta}$, \begin{enumerate}
\item $f^{A^\delta}$ is closed Esakia iff it satisfies the closed intersection condition;
\item $f^{A^\delta}$ is open Esakia iff it satisfies the open intersection condition;
\end{enumerate}
\end{lemma}

\subsection{Sufficient conditions for generalized $\sigma$-expanding or $\pi$-contracting maps}\label{sec:diffi}
In the present subsection, we give conditions guaranteeing maps to be $\sigma$-expanding or $\pi$-contracting. In what follows, we only discuss the property of being $\sigma$-expanding, since the treatment for $\pi$-contracting maps can be obtained by order-duality.

\subsubsection{Upper and lower continuity}
In Section \ref{subsec:gce:basic:property}, we proved that the generalized $\sigma$-extension (resp.\ $\pi$-extension) is the greatest (resp.\ least) upper (resp.\ lower) continuous extension of a given map (cf.\ Proposition \ref{prop:largestUC}). The following is an immediate consequence of this fact.

\begin{cor}\label{cor:largestgenuc}
For any order-preserving map $g^{A^\delta}:A^\delta\to\mathbb{B}^{\delta}$,
\begin{enumerate}
\item if $g^{A^\delta}$ is UC, then $g^{A^\delta}\leq (g^{\mathbb{A}})^{\sigma}$, i.e.\ $g$ is $\sigma$-expanding
\item if $g^{A^\delta}$ is LC, then $g^{A^\delta}\geq (g^{\mathbb{A}})^{\pi}$, i.e.\ $g$ is $\pi$-contracting
\end{enumerate}
\end{cor}

\subsubsection{Weak $m$-Scott and dual weak $m$-Scott continuity}

In the present subsection we study the order-theoretic properties of generalized extensions of \emph{additive} maps (cf.\ Definition \ref{def:additive}), i.e., order-preserving maps $f^{\mathbb{A}}:\mathbb{A}_1\times\ldots\times\mathbb{A}_m\to\mathbb{B}^{\delta}$ which preserve finite non-empty joins in each coordinate. Recall that \emph{completely additive} maps are order-preserving maps $f^{A^\delta}:\mathbb{A}^{\delta}_1\times\ldots\times\mathbb{A}^{\delta}_m\to\mathbb{B}^{\delta}$ which preserve arbitrary non-empty joins in each coordinate. \emph{Multiplicative} and \emph{completely multiplicative} maps are defined order-dually.
\begin{lemma}\label{lem:complete:oper}
For any order-preserving map $f^{\mathbb{A}}:\mathbb{A}_1\times\ldots\times\mathbb{A}_m\to\mathbb{B}^{\delta}$,
\begin{enumerate}
\item if $f^{\mathbb{A}}$ is additive, then $(f^{\mathbb{A}})^{\sigma}:\mathbb{A}^{\delta}_1\times\ldots\times\mathbb{A}^{\delta}_m\to\mathbb{B}^{\delta}$ is completely additive;
\item if $f^{\mathbb{A}}$ is multiplicative, then $(f^{\mathbb{A}})^{\pi}:\mathbb{A}^{\delta}_1\times\ldots\times\mathbb{A}^{\delta}_m\to\mathbb{B}^{\delta}$ is completely multiplicative.
\end{enumerate}
\end{lemma}

The following lemma generalizes  Corollary 5.7 in \cite{GeNaVe05}. In what follows,
 we let  $f_i^{A^\delta}:A^\delta\to{\mathbb{B}}_i^{\delta}$ be order-preserving for any $1\leq i\leq m$. We let ${\mathbb{B}}^{\delta}:={\mathbb{B}}_1^{\delta}\times\ldots\times{\mathbb{B}}_m^{\delta}$   and $g^{{\mathbb{B}}^{\delta}}:{\mathbb{B}}_1^{\delta}\times\ldots\times{\mathbb{B}}_m^{\delta}\to\mathbb{C}^{\delta}$ be order-preserving,  and  $(g\circ (f_1, \ldots, f_m))^{\mathbb{A}}$ be the restriction of  $g^{{\mathbb{B}}^{\delta}}(f_1^{A^\delta}, \ldots, f_m^{A^\delta})$ to $\mathbb{A}$.

\begin{lemma}\label{lem:gen:Scott}
For all  $f_i^{A^\delta}$, $g^{{\mathbb{B}}^{\delta}}$, and $(g\circ (f_1, \ldots, f_m))^{\mathbb{A}}$ as above,
\begin{enumerate}
\item if $g^{{\mathbb{B}}^{\delta}}$ is completely additive, then $g^{{\mathbb{B}}^{\delta}}((f_1^{\mathbb{A}})^{\sigma}, \ldots, (f_m^{\mathbb{A}})^{\sigma})\leq((g\circ (f_1, \ldots, f_m))^{\mathbb{A}})^{\sigma}$;
\item if $g^{{\mathbb{B}}^{\delta}}$ is completely multiplicative, then $g^{{\mathbb{B}}^{\delta}}((f_1^{\mathbb{A}})^{\pi}, \ldots, (f_m^{\mathbb{A}})^{\pi})\geq((g\circ (f_1, \ldots, f_m))^{\mathbb{A}})^{\pi}$.
\end{enumerate}
\end{lemma}

\subsubsection{Strong upper and lower continuity}
In \cite{GeNaVe05}, it is shown that if  $f^{\mathbb{A}}:\mathbb{A}\to\mathbb{B}$ is meet-preserving, then $(f^{\mathbb{A}})^{\sigma}$ is SUC. This result  generalizes as  follows:
\begin{theorem}\label{thm:cmp:SUC}
\begin{enumerate}
\item Let $f^{A^\delta}:\mathbb{A}^{\delta}\to\mathbb{B}^{\delta}$ be completely p-multiplicative and open Esakia (cf. Definition \ref{Def:Esa}), and such that $f^{A^\delta}(a)\in O({\mathbb{B}}^{\delta})$ for all $a\in\mathbb{A}$. Then $f^{A^\delta}$ is SUC, and hence is also $\sigma$-expanding.
\item Let $f^{A^\delta}:\mathbb{A}^{\delta}\to\mathbb{B}^{\delta}$ be completely p-additive and closed Esakia (cf. Definition \ref{Def:Esa}), and such that $f^{A^\delta}(a)\in K({\mathbb{B}}^{\delta})$ for all $a\in\mathbb{A}$. Then $f^{A^\delta}$ is SLC, and hence is also $\pi$-contracting.
\end{enumerate}
\end{theorem}

Corollary 5.9 in \cite{GeNaVe05} is  generalized in the lemma below. In what follows, $f^{A^\delta}:A^\delta\to{\mathbb{B}}^{\delta}$ and $g^{{\mathbb{B}}^{\delta}}:{\mathbb{B}}^{\delta}\to\mathbb{C}^{\delta}$ are order-preserving maps,  and $(g\circ f)^{\mathbb{A}}$ denotes the restriction of their composition $g^{{\mathbb{B}}^{\delta}}\circ f^{A^\delta}$ to $\mathbb{A}$.
\begin{lemma}\label{lem:gen:SUC}
For any  $f^{A^\delta}$,  $g^{{\mathbb{B}}^{\delta}}$, and $(g\circ f)^{\mathbb{A}}$ as above,
\begin{enumerate}
\item if $f^{A^\delta}$ is completely p-multiplicative, open Esakia, and moreover $f^{A^\delta}(a)\in O({\mathbb{B}}^{\delta})$ for all $a\in\mathbb{A}$, and $g^{{\mathbb{B}}^{\delta}}$ is open Esakia, then $(g^\mathbb{B})^{\sigma}\circ f^{A^\delta}\leq((g\circ f)^{\mathbb{A}})^{\sigma}$;
\item if $f^{A^\delta}$ is completely p-additive, closed Esakia, and moreover $f^{A^\delta}(a)\in K({\mathbb{B}}^{\delta})$ for all $a\in\mathbb{A}$, and $g^{{\mathbb{B}}^{\delta}}$ is closed Esakia, then $(g^\mathbb{B})^{\pi}\circ f^{A^\delta}\geq((g\circ f)^{\mathbb{A}})^{\pi}$.
\end{enumerate}
\end{lemma}

\section{Preliminaries for translation via canonicity}

\begin{definition}
A topological space is called a \textbf{Stone Space} if it satisfies the following three conditions:
\begin{enumerate}
\item It is Hausdorff: for every $x,y \in X$, if $x \neq y$ then there exist opens $U, V$ such that $U \cap V = \emptyset$ and $x \in U$, $y \in V$.
\item It is compact: given any arbitrary open covering of $X$, there exists a finite subcovering $X = \cup_{i = 1}^n U_i$.
\item It is zero-dimensional, that is, every open $U$ is the union of clopens.
\end{enumerate}
\end{definition}

\begin{definition}
A Priestley space $(X, \mathcal{O}, \leq)$ is a topological space $(X, \mathcal{O})$ together with a partial order $\leq$ on $X$, such that the following Priestley separation axiom holds:
\[
x\nleq y \text{ implies there is a clopen upset } U \text{ such that } x\in U \text{ and } y \notin U.
\]
\end{definition}

\begin{definition} The relation $\leq$ is called clopen if $U\downarrow$ is clopen for every clopen set $U$.
\end{definition}

\begin{definition}\label{def:Esakia}
\begin{enumerate}
\item We say that $(X, \mathcal{O}, \leq)$ is an Esakia space if it is a Priestley space and $\leq$ is clopen.
\item  We say that $(X, \mathcal{O}, \leq)$ is a co-Esakia space if it is a Priestley space and $\geq$ is clopen.
\item We say that $(X, \mathcal{O}, \leq)$ is a bi-Esakia space if it is a Priestley space and $\leq$ is clopen and $\geq$ is also clopen.
\end{enumerate}
\end{definition}

Given an (ordered) topological space $X$ we use $\mathcal{CP}(X)$ (resp.\ $ \mathcal{CUP}(X)$, $\mathcal{C}(X)$ and $\mathcal{CU}(X)$ to denote the collection of clopen sets of $X$ (resp.\ the collection of clopen upsets, closed sets and closed upsets) of $X$.

\begin{thm}\label{stone dual and esakia dual}
\begin{enumerate}
\item For every Boolean algebra $\mathbb{B}$ there exists a Stone space $(X, \mathcal{O})$ such that $\mathbb{B}$ is isomorphic to $ \mathcal{C} \mathcal{P}(X)$, which is the Boolean algebra of all clopens of $(X, \mathcal{O})$.
\item For every Heyting algebra $\mathbb{A}$ there exists an Esakia space $(X, \mathcal{O}, \leq)$ such that $\mathbb{A}$ is isomorphic to the Heyting algebra of all clopen upsets of $X$ which we denote by $\mathcal{CUP}(X)$.
\item For every co-Heyting algebra $\mathbb{A}$ there exists a co-Esakia space $(X, \mathcal{O}, \leq)$ such that $\mathbb{A}$ is isomorphic to the co-Heyting algebra of all clopen upsets of $X$.
\item For every bi-Heyting algebra $\mathbb{A}$ there exists a bi-Esakia space $(X, \mathcal{O}, \leq)$ such that $\mathbb{A}$ is isomorphic to the Heyting algebra of all clopen upsets of $X$.
\end{enumerate}
\end{thm}

\paragraph{Constructing the Boolean algebra from the Heyting algebra}
Given a Heyting algebra $\mathbb{A}$, by Theorem \ref{stone dual and esakia dual} item 2. there exists an Esakia space $(X, \mathcal{O}, \leq) $ such that $\mathbb{A}$ is isomorphic to the Heyting algebra of all clopen upsets of $X$. Since for any Esakia space $(X, \mathcal{O}, \leq)$ we have that $(X, \mathcal{O}) $ is a Stone space, we can define the Boolean algebra $\mathbb{B}$ to be the Boolean algebra of clopen sets of said Stone space, where we also have a natural embedding $e \colon \mathcal{CPU}(X) \to \mathcal{CP}(X)$. By abuse of notation, in what follows we will identify $\mathbb{A}$ with $\mathcal{CPU}(X)$ and $\mathbb{B}$ with $\mathcal{CP}(X)$. \\

\begin{prop}\label{prop:existence of algebras and adjoints}
\begin{enumerate}
\item For every Heyting algebra $\mathbb{A}$ there exists a Boolean algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e \colon \mathbb{A} \hookrightarrow \mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$. Moreover, $e$ has a right adjoint.
\item For every co-Heyting algebra $\mathbb{A}$ there exists a Boolean algebra $\mathbb{B}$ such that $\mathbb{A}$ embeds into $\mathbb{B}$ via some order-embedding $e \colon \mathbb{A} \hookrightarrow \mathbb{B}$ which is also a homomorphism of the lattice reducts of $\mathbb{A}$ and $\mathbb{B}$. Moreover, $e$ has a left adjoint.
\end{enumerate}
\end{prop}

Let us define $\iota \colon \mathcal{CP}(X) \to \mathcal{CPU}(X)$ such that $\iota(Y) = (Y^c)  \downarrow ^c$. We can show the following:

\begin{lemma}\label{lemma:adjunction:iota} For any $Y \in \mathcal{CPU}(X)$ and any $Z \in \mathcal{CP}(X)$, $e (Y) \subset
Z$ if and only if $Y \subset \iota(Z)$.
\end{lemma}

\begin{proof}
It suffices to show that $Y \subset Z$ if and only if $Y \subset \iota Z$. The right to left direction is easy. For the converse, since $Y$ is an up-set, $Y^c$ is a down-set so $Y^c \downarrow = Y^c$ and therefore $Y = (Y^c)^c= Y^c \downarrow^c = \iota (Y) $, so $Y = \iota
(Y) \subset \iota (Z).$
\end{proof}

However, for the Heyting case we cannot always guarantee that $e$ has a left adjoint $c \colon \mathcal{CP}(X) \to \mathcal{CPU}(X)$ because by defining $c (Y) \colon = Y \uparrow$, while $Y$ is a clopen set, we cannot guarantee that $Y \uparrow$ is clopen. We can show that $Y \uparrow$ is closed, therefore we can define $\Diamond \colon = e \circ c \colon \mathcal{CP}(X) \to \mathcal{CU}(X)$, where $\mathcal{CU}(X)$ is the collection of \emph{closed} up-sets of $X$.

The following lemma is a property of Priestley spaces:
\begin{lemma}\label{lemma:closed:c}
For any $Y \in \mathcal{C}(X)$, $c(Y) \in \mathcal{CU}(X)$.
\end{lemma}
\begin{lemma}\label{lemma:adjunction:c}
For any $Y \in \mathcal{C}(X)$ and any $Z \in \mathcal{CU}(X)$, $c(Y) \subset Z$ if and only if $Y \subset e(Z).$
\end{lemma}

\begin{lemma}\label{closed esakia lemma}
For any downward directed nonempty collection $\mathcal{C} \subset \mathcal{C}(X)$,
\[
\bigcap_{C \in \mathcal{C}}C \uparrow = \bigcap_{C \in \mathcal{C}}(C \uparrow).
\]

\end{lemma}

\begin{lemma}\label{join preserving lemma}
For any collection $\mathcal{X} \subset \mathcal{P}(X)$, $Y \in \mathcal{X}$,
\[
\bigcup_{Y \in \mathcal{X}} Y \uparrow = \bigcup_{Y \in \mathcal{X}} (Y \uparrow).
\]
\end{lemma}

\end{comment}
\bibliographystyle{abbrv}