# On a Generalization of Heyting Algebras I

Amirhossein Akbar Tabatabai  Institute of Mathematics, Czech Academy of
Sciences  Majid Alizadeh  School of Mathematics, Statistics and Computer
Science, College of Science, University of Tehran  Masoud Memarzadeh  School
of Mathematics, Statistics and Computer Science, College of Science,
University of Tehran

###### Abstract

$\nabla$-algebra is a natural generalization of Heyting algebra, unifying many
algebraic structures including bounded lattices, Heyting algebras, temporal
Heyting algebras and the algebraic presentation of the dynamic topological
systems. In a series of two papers, we will systematically study the algebro-
topological properties of different varieties of $\nabla$-algebras. In the
present paper, we start with investigating the structure of these varieties by
characterizing their subdirectly irreducible and simple elements. Then, we
prove the closure of these varieties under the Dedekind-MacNeille completion
and provide the canonical construction and the Kripke representation for
$\nabla$-algebras by which we establish the amalgamation property for some
varieties of $\nabla$-algebras. In the sequel of the present paper, we will
complete the study by covering the logics of these varieties and their
corresponding Priestley-Esakia and spectral duality theories.

Keywords: Heyting algebras, temporal Heyting algebras, dynamic topological
systems, amalgamation property.

##  1 Introduction

#### Abstract Implications

Implication is the logical machinery to _internalize_ the _meta-linguistic_
provability relation defined _over_ a language to a logical constant _inside_
the language itself. Generally speaking, the internalization is a process to
reflect _some_ properties of the relation $\vdash$ by the corresponding
properties of its internal version $\to$. For instance, the reflexivity of
$\vdash$, i.e., the property $A\vdash A$ is reflected by the property $\vdash
A\to A$ and the transitivity of $\vdash$, i.e., the property “ _$A\vdash B$
and $B\vdash C$ implies $A\vdash C$_” is reflected by the property $(A\to
B)\wedge(B\to C)\vdash(A\to C)$. Depending on the structures available over
the propositions and the extent to which the internalization process reflects
the corresponding properties, various types of implications appeared in
various logical systems. The spectrum spreads from the standard instances of
classical, intuitionistic and substructural implications to philosophically
motivated conditionals [15], weak sub-intuitionistic [39, 40, 37] and
mathematically motivated implications appearing in provability logic [40] and
preservability logic [26, 27, 34]. To unify all these instances under one
umbrella notion, some formalizations have been proposed [12, 5]. Here, we
follow the abstract notion of implication introduced in [1] as a binary
operation performing the minimum amount of internalization, i.e.,
internalizing the fact that the provability relation is actually a preorder.
More precisely, an implication $\to$ is a binary operation over a meet semi-
lattice $\mathsf{A}$, decreasing in its first argument and increasing in its
second satisfying the _internal reflexivity_ $(a\to a)=1$ and the _internal
transitivity_ $(a\to b)\wedge(b\to c)\leq(a\to c)$, for any
$a,b,c\in\mathsf{A}$.111Technically, the definition presented in [1] uses a
monoidal poset rather than a meet semi-lattice to cover the substructural
implications. However, in this paper, we restrict ourselves to this special
case as we are only interested in the so-called structural framework.

Among all possible implications, the Heyting implication and its defining
adjunction have a special mathematical and philosophical position. The reason
is the role that the adjunction plays in the internalization process by
_reducing_ the internal version of a property into the property itself. Let us
explain this role by a concrete example. Consider the existence of the binary
meets identified by the _equivalence_ between “$a\leq b\wedge c$” and
“(_$a\leq b$ and $a\leq c$_)” and note that its internal version is the
_equality_ $(a\to(b\wedge c))=(a\to b)\wedge(a\to c)$. To prove the internal
version for the Heyting implication, we show the equivalence between $d\leq
a\to(b\wedge c)$ and $d\leq(a\to b)\wedge(a\to c)$, for an arbitrary $d$. By
the adjunction, $d\leq a\to(b\wedge c)$ is equivalent to $d\wedge a\leq
b\wedge c$. By the original property of the existence of the meets, this is
equivalent to ($d\wedge a\leq b$ and $d\wedge a\leq c$) and by the adjunction
again and using the properties of the meet, we reach $d\leq(a\to b)\wedge(a\to
c)$. It is clear that the adjunction reduces the internal version of the
existence of the binary meets to its original version. The examples of such
reductions abound. For instance, think about the property $(a\vee b)\to
c=(a\to c)\wedge(b\to c)$ for the Heyting implication as the internalization
of the existence of the binary joins or $(a\to(b\supset c))=(a\wedge b)\to c$,
as the internalization of the existence of the Heyting implication $\supset$.

Compared to the well-behaved Heyting implication, an abstract implication is
known to be rather ill-behaved. The reason, we believe, is the lack of the
adjunction and the natural reduction process it provides. Without a reduction
procedure, we are forced to select the internalized properties ourselves and
the choice can be quite artificial if we do not have a general guiding
principle in the selection process. For instance, internalizing the structure
of a bounded distributive lattice, one may wonder if the internalization of
both the existence of the binary meets and the binary joins, i.e., satisfying
$(a\to(b\wedge c))=(a\to b)\wedge(a\to c)$ and $(a\vee b)\to c=(a\to
c)\wedge(b\to c)$ is what one must expect or having one without the other is
also meaningful. The reader probably shares our feeling that the answer to
this problem is quite far from clear.
Apart from the importance of the reduction processes, there are also other and
probably more conceptual arguments in favor of the adjunctions. The most
important one is the role that the adjunction plays in specifying the meaning
of a logical constant. To explain, an adjuncton is nothing but a full pair of
introduction and elimination rules providing a full characterization of how
the constant can be introduced on the one hand and how it can be used on the
other. This full characterization specifies the behavior of the logical
constant which we can consider as the (proof-theoretic) meaning of the
constant. In this sense, the lack of the adjunction leads to an incomplete
determination of the meaning of a connective and it is no surprise that such a
connective is ill-behaved to some extent.

To overcome this lack of adjunction, [1] introduced $\nabla$-algebras222In
[1], $\nabla$-algebras are called temporal algebras and they are again based
on monoidal posets to also cover the substructural instances. as a
generalization of Heyting algebras importing many of their nice properties
into the realm of the abstract implications. Formally, a $\nabla$-algebra is a
tuple $(\mathsf{A},\nabla,\to)$, where $\mathsf{A}$ is a bounded lattice over
the set $A$, $\nabla:A\to A$ is a unary operation and $\to\,:A\times A\to A$
is a binary operation such that $\nabla(-)\wedge a\dashv a\to(-)$, i.e.,
$\nabla(-)\wedge a$ is left adjoint to $a\to(-)$, for any $a\in A$.
$\nabla$-algebras are the clear generalization of both Heyting algebras
($\nabla=id$) and bounded lattices ($\nabla a=0$ and $a\to b=1$). It is easy
to see that in any $\nabla$-algebra, $\to$ is an abstract implication
empowered by the adjunction to run a natural reduction process on the one hand
and provide a complete proof-theoretic meaning for the implication, on the
other. The main feature of $\nabla$-algebras, however, is their ability to
fuse the full generality of the abstract implications to the nice behavior of
the Heyting implications. To be more precise, $\nabla$-algebras provide not
only a nice family of implications but also a sufficiently general one
powerful enough to represent all abstract implications up to a correcting
factor, see [1] and also Theorem 3.20 in the present paper. Having this
representation theorem, it is then mathematically justified to employ the
strategy of studying the well-behaved $\nabla$-algebras in order to understand
all abstract implications. This is exactly the task that the present series of
two papers is devoted to. Before explaining how, let us complete the list of
motivations for $\nabla$-algebras by providing two other minor yet interesting
instances.

#### Intuitionistic Temporal Logics

Temporal logics form an interesting family of modal logics addressing the
temporal aspects of the natural language. The intuitionistic version of these
logics addressing the combinations of knowledge and various temporal
modalities including “past” and “present” [20, 17], “next” [16, 30],
“henceforth” [29] and their combinations [35, 7, 10] is also introduced and
investigated in the literature. The most basic system among these logics is
the one only consisting of one _existential past_ modality $\Diamond$ and one
_universal future_ modality $\Box$. Putting algebraically, the logic is
nothing but a _temporal Heyting algebra_ , i.e., a Heyting algebra augmented
with an adjunction $\Diamond\dashv\Box$ [18, 13]. Many extensions of temporal
Heyting algebras, their Sahlqvist correspondence theory and their canonicity
are studied, e.g. see [24, 14].
Having this temporal setting in mind, one can read $\nabla$-algebras as a
generalization of temporal Heyting algebras weakening the base from a Heyting
algebra to a bounded lattice and strengthening the unary $\Box$ to a binary
$\to$. Here, $\nabla a$ is interpreted similar to $\Diamond a$ as “ _$a$ was
true at some point in the past_” and $a\to b$ means “ _$a$ implies $b$, always
in the future_”. As expected, when the base lattice of a $\nabla$-algebra has
the Heyting structure, we regain our temporal Heyting algebras. The reason is
the fact that in the presence of the Heyting implication $\supset$, the
implication of a $\nabla$-algebra satisfies $a\to b=1\to(a\supset b)$.
Therefore, setting $\Box a=1\to a$, the structure of a Heyting
$\nabla$-algebra simplifies to a Heyting algebra augmented with the adjunction
$\nabla\dashv\Box$. Having this observation, it is safe to say that
$\nabla$-algebras genuinely generalize temporal Heyting algebras and hence
their study encompasses the algebraic study of the basic intuitionistic
temporal logic. However, it is also important to keep in mind that
$\nabla$-algebras are more general than temporal Heyting algebras as in lack
of the Heyting implication, the binary implication $\to$ is more expressive
and forces more structure than the unary $\Box$. To see why, compare the
structure of a $\nabla$-algebra to a bounded lattice augmented with an
adjunction $\nabla\dashv\Box$. Trivializing $\nabla$ to the identity function
turns them into a Heyting algebra and a bounded lattice, respectively, where
the former has far more structure than the latter.

#### The Logic of Dynamic Topological Systems

A dynamic topological system is a pair $(X,f)$, where $X$ is a topological
space formalizing the _state space_ of the system and $f:X\to X$ is a
continuous map encoding its _dynamism_ [2]. To describe the dynamic
topological systems, [6] enhanced the logical system $\mathsf{S4}$ by a “next”
modality $\bigcirc$, where the former described the topological space and the
latter captured the effect of the inverse image of the map $f$. Later, [33]
enriched the language further to make it expressive enough to address the
asymptotic behavior of the systems, as well. The logic turned out to be
undecidable [31]. In the quest of finding a rich enough decidable fragment and
following an unpublished suggestion of Kremer [32], Fernández-Duque [21]
introduced the intuitionistic version of the dynamic topological logic, where
$\mathsf{S4}$ is replaced by the intuitionistic propositional logic to
describe the topological state space. Inspired by [21], it is natural to claim
that a very basic algebraic setting to formalize the dynamic topological
system $(X,f)$ is a Heyting algebra representing the locale $\mathcal{O}(X)$
augmented with a modality $\nabla$ representing the map $f^{-1}$. To identify
the properties of this modality, by imitating the behavior of $f^{-1}$, we
expect $\nabla$ to preserve the finite meets and the arbitrary joins. The
former is easy to axiomatize algebraically. To capture the latter in an
elementary way, first note that as $f^{-1}$ preserves all the joins over the
complete lattice $\mathcal{O}(X)$, it must have a right adjoint $f_{*}$. Thus,
to reflect the behavior of $f^{-1}$ in an elementary way, it is enough to also
add $\Box$ to the signature to mimic the map $f_{*}$. Therefore, the structure
we are looking for is simply a Heyting algebra augmented with an adjunction
$\nabla\dashv\Box$. As we saw before, such a structure is nothing but a
Heyting $\nabla$-algebra, this time with the additional condition that
$\nabla$ must respect all the finite meets. Calling this property the
_normality_ condition, we can conclude that normal Heyting $\nabla$-algebras
provide an algebraic presentation for the dynamic topological systems. Using
this observation, one can expand the intuition to read any normal
$\nabla$-algebra (not necessarily Heyting) as some sort of dynamic system
where the base lattice captures the observables of the system and $\nabla$
encodes its dynamism.

#### Our Contribution

Inspired by the above motivations, in a series of two papers, we provide an
extensive algebro-topological study of different varieties of
$\nabla$-algebras. In the present paper, after covering the preliminary
concepts in Section 2 and introducing some varieties of $\nabla$-algebras in
Section 3, we study the structure of these varieties in Section 4 and provide
a characterization for subdirectly irreducible and simple normal distributive
$\nabla$-algebras. In Section 5, we cover the Dedekind-MacNeille completion of
$\nabla$-algebras to show how well-behaved the notion of a $\nabla$-algebra
is. We will also need this completion to prove stronger forms of completeness
in the sequel of the present paper. Section 6 is devoted to Kripke frames and
the usual canonical construction providing an interesting representation
theorem for distributive normal $\nabla$-algebras as the _dynamic posets_ ,
i.e, the posets equipped with an order-preserving map over them. The
representation then helps to prove the amalgamation property for some
varieties of normal distributive $\nabla$-algebras. This completes the scope
of the present paper. In its sequel, we introduce some logical systems for
which $\nabla$-algebras provide an algebraic semantics. We prove the deductive
interpolation property for some of these logics. We also provide Kripke and
topological semantics for them and prove a corresponding soundness and
completeness theorem. We will continue by providing a full duality theory for
the distributive $\nabla$-algebras, unifying Priestley and Esakia dualities as
the two instances of one duality theory. This duality theory then leads to a
corresponding spectral duality à la [8]. We will use the latter to provide a
ring-theoretic representation for normal distributive $\nabla$-algebras
interpreting the algebra as a _dynamic ring_ , i.e., a ring equipped with a
ring endomorphism.

##  2 Preliminaries

In this section, we will present the preliminary concepts and their
corresponding theorems that we need throughout the paper. In the algebraic
part that is our main emphasis, we will be quite extensive. In the topological
part, though, we only recall some useful points.

A _poset_ $\mathcal{P}=(P,\leq)$ is a pair of a set and a reflexive, anti-
symmetric and transitive binary relation $\leq\;\subseteq P^{2}$. By
$\mathcal{P}^{op}$, we mean the poset $(P,\geq)$, namely $P$ with the opposite
order. A subset $S\subseteq P$ is called a _downset_ , if it is downward
closed, i.e., for every $x\in S$ and any $y\in P$, if $y\leq x$, we have $y\in
S$. An _upset_ is defined dually. For any subset $S\subseteq P$, by its
downset, denoted by $\downarrow\\!\\!S$, we mean the least downset extending
$S$ and by the upset of $S$, denoted by $\uparrow\\!\\!S$, we mean the least
upset extending $S$. When $S=\\{a\\}$, we denote $\downarrow\\!\\!S$ and
$\uparrow\\!\\!S$ by $\downarrow\\!\\!a$ (or $(a]$) and $\uparrow\\!\\!a$ (or
$[a)$), respectively. The set of all upsets and downsets of $(P,\leq)$ are
denoted by $U(P,\leq)$ and $D(P,\leq)$, respectively. For any $S\subseteq P$,
if the greatest lower bound of $S$ exists, it is called the _meet_ of the
elements of $S$ and is denoted by $\bigwedge S$. If $S=\\{a,b\\}$, the meet
$\bigwedge S$ is usually denoted by $a\wedge b$. A poset is called _complete_
if for any set $S\subseteq P$, the meet $\bigwedge S$ exists. If the least
upper bound of $S$ exists, it is called the _join_ of the elements of $S$ and
is denoted by $\bigvee S$. If $S=\\{a,b\\}$, the join $\bigvee S$ is usually
denoted by $a\vee b$. In any complete poset all the joins also exist. A poset
is called a _meet semi-lattice_ , if for any $a,b\in P$, the meet $a\wedge b$
exists. It is called bounded if it also has a greatest element, denoted by
$1$. A meet semi-lattice is called a _lattice_ , if for any $a,b\in P$, the
join $a\vee b$ also exits. A lattice is called _bounded_ , if it has both the
greatest and the least elements, denoted by $1$ and $0$, respectively. A
bounded lattice is called _distributive_ , if $a\wedge(b\vee c)=(a\wedge
b)\vee(a\wedge c)$, for any $a,b,c\in P$. A bounded lattice $(P,\leq)$ is
called a _locale_ , if it is complete and $a\wedge\bigvee_{b\in
S}b=\bigvee_{b\in S}(a\wedge b)$, for any $a\in P$ and any $S\subseteq P$. We
will use the sanserif font as in $\mathsf{A}$ for the bounded lattices and for
brevity, when we are working with a bounded lattice $\mathsf{A}$, without any
further explanation, we use the normal $A$ as the base set of $\mathsf{A}$. A
subset of a bounded lattice is called a _filter_ , if it is an upset and
closed under all finite meets. The filters in the form $[a)$ are called the
_principal filters_. The set of all filters of the lattice $\mathsf{A}$ is
denoted by $\mathcal{F}(\mathsf{A})$. A filter is called _prime_ if $0\notin
P$ and $a\vee b\in P$ implies either $a\in P$ or $b\in P$. The set of all
prime filters of a lattice $\mathsf{A}$ is denoted by
$\mathcal{F}_{p}(\mathsf{A})$. A subset of $\mathsf{A}$ is called an _ideal_ ,
if it is a downset and closed under all finite joins. The ideals in the form
$(a]$ are called the _principal ideals_. The set of all ideals of a lattice
$\mathsf{A}$ is denoted by $\mathcal{I}(\mathsf{A})$. The following theorem is
a useful tool when the bounded lattice is distributive.

######  Theorem 2.1.

[19](Prime filter theorem) Let $\mathsf{A}$ be a distributive lattice, $F$ be
a filter and $I$ be an ideal such that $F\cap I=\varnothing$. Then there
exists a prime filter $P$ such that $F\subseteq P$ and $P\cap I=\varnothing$.

Let $(P,\leq_{P})$ and $(Q,\leq_{Q})$ be two posets and $f:P\to Q$ be a
function. It is called a _order-preserving map_ , if it preserves the order,
meaning $f(p)\leq_{Q}f(q)$ for any $p\leq_{P}q$. An order-preserving map is
called an _order embedding_ , if for any $p,q\in P$, the inequality
$f(p)\leq_{Q}f(q)$ implies $p\leq_{P}q$. An order-preserving map between two
meet semi-lattices is called a _meet semi-lattice map_ , if it preserves the
binary meets. Similarly, an order-preserving map is called a _bounded meet-
semilattice map_ , if it also preserves the greatest element. It is called a
lattice map, if it preserves both meets and joins and it is a _locale map_ if
it preserves all finite meets and all possible joins. For two order-preserving
maps $f:P\to Q$ and $g:Q\to P$, the map $f$ is called the _left adjoint_ for
$g$ (and $g$ is called the _right adjoint_ for $f$) denoted by _$f\dashv g$_
iff

$f(a)\leq_{Q}b\;\;\;\text{iff}\;\;\;a\leq_{P}g(b),$

for any $a\in P$ and $b\in Q$. In such a situation, the pair $(f,g)$ is called
an _adjunction_. We will use the following two easy theorems throughout the
paper.

######  Theorem 2.2.

[9] Let $(P,\leq_{P})$ and $(Q,\leq_{Q})$ be two posets and $f:P\to Q$ and
$g:Q\to P$ be two order-preserving maps such that $f\dashv g$. Then:

  * •

$fg(q)\leq_{Q}q$ and $p\leq_{P}gf(p)$, for any $p\in P$ and $q\in Q$.

  * •

$fgf(p)=f(p)$ and $gfg(q)=g(q)$, for any $p\in P$ and $q\in Q$.

  * •

$f$ is one-to-one iff $g$ is surjective iff $gf(p)=p$, for any $p\in P$.

  * •

$f$ is surjective iff $g$ is one-to-one iff $fg(q)=q$, for any $q\in Q$.

######  Theorem 2.3.

[9] (Adjoint functor theorem for posets) Let $(P,\leq_{P})$ be a complete
poset and $(Q,\leq_{Q})$ be a poset. Then an order-preserving map
$f:(P,\leq_{P})\to(Q,\leq_{Q})$ has a right (left) adjoint iff it preserves
all joins (meets).

Let $X$ be a topological space. We denote the locale of its open subsets by
$\mathcal{O}(X)$. A topological space is called $T_{0}$, if for any two
different points $x,y\in X$, there is an open set which contains one of these
points and not the other. It is called $T_{D}$, if for any $x\in X$, there is
an open $U$ such that $x\in U$ and $U-\\{x\\}$ is open, as well. A continuous
map is called a topological embedding if $f$ induces a homeomorphism between
$X$ and $f[X]$. The following provides a point-free version of surjectivity
and embeddingness.

######  Theorem 2.4.

[28] Let $X$ and $Y$ be two topological spaces and $f:X\to Y$ be a continuous
map. Then,

  * •

If $f$ is surjective, then $f^{-1}:\mathcal{O}(Y)\to\mathcal{O}(X)$ is one-to-
one. The converse is true, if $Y$ is $T_{D}$.

  * •

If $f$ is a topological embedding, then
$f^{-1}:\mathcal{O}(Y)\to\mathcal{O}(X)$ is surjective. The converse is also
true, if $X$ is $T_{0}$.

##  3 $\nabla$-Algebras

In this section, we first introduce $\nabla$-algebras as the main notion of
the present paper. Then, we present some interesting families of
$\nabla$-algebras and two canonical types of examples to connect them to basic
temporal Heyting algebras and dynamic topological systems. We then proceed by
proving some basic properties of the introduced families and showing that they
all form a variety. Finally, we recall the notion of an abstract implication
and its representation by $\nabla$-algebras. As already mentioned in
Introduction, this representation serves as the main motivation for
$\nabla$-algebras.

###  3.1 The Basics of $\nabla$-algebras

Let us start this subsection with the definition of a $\nabla$-algebra:

######  Definition 3.1.

Let $\mathsf{A}=(A,\wedge,\vee,0,1)$ be a bounded lattice with the lattice
order $\leq$. A tuple $\mathcal{A}=(\mathsf{A},\nabla,\to)$ is called a
$\nabla$-algebra if $\nabla c\wedge a\leq b$ is equivalent to $c\leq a\to b$,
for any $a,b,c\in A$. In any $\nabla$-algebra, $\Box a$ is defined as $1\to
a$.

######  Example 3.2.

Any bounded lattice $\mathsf{A}$ with the operations $\nabla$ and $\to$
defined by setting $\nabla a=0$ and $a\to b=1$, for any $a,b\in A$, forms a
$\nabla$-algebra, because

$0=\nabla c\wedge a\leq b\;\;\;\text{iff}\;\;\;c\leq a\to b=1.$

To have another example, any Heyting algebra with $\nabla a=a$ and $a\to
b=a\supset b$, where $\supset$ is the Heyting implication, forms a
$\nabla$-algebra. Therefore, $\nabla$-algebras are a common generalization of
the bounded lattices and the Heyting algebras.

Before moving to the more interesting examples, let us first introduce some
specific families of $\nabla$-algebras. Later, in Example 3.6 and Example 3.8,
we will see the concrete situations from which these families are abstracted.

######  Definition 3.3.

Let $\mathcal{A}=(\mathsf{A},\nabla,\to)$ be a $\nabla$-algebra:

$(D)$

If $\mathsf{A}$ is distributive, then the $\nabla$-algebra is called
_distributive_.

$(H)$

If $\mathsf{A}$ has the Heyting structure, then the $\nabla$-algebra is called
_Heyting_. This does not mean that $\to$ is the Heyting implication. It only
dictates that the Heyting implication exists over $\mathsf{A}$.

$(N)$

If $\nabla$ commutes with all finite meets, i.e., $\nabla 1=1$ and
$\nabla(a\wedge b)=\nabla a\wedge\nabla b$, for any $a,b\in A$, then the
$\nabla$-algebra is called _normal_.

$(R)$

If $a\leq\nabla a$, for any $a\in A$, the $\nabla$-algebra is called _right_.

$(L)$

If $\nabla a\leq a$, for any $a\in A$, the $\nabla$-algebra is called _left_.

$(Fa)$

If $\nabla$ is surjective, the $\nabla$-algebra is called _faithful_.

$(Fu)$

If $\Box$ is surjective, the $\nabla$-algebra is called _full_.

######  Remark 3.4.

The Heyting implication is a structure and not a mere property. Therefore,
“Heyting $\nabla$-algebra” is an ambiguous notion, as it is not clear whether
we include the Heyting implication in the signature of the algebra or not. To
solve this ambiguity, when we mean a $\nabla$-algebra that is also Heyting, we
call it “ _Heyting $\nabla$-algebra_” and when we mean an algebra in the form
$(\mathsf{A},\nabla,\to,\supset)$, where $(\mathsf{A},\nabla,\to)$ is a
$\nabla$-algebra and $\supset$ is the Heyting implication over $\mathsf{A}$,
we call the structure “ _explicitly Heyting $\nabla$-algebra_”. This
difference in the signature is important when we investigate the algebraic or
categorical properties of the algebras.

######  Definition 3.5.

For any $C\subseteq\\{D,H,N,R,L,Fa,Fu\\}$, by $\mathcal{V}(C)$ we mean the
class of all $\nabla$-algebras with the properties described in the set $C$.
For instance, $\mathcal{V}(\\{N,D\\})$ is the class of all normal distributive
$\nabla$-algebras. Sometimes, for simplicity, we omit the brackets. For
instance, we write $\mathcal{V}(N,D)$ for $\mathcal{V}(\\{N,D\\})$ and if
$X\in\\{D,H,N,R,L,Fa,Fu\\}$, we write $\mathcal{V}(X,C)$ for
$\mathcal{V}(\\{X\\}\cup C)$. By $\mathcal{V}_{H}(C)$, we mean the class of
all explicitly Heyting $\nabla$-algebras satisfying the conditions in $C$. For
two $\nabla$-algebras
$\mathcal{A}=(\mathsf{A},\nabla_{\mathcal{A}},\to_{\mathcal{A}})$ and
$\mathcal{B}=(\mathsf{B},\nabla_{\mathcal{B}},\to_{\mathcal{B}})$, by a
_$\nabla$ -algebra morphism_, we mean a bounded lattice morphism
$f:\mathsf{A}\to\mathsf{B}$ that also preserves $\nabla$ and $\to$, meaning
that $f(\nabla_{\mathcal{A}}a)=\nabla_{\mathcal{B}}f(a)$ and
$f(a\to_{\mathcal{A}}b)=f(a)\to_{\mathcal{B}}f(b)$, for any $a,b\in A$. If
both $\nabla$-algebras are explicitly Heyting and $f$ also preserves the
Heyting implication, it is called a _Heyting $\nabla$-algebra morphism_. A
$\nabla$-algebra morphism is called an _embedding_ if it is injective. For any
$C\subseteq\\{D,H,N,R,L,Fa,Fu\\}$, the class $\mathcal{V}(C)$ of
$\nabla$-algebras together with the $\nabla$-algebra morphisms forms a
category, denoted by $\mathbf{Alg}_{\nabla}(C)$. Similarly, the class
$\mathcal{V}_{H}(C)$ of explicitly Heyting $\nabla$-algebras with Heyting
morphisms forms a category, denoted by $\mathbf{Alg}^{H}_{\nabla}(C)$.

The following two examples are borrowed from [1] to provide some natural
families of $\nabla$-algebras.

######  Example 3.6.

_(Dynamic Topological Systems)_ Let $X$ be a topological space and $f:X\to X$
be a continuous function. Then, the pair $(X,f)$ is called a _dynamic
topological system_. If $f$ is a topological embedding (resp. surjection), the
dynamic topological system is called _faithful_ (resp. _full_). For any
dynamic topological system $(X,f)$, define $\to_{f}$ over $\mathcal{O}(X)$ by
$U\to_{f}V=f_{*}(int(U^{c}\cup V))$, where $int$ is the interior operation,
$U^{c}$ is the complement of $U$ and $f_{*}:\mathcal{O}(X)\to\mathcal{O}(X)$
is the right adjoint of $f^{-1}$. Note that using Theorem 2.3, the map $f_{*}$
exists, as $f^{-1}$ preserves the arbitrary unions and $\mathcal{O}(X)$ is
complete. Then, the structure $(\mathcal{O}(X),f^{-1},\to_{f})$ is a normal
Heyting $\nabla$-algebra, simply because for any $U,V,W\in\mathcal{O}(X)$, we
have

$f^{-1}(W)\cap U\subseteq V\;\;\;\text{iff}\;\;\;W\subseteq
f_{*}(int(U^{c}\cup V))=U\to_{f}V,$

and $f^{-1}$ commutes with finite intersections. It is also worth mentioning
that adding the Heyting implication $\supset$ to the structure results in the
explicitly Heyting normal $\nabla$-algebra
$(\mathcal{O}(X),f^{-1},\to_{f},\supset)$. Moreover, using Theorem 2.2 and
Theorem 2.4, we can observe that if $(X,f)$ is full, i.e., $f$ is surjective,
then the algebra $(\mathcal{O}(X),f^{-1},\to_{f})$ is full, as the
surjectivity of $f$ implies the injectivity of $\nabla=f^{-1}$ and hence the
surjectivity of $f_{*}$. The converse also holds if $X$ is $T_{D}$. In
addition, if $(X,f)$ is faithful, i.e., $f$ is a topological embedding, then
the $\nabla$-algebra $(\mathcal{O}(X),f^{-1},\to_{f})$ is faithful, as being
an embedding implies the surjectivity of $\nabla=f^{-1}$. The converse also
holds if $X$ is $T_{0}$.

As shown in Example 3.6, any dynamic topological system gives rise to a normal
$\nabla$-algebra over a locale. The converse is not necessarily true, as the
locale may not be the locale of the opens of a topological space. However,
this is the only obstacle and moving to the point-free setting, these
$\nabla$-algebras actually coincide with the _point-free dynamic topological
systems_ , i.e., the pairs $(\mathscr{X},F)$ where $\mathscr{X}$ is a locale
and $F:\mathscr{X}\to\mathscr{X}$ is a locale map. The reason simply is the
fact that in any normal $\nabla$-algebra $(\mathscr{X},\nabla,\to)$ over the
locale $\mathscr{X}$, the $\nabla$ is both join-preserving and finite meet-
preserving and hence it is a locale map over $\mathscr{X}$ and conversely, as
soon as $\nabla$ is a locale map over $\mathscr{X}$, its adjoint, i.e., $\to$
exists by the adjoint functor theorem, Theorem 2.3 and it is unique.
Therefore, the normal $\nabla$-algebra $(\mathscr{X},\nabla,\to)$ over the
locale $\mathscr{X}$ is nothing but the point-free dynamic topological system
$(\mathscr{X},\nabla)$. Having that observed, then $(Fa)$ is the point-free
way to state that the dynamism $\nabla$ is a topological embedding, while
$(Fu)$ is the point-free version of the surjectivity of $\nabla$. Notice that
$(N)$, $(Fa)$ and $(Fu)$ together axiomatize the point-free situation where
the dynamism is actually a homeomorphism.

######  Remark 3.7.

Faithfulness is an interesting condition to consider even if the
$\nabla$-algebra does not correspond to any dynamic topological system or its
base lattice is not even a Heyting algebra. The reason is the pure
implicational role that the faithfulness plays. To be more precise, a
$\nabla$-algebra is faithful iff $c\to a\leq c\to b$ implies $c\wedge a\leq
b$, for any $a,b,c\in A$, see Theorem 3.13. This property is known to
logicians for its philosophical and technical roles, see for instance [3, 4].

######  Example 3.8.

_(Kripke Frames)_ Let $(W,\leq)$ be a poset. By a _Kripke frame_ , we mean a
tuple $\mathcal{K}=(W,\leq,R)$, where $R$ is a binary relation over $W$
compatible with the partial order, i.e., $\leq\circ\,R\,\circ\leq\,\subseteq
R$ or more explicitly, if $k^{\prime}\leq k$, $l\leq l^{\prime}$ and $(k,l)\in
R$ then $(k^{\prime},l^{\prime})\in R$, for any $k,k^{\prime},l,l^{\prime}\in
W$:

${k}$${l}$${{k^{\prime}}}$${{l^{\prime}}}$$\scriptstyle{\leq}$$\scriptstyle{R}$$\scriptstyle{\leq}$$\scriptstyle{R}$

To any Kripke frame, we can assign a canonical Heyting $\nabla$-algebra,
encoding its structure algebraically. Set $\mathscr{X}$ as the locale of all
upsets of $(W,\leq)$ and define $\nabla:\mathscr{X}\to\mathscr{X}$ as
$\nabla_{\mathcal{K}}U=\\{x\in W\mid\exists y\in U,(y,x)\in R\\}$ and
$U\to_{\mathcal{K}}V=\\{x\in W\mid\forall y\in W[(x,y)\in R\wedge y\in
U\Rightarrow y\in V]\\}$. It is easy to see that
$(\mathscr{X},\nabla_{\mathcal{K}},\to_{\mathcal{K}})$ is a Heyting
$\nabla$-algebra and hence
$(\mathscr{X},\nabla_{\mathcal{K}},\to_{\mathcal{K}},\supset)$ is an
explicitly Heyting $\nabla$-algebra, where $\supset$ is the usual Heyting
implication, i.e., $U\supset V=\\{x\in W\mid\forall y\in W[(x\leq y)\wedge
y\in U\Rightarrow y\in V]\\}$. It is also easy to see that the
$\nabla$-algebra $(\mathscr{X},\nabla_{\mathcal{K}},\to_{\mathcal{K}})$ is
right (resp. left) if $R$ is reflexive (resp. $R\subseteq\,\leq$).

One can read a Kripke frame as a very basic intuitionistic temporal setting,
where the set $W$ is the state space and the relations $\leq$ and $R$ are
capturing the growth of the knowledge and time over $W$, respectively. Notice
that by this interpretation, the reflexivity condition on $R$ simply says that
the order of time is reflexive while the condition $R\subseteq\,\leq$ means
that the growth of time implies the growth of knowledge. Having such a
temporal setting, the $\nabla$-algebra constructed in Example 3.8 encodes the
structure that the intuitionistic temporal setting imposes on the
propositions. Apart from being a Heyting algebra, the structure is simply the
pair of the _existential past_ modality $\nabla$ and the _universal future_
modality $\to$.

######  Remark 3.9.

Left and right conditions are interesting even if the $\nabla$-algebra does
not correspond to any Kripke frame or its base lattice is not even a Heyting
algebra. The reason again is the pure implicational role that these properties
play. To be more precise, the left $\nabla$-algebras are the ones where the
introduction rule for the implication is admissible, i.e., $c\wedge a\leq b$
implies $c\leq a\to b$, see Theorem 3.12, and the right $\nabla$-algebras are
the ones where the modus ponens is admissible, i.e., $(a\to b)\wedge a\leq b$,
see Theorem 3.11. Such implications are investigated in the literature for
some philosophical [3, 4, 36] and technical reasons [40].

In the rest of this subsection, we will investigate some of the basic
properties of $\nabla$-algebras. We will then use these properties to show
that for any $C\subseteq\\{D,N,R,L,Fa,Fu\\}$, the classes $\mathcal{V}(C)$ and
$\mathcal{V}_{H}(C)$ form a variety.

######  Theorem 3.10.

Let $(\mathsf{A},\nabla,\to)$ be a $\nabla$-algebra. Then:

$(i)$

The operations $\nabla:(A,\leq)\to(A,\leq)$ and
$\to:(A,\leq)^{op}\times(A,\leq)\to(A,\leq)$ are order-preserving. Therefore,
it is possible to define a $\nabla$-algebra as a structure
$(\mathsf{A},\nabla,\to)$, where $\mathsf{A}$ is a bounded lattice and for any
$a\in A$, the operations $\nabla$ and $a\to(-)$ are two order-preserving maps
satisfying the adjunction $\nabla(-)\wedge a\dashv a\to(-)$.

$(ii)$

$\nabla\dashv\Box$. Therefore, in any $\nabla$-algebra, $\nabla$ (resp.
$\Box$) preserves all the existing joins (resp. meets), especially, $\nabla
0=0$, $\nabla(a\vee b)=\nabla a\vee\nabla b$, $\Box 1=1$ and $\Box(a\wedge
b)=\Box a\wedge\Box b$, for any $a,b\in A$.

$(iii)$

$\nabla(a\to b)\wedge a\leq b$, $\nabla\Box a\leq a$ and $a\leq\Box\nabla a$,
for any $a,b\in A$.

###### Proof.

For $(i)$, if $c\leq d$, for any $b\in A$, we have

$\nabla d\leq b\;\;\;\text{implies}\;\;\;d\leq 1\to
b\;\;\;\text{implies}\;\;\;c\leq 1\to b\;\;\;\text{implies}\;\;\;\nabla c\leq
b.$

Setting $b=\nabla d$, we reach $\nabla c\leq\nabla d$. A similar argument
works for $\to$. The rest are trivial. ∎

######  Theorem 3.11.

(Right) Let $\mathcal{A}=(\mathsf{A},\nabla,\to)$ be a $\nabla$-algebra. Then,
the following are equivalent:

$(i)$

$b\leq\nabla b$, for any $b\in A$.

$(ii)$

$a\wedge(a\to b)\leq b$, for any $a,b\in A$.

$(iii)$

$\Box b\leq b$, for any $b\in A$.

###### Proof.

To prove $(ii)$ from $(i)$, apply Theorem 3.10 to have $a\wedge(a\to b)\leq
a\wedge\nabla(a\to b)\leq b$. To prove $(iii)$ from $(ii)$, put $a=1$ in
$(ii)$. To prove $(i)$ from $(iii)$, by Theorem 3.10, we have $b\leq\Box\nabla
b\leq\nabla b$. ∎

######  Theorem 3.12.

(Left) Let $\mathcal{A}=(\mathsf{A},\nabla,\to)$ be a $\nabla$-algebra. Then,
the following are equivalent:

$(i)$

$\nabla b\leq b$, for any $b\in A$.

$(ii)$

$c\wedge a\leq b$ implies $c\leq a\to b$, for any $a,b,c\in A$.

$(iii)$

$b\leq\Box b$, for any $b\in A$.

###### Proof.

To prove $(ii)$ from $(i)$, if $c\wedge a\leq b$, then $\nabla c\wedge a\leq
b$ and hence $c\leq a\to b$, by adjunction. To prove $(iii)$ from $(ii)$, put
$a=1$ and $c=b$ in $(ii)$. To prove $(i)$ from $(iii)$, use the adjunction
$\nabla\dashv\Box$ in Theorem 3.10. ∎

######  Theorem 3.13.

(Faithfulness) Let $\mathcal{A}=(\mathsf{A},\nabla,\to)$ be a
$\nabla$-algebra. Then, the following are equivalent:

$(i)$

$\nabla\Box a=a$, for any $a\in A$.

$(ii)$

$\nabla$ is surjective.

$(iii)$

$a\wedge\nabla(a\to b)=a\wedge b$, for any $a,b\in A$.

$(iv)$

$c\to a\leq c\to b$ implies $c\wedge a\leq b$, for any $a,b,c\in A$.

$(v)$

$\Box$ is an order embedding, i.e., if $\Box a\leq\Box b$ then $a\leq b$, for
any $a,b\in A$.

###### Proof.

It is clear that $(i)$ implies $(ii)$. To prove $(iii)$ from $(ii)$, by
Theorem 3.10, we have $a\wedge\nabla(a\to b)\leq b$. Therefore, it is enough
to show that $b\leq\nabla(a\to b)$. Since $\nabla$ is surjective, there exists
$c\in A$ such that $b=\nabla c$. Since $b\wedge a\leq b$, we have $\nabla
c\wedge a\leq b$ which implies $c\leq a\rightarrow b$ and hence, $b=\nabla
c\leq\nabla(a\rightarrow b)$, by the monotonicity of $\nabla$ proved in
Theorem 3.10. To prove $(iv)$ from $(iii)$, assume $c\to a\leq c\to b$. Hence,
$c\wedge\nabla(c\to a)\leq c\wedge\nabla(c\to b)$, again by the the
monotonicity of $\nabla$. Therefore, using $(iii)$, we have $c\wedge a\leq b$.
To reach $(v)$ from $(iv)$, it is just enough to set $c=1$ in $(iv)$. And
finally, to prove $(i)$ from $(v)$, use Theorem 2.2. ∎

######  Remark 3.14.

Note that $\nabla 1=1$, in any faithful $\nabla$-algebra. Because,
$1=\nabla\Box 1=\nabla(1\to 1)=\nabla 1$. As a consequence, $a\to b=1$ iff
$a\leq b$, because $1\leq a\to b$ iff $\nabla 1\wedge a\leq b$ iff $a\leq b$.

######  Corollary 3.15.

Any faithful $\nabla$-algebra has a Heyting structure. Consequently, any
faithful $\nabla$-algebra is distributive.

###### Proof.

Define $a\supset b=\nabla(a\to b)$, for any $a,b\in A$. We claim that
$\supset$ is the Heyting implication. To prove, if $c\wedge a\leq b$, then by
part $(i)$ of Theorem 3.13, we have $\nabla\Box c=c$. Hence, $\nabla\Box
c\wedge a\leq b$ which implies $\Box c\leq a\to b$ and then $c=\nabla\Box
c\leq\nabla(a\to b)$, by the monotonicity of $\nabla$, Theorem 3.10.
Conversely, if $c\leq\nabla(a\to b)$, then $c\wedge a\leq\nabla(a\to b)\wedge
a\leq b$, by Theorem 3.10. ∎

######  Theorem 3.16.

(Fullness) Let $\mathcal{A}=(\mathsf{A},\nabla,\to)$ be a $\nabla$-algebra.
Then, the following are equivalent:

$(i)$

$\Box\nabla a=a$, for any $a\in A$.

$(ii)$

$\Box$ is surjective.

$(iii)$

$\nabla$ is an embedding, i.e., if $\nabla a\leq\nabla b$ then $a\leq b$, for
any $a,b\in A$.

###### Proof.

See Theorem 2.2. ∎

######  Theorem 3.17.

The following set of equalities and inequalities axiomatize the class of all
$\nabla$-algebras:

$(1)$

The set of equalities axiomatizing the variety of bounded lattices,

$(2)$

$(a\wedge b)\rightarrow a=1$.

$(3)$

$\nabla(a\wedge b)\leq\nabla a\wedge\nabla b$.

$(4)$

$a\wedge\nabla(a\rightarrow b)\leq b$.

$(5)$

$c\wedge[(\nabla c\wedge a)\to b]\leq a\rightarrow b$.

Therefore, the class $\mathcal{V}$ is a variety. More generally, for any
subset $C\subseteq\\{D,N,R,L,Fa,Fu\\}$, the classes $\mathcal{V}(C)$ and
$\mathcal{V}_{H}(C)$ are varieties.

###### Proof.

To prove the soundness of the axiomatization, we have to show that all the
axioms in $(1)-(5)$ are satisfied in any $\nabla$-algebra. The axioms in $(1)$
hold as any $\nabla$-algebra is a bounded lattice and $(2)-(4)$ are trivially
satisfied using the adjunction and the monotonicity of $\nabla$, see Theorem
3.10. For $(5)$, by the adjunction, it is enough to show that
$\nabla[c\wedge[(\nabla c\wedge a)\to b]]\wedge a\leq b$. By the monotonicity
of $\nabla$, we have $\nabla[c\wedge[(\nabla c\wedge a)\to b]]\leq\nabla
c\wedge\nabla[(\nabla c\wedge a)\to b]$ and since

$\nabla c\wedge\nabla[(\nabla c\wedge a)\to b]\wedge a=\nabla[(\nabla c\wedge
a)\to b]\wedge(\nabla c\wedge a)\leq b,$

we are done. For the completeness, assume that $(\mathsf{A},\nabla,\to)$
satisfies $(1)-(5)$. First, notice that by the axioms in $(1)$, $\mathsf{A}$
is a bounded lattice. Secondly, note that if $x\leq y$ then $x\to y=1$, for
any $x,y\in A$, as $x\leq y$ implies $x=x\wedge y$ which by the axiom $(2)$
implies $x\to y=(x\wedge y)\to y=1$. Thirdly, notice that $\nabla$ is order-
preserving, as if $x\leq y$ then $x\wedge y=x$. Hence, by axiom $(3)$, we have
$\nabla x=\nabla(x\wedge y)\leq\nabla x\wedge\nabla y$, which implies $\nabla
x\leq\nabla y$. Now, to prove the adjunction condition of a $\nabla$-algebra,
if $\nabla c\wedge a\leq b$ then $(\nabla c\wedge a)\to b=1$ and hence, by the
axiom $(5)$, we have $c\leq a\rightarrow b$. Conversely, if $c\leq
a\rightarrow b$, then since $\nabla$ is order-preserving, $\nabla
c\leq\nabla(a\rightarrow b)$. Therefore, $\nabla c\wedge a\leq\nabla(a\to
b)\wedge a$. Finally, by the axiom $(4)$, we reach $\nabla c\wedge a\leq b$.
This completes the first part of the claim. For the second part, it is enough
to note that in the presence of the lattice axioms, the inequalities $(2)-(5)$
can be rewritten as some equalities. Hence, $\mathcal{V}$ is a variety.

For the third part, it is enough to axiomatize any property in the set
$\\{D,N,R,L,Fa,Fu\\}$ by an equality. The only non-trivial cases are for
$(Fa)$ and $(Fu)$ for which one can use Theorem 3.13 and Theorem 3.16. Hence,
for any $C\subseteq\\{D,N,R,L,Fa,Fu\\}$, the class $\mathcal{V}(C)$ is a
variety. The case for $\mathcal{V}_{H}(C)$ is also easy, using the fact that
being a Heyting algebra is definable by equalities using a new symbol for the
Heyting implication. ∎

######  Remark 3.18.

Note that Theorem 3.17 excludes the classes $\mathcal{V}(C,H)$, for any
$C\subseteq\\{D,N,R,L,Fa,Fu\\}$. The reason is the lack of the Heyting
implication in the signature of the Heyting $\nabla$-algebras. This operation
is usually required in the axiomatizations that only use the equalities. For
instance, one can show that $\mathcal{V}(H)$ is not a variety. The reason
simply is the existence of $\nabla$-algebras $\mathcal{A}$ and $\mathcal{B}$
and a $\nabla$-algebra embedding $i:\mathcal{A}\to\mathcal{B}$ such that
$\mathcal{B}$ is Heyting while $\mathcal{A}$ is not. To have a concrete
example, set $\mathcal{B}=(P(\mathbb{N}),\nabla,\to)$, where $P(\mathbb{N})$
is a boolean algebra of all subsets of $\mathbb{N}$, $\nabla U=\varnothing$
and $U\to V=\mathbb{N}$, for any $U,V\in P(\mathbb{N})$,
$\mathcal{A}=(F(\mathbb{N})\cup\\{\mathbb{N}\\},\nabla,\to)$, where
$F(\mathbb{N})$ is the set of all finite subsets of $\mathbb{N}$ and $\nabla$
and $\to$ are as in $\mathcal{B}$ and $i:\mathcal{A}\to\mathcal{B}$ is simply
the inclusion function. Having said that, it is also worth mentioning that
there are some cases where the conditions in $C$ imply the existence of the
Heyting structure and hence $\mathcal{V}(C,H)=\mathcal{V}(C)$ is a variety.
For instance, consider the cases where $Fa\in C$ and note that any faithful
$\nabla$-algebra is Heyting by Corollary 3.15.

###  3.2 Abstract Implications

In this subsection, we will recall the abstract implications and their
representations by the $\nabla$-algebras.

######  Definition 3.19.

Let $\mathsf{A}=(A,\wedge,1)$ be a bounded meet semi-lattice and $\leq$ be its
meet-semilattice order. A binary order-preserving operation $\to$ from
$(A,\leq)^{op}\times(A,\leq)$ to $(A,\leq)$ is called an _implication_ , if
for any $a,b,c\in A$:

  * $\bullet$

_(internal reflexivity)_ $a\to a=1$,

  * $\bullet$

_(internal transitivity)_ $(a\to b)\wedge(b\to c)\leq a\to c$.

The pair $\mathcal{A}=(\mathsf{A},\to)$ is called a _strong algebra_ (short
for strong enough to internalize its order). An implication is called _meet-
internalizing_ if $a\to(b\wedge c)=(a\to b)\wedge(a\to c)$ and _join-
internalizing_ (when $\mathsf{A}$ is also a bounded lattice) if $(a\vee b)\to
c=(a\to c)\wedge(b\to c)$, for any $a,b,c\in A$. In any strong algebra, $\Box
a$ is an abbreviation for $1\to a$. If
$\mathcal{A}=(\mathsf{A},\to_{\mathcal{A}})$ and
$\mathcal{B}=(\mathsf{B},\to_{\mathcal{B}})$ are two strong algebras, by a
_strong algebra morphism_ , we mean a map $f:A\to B$, preserving the order,
all the finite meets and the implication. It is called an _embedding_ if it is
also an order embedding.

The following theorem ensures that any $\nabla$-algebra provides an
implication while such well-behaved implications are general enough to
represent all abstract implications. A weaker version of the second part first
appeared in the unpublished draft of the present paper and then generalized in
[1] to its current form.

######  Theorem 3.20.

$(i)$

Let $(\mathsf{A},\nabla,\to)$ be a $\nabla$-algebra. Then, $\to$ is a meet-
internalizing implication and if $\mathsf{A}$ is distributive, it is join-
internalizing, as well.

$(ii)$

Let $(\mathsf{A},\to_{\mathcal{A}})$ be a strong algebra. Then, there exists a
locale $\mathscr{X}$, a $\nabla$-algebra
$(\mathscr{X},\nabla,\to_{\mathscr{X}})$, an order-preserving map
$F:\mathscr{X}\to\mathscr{X}$ and a bounded meet semi-lattice embedding
$i:\mathsf{A}\to\mathscr{X}$ such that

$i(a\to_{\mathcal{A}}b)=F(i(a))\to_{\mathscr{X}}F(i(b)),$

for any $a,b\in A$. Moreover, if $\to_{\mathcal{A}}$ is meet-internalizing,
then $F$ can be set as the identity function and hence $i$ becomes a strong
algebra morphism. If $\mathsf{A}$ is also distributive and $\to_{\mathcal{A}}$
is join-internalizing, then $i$ can be set as a bounded lattice morphism.

###### Proof.

For $(i)$, first, notice that if $a\leq b$, then $\nabla 1\wedge a\leq b$
which by adjunction implies $1\leq a\to b$ and hence $a\to b=1$. Now, as a
special case, since $a\leq a$, we have $a\to a=1$ which proves the internal
reflexivity. For the internal transitivity, let $d\in A$ be an arbitrary
element satisfying $d\leq(a\to b)\wedge(b\to c)$. Therefore, $d\leq a\to b$
and $d\leq b\to c$. By the adjunction, $\nabla d\wedge a\leq b$ and $\nabla
d\wedge b\leq c$. Hence, $\nabla d\wedge a\leq c$. By the adjunction again,
$d\leq a\to c$. As $d$ is arbitrary, we have $(a\to b)\wedge(b\to c)\leq(a\to
c)$. To show that $\to$ is increasing (resp. decreasing) in its succedent
(antecedent), let $a^{\prime}\leq a$ and $b\leq b^{\prime}$. Then, by the
first observation, $(a^{\prime}\to a)=(b\to b^{\prime})=1$. Therefore, by the
internal transitivity, we have

$(a\to b)=(a^{\prime}\to a)\wedge(a\to b)\wedge(b\to
b^{\prime})\leq(a^{\prime}\to b^{\prime}).$

To show that $\to$ is meet-internalizing, note that for any $a\in A$, the
operation $a\to(-)$ has a left adjoint and hence preserves all finite meets.
To prove that $\to$ is join-internalizing, for any arbitrary $d\in A$,
consider the following equivalences:

$d\leq(a\vee b)\to c\quad\text{iff}\quad\nabla d\wedge(a\vee b)\leq
c\quad\text{iff}\quad(\nabla d\wedge a)\vee(\nabla d\wedge b)\leq
c\quad\text{iff}$ $[\nabla d\wedge a\leq c\;\;\&\;\;\nabla d\wedge b\leq
c]\quad\text{iff}\quad[d\leq a\to c\;\;\&\;\;d\leq b\to
c]\quad\text{iff}\quad$ $d\leq(a\to c)\wedge(b\to c).$

Therefore, as $d$ is arbitrary, we reach $(a\vee b)\to c=(a\to c)\wedge(b\to
c)$.

For the first part of $(ii)$, we refer the reader to Theorem 8 in [1] that
proves a generalized version of our claim for monoidal posets rather than meet
semi-lattices. The proof also works verbatim here. For the second part, the
reader is referred to Theorem 17 in [1]. ∎

To complete the relationship between the strong algebras and the
$\nabla$-algebras, notice that Theorem 3.20 just ensures that any meet-
internalizing abstract implication is the implication of a $\nabla$-algebra,
if we enlarge the bounded meet-semilattice base to a locale. However, without
the enlargement part, the claim may not hold, even if the base is already a
locale. In the following, working over locales, we will provide a
characterization for the implications that come from the $\nabla$-algebras.

######  Theorem 3.21.

Let $\mathscr{X}$ be a locale and $(\mathscr{X},\to)$ be a strong algebra.
Then, the following are equivalent:

$(i)$

There is an operation $\nabla:\mathscr{X}\to\mathscr{X}$ such that
$(\mathscr{X},\nabla,\to)$ is a $\nabla$-algebra.

$(ii)$

The operation $\to$ internalizes both the arbitrary meets and the Heyting
implication, where the former means $a\to\bigwedge_{i\in
I}b_{i}=\bigwedge_{i\in I}(a\to b_{i})$, for any $a\in\mathscr{X}$ and any
family $\\{b_{i}\\}_{i\in I}$ of the elements of $\mathscr{X}$ and the latter
means $a\to(b\supset c)=a\wedge b\to c$, for any $a,b,c\in\mathscr{X}$, where
$\supset$ is the Heyting implication of $\mathscr{X}$.

$(iii)$

The operation $\Box$ preserves all arbitrary meets and for any
$b,c\in\mathscr{X}$, we have $b\to c=\Box(b\supset c)$, where $\supset$ is the
Heyting implication of $\mathscr{X}$.

###### Proof.

To prove $(ii)$ from $(i)$, since $\nabla(-)\wedge a\dashv a\to(-)$, the
operation $a\to(-)$ must preserve all arbitrary meets. Moreover, for any
$d\in\mathscr{X}$, we have the following equivalences: $d\leq a\to(b\supset
c)$ iff $\nabla d\wedge a\leq b\supset c$ iff $\nabla d\wedge a\wedge b\leq c$
iff $d\leq a\wedge b\to c$. Therefore, $a\to(b\supset c)=a\wedge b\to c$. To
prove $(iii)$ from $(ii)$, just set $a=1$ in both equations. Finally, to prove
$(i)$ from $(iii)$, since $\Box$ preserves all meets and $\mathscr{X}$ is
complete, by the adjoint functor theorem, Theorem 2.3, $\Box$ has a left
adjoint. Call it $\nabla$. As

$\nabla d\wedge b\leq c\;\;\;\text{iff}\;\;\;\nabla d\leq b\supset
c\;\;\;\text{iff}\;\;\;d\leq\Box(b\supset c)\;\;\;\text{iff}\;\;\;d\leq b\to
c,$

it is clear that this $\nabla$ works. ∎

In the following, we will provide an example of a locale $\mathscr{X}$ and a
join- and meet-internalizing implication $\to$ such that $a\to(-)$ preserves
all the meets, for any $a\in\mathscr{X}$, while it does not internalize the
Heyting implication and hence is not a part of a $\nabla$-algebra.

######  Example 3.22.

Consider the set $\\{a,b\\}$ and define $\leq$ as the partial order generated
by the inequality $a\leq b$. Define $f:\\{a,b\\}\to\\{a,b\\}$ as $f(a)=f(b)=a$
and set $X$ as the topological space of the upsets of $\\{a,b\\}$. Hence,
$\mathcal{O}(X)$ looks like:

${{\\{a,b\\}}}$${{\\{b\\}}}$${\varnothing}$

As $f$ is order-preserving, it is also continuous. Therefore, $f^{-1}$ maps
$\mathcal{O}(X)$ into $\mathcal{O}(X)$. Define $U\to V=f^{-1}(U)\supset
f^{-1}(V)$, where $\supset$ is the Heyting implication of $\mathcal{O}(X)$. As
$f^{-1}$ is order-preserving, it is easy to check that $\to$ is an implication
on $\mathcal{O}(X)$ and as $f^{-1}$ preserves the arbitrary unions and
intersections, it is also possible to show that $\to$ is both meet- and join-
internalizing. Moreover, as $X$ is finite, any meet is a finite meet.
Therefore, the operation $U\to(-)$ is meet-preserving, for any
$U\in\mathcal{O}(X)$. However, $\to$ does not internalize the Heyting
implication and hence there is no $\nabla$ to make
$(\mathcal{O}(X),\nabla,\to)$ a $\nabla$-algebra. Assuming otherwise, we must
have $f^{-1}(U)\supset f^{-1}(V)=U\to V=\Box(U\supset V)=f^{-1}(U\supset V)$,
for any opens $U$ and $V$ of $X$. Set $U=\\{b\\}$ and $V=\varnothing$. Since
$f^{-1}(\\{b\\})=\varnothing$, we have $f^{-1}(\\{b\\})\supset
f^{-1}(\varnothing)=X$, while $(\\{b\\}\supset\varnothing)=\varnothing$ and
hence $f^{-1}(\\{b\\}\supset\varnothing)=\varnothing$. Therefore,
$f^{-1}(U\supset V)\neq f^{-1}(U)\supset f^{-1}(V)$ which is a contradiction.

##  4 Subdirectly irreducible and Simple Normal Distributive $\nabla$-algebras

Let us recall some basic definitions from universal algebra specified to the
setting of $\nabla$-algebras. Let $\mathcal{A}=(\mathsf{A},\nabla,\to)$ be a
$\nabla$-algebra. A binary relation $\theta\subseteq A\times A$ is called a
_congruence relation_ if it is an equivalence relation compatible with all the
algebraic operations in the signature, namely the finite meets, the finite
joins, $\nabla$ and $\to$. We denote the set of all congruence relations of
$\mathcal{A}$ by $\Theta(\mathcal{A})$. Any $\nabla$-algebra has two trivial
congruence relations, namely the equality and the whole set $A\times A$. A
$\nabla$-algebra is called _simple_ , if it has no nontrivial congruence
relation and it is called _subdirectly irreducible_ , if it is either trivial
(with exactly one element) or it has a least non-identity congruence with
respect to the inclusion. For more information on the general universal
algebraic notions, see [11] and for the characterization of subdirectly
irreducible and simple Heyting algebras, see [19].

######  Remark 4.1.

Working with normal explicitly Heyting algebras, the previous definition of
congruence relations may appear somewhat ambiguous, as it is not clear if a
congruence relation must also respect the Heyting implications. To make the
definition more clear, let us emphasize that we do not assume this
preservation condition. However, we will see that it automatically follows
from the original definition. This makes the definition natural, even in its
extended signature.

To provide a characterization for simple and subdirectly irreducible normal
distributive $\nabla$-algebras, as it is well-known in the theory of Heyting
algebras, we establish a connection between the congruence relations and a
family of filters. In our case, the filters we are interested in are what we
call the _modal filters_.

######  Definition 4.2.

Let $\mathcal{A}$ be a normal $\nabla$-algebra. By a _modal filter_ $F$ on
$\mathcal{A}$, we mean an upset of $\mathcal{A}$, closed under all finite
meets and the modal operations $\Box$ and $\nabla$. We denote the class of all
modal filters of $\mathcal{A}$ by $\mathcal{M}(\mathcal{A})$.

######  Example 4.3.

Any normal $\nabla$-algebra has two trivial modal filters $F=\\{1\\}$ and
$F=A$. The latter is clear. For the former, notice that the normality implies
$\nabla 1=1$, while $\Box 1=1$ holds in all $\nabla$-algebras.

The following lemma proves the existence and also provides an explicit
description for the least modal filter containing a given set $S$ of the
elements of a normal $\nabla$-algebra.

######  Lemma 4.4.

Let $\mathcal{A}$ be a normal $\nabla$-algebra. For any subset $S\subseteq A$,
the least modal filter extending the set $S$, denoted by $m(S)$, exists and is
described as:

$m(S)=\\{y\in A\mid\exists I\,\forall i\in I\,\exists
m_{i},n_{i}\in\mathbb{N}\;\exists s_{i}\in S\;(\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}s_{i}\leq y)\\},$

where $I$ ranges over the _finite_ sets. We will denote $m(\\{x\\})$ by
$m(x)$.

###### Proof.

It is clear that any modal filter that extends $S$ includes $m(S)$. Therefore,
it is enough to show that $m(S)$ is a modal filter itself. It is clearly a
filter and since $\nabla$ commutes with all finite meets, it is also closed
under $\nabla$. To show its closure under $\Box$, assume $y\in m(S)$. Hence,
there is a finite set $I$ such that for any $i\in I$, there are
$m_{i},n_{i}\in\mathbb{N}$ and $s_{i}\in S$ such that $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}s_{i}\leq y$. Therefore, $\Box\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}s_{i}\leq\Box y$. Since $\Box$ is a right adjoint,
it commutes with meets and hence $\bigwedge_{i\in
I}\Box\nabla^{m_{i}}\Box^{n_{i}}s_{i}\leq\Box y$. Define $J$ as the set of all
$i$’s in $I$ such that $m_{i}>0$. Then, since for any $x\in A$, we have
$x\leq\Box\nabla x$, we have
$\nabla^{m_{i}-1}\Box^{n_{i}}s_{i}\leq\Box\nabla^{m_{i}}\Box^{n_{i}}s_{i}$,
for any $i\in J$. Hence,

$\left(\bigwedge_{i\in
I-J}\Box^{n_{i}+1}s_{i}\right)\wedge\left(\bigwedge_{i\in
J}\nabla^{m_{i}-1}\Box^{n_{i}}s_{i}\right)\leq\left(\bigwedge_{i\in
I-J}\Box^{n_{i}+1}s_{i}\right)\wedge\left(\bigwedge_{i\in
J}\Box\nabla^{m_{i}}\Box^{n_{i}}s_{i}\right)$

As the right hand side equals to $\bigwedge_{i\in
I}\Box\nabla^{m_{i}}\Box^{n_{i}}s_{i}$ and we observed that it is smaller than
$\Box y$, we have $\Box y\in m(S)$. ∎

In the following, we will show that the modal filters and the congruence
relations in normal distributive $\nabla$-algebras are in one-to-one
correspondence. To establish that connection, we need the following lemma:

######  Lemma 4.5.

In any normal distributive $\nabla$-algebra, the following inequalities are
satisfied:

$(1)$

$x\to y\leq(x\wedge z)\to(y\wedge z)$,

$(2)$

$x\to y\leq(x\vee z)\to(y\vee z)$,

$(3)$

$\nabla(x\to y)\leq\nabla x\to\nabla y$,

$(4)$

$\Box(x\to y)\leq(z\to x)\to(z\to y)$,

$(5)$

$\Box(x\to y)\leq(y\to z)\to(x\to z)$.

If the $\nabla$-algebra is also Heyting with the Heyting implication
$\supset$, we also have:

$(6)$

$x\to y\leq(z\supset x)\to(z\supset y)$,

$(7)$

$x\to y\leq(y\supset z)\to(x\supset z)$.

###### Proof.

For $(1)$, using the adjunction, it is enough to prove $\nabla(x\to y)\wedge
x\wedge z\leq y\wedge z$, which is clear from $\nabla(x\to y)\wedge x\leq y$.
For $(2)$, using the adjunction, we have to show that $\nabla(x\to
y)\wedge(x\vee z)\leq y\vee z$. Using distributivity and the fact that
$\nabla(x\to y)\wedge x\leq y$, the claim easily follows. For $(3)$, by
normality, we have

$\nabla\nabla(x\to y)\wedge\nabla x=\nabla[\nabla(x\to y)\wedge x]\leq\nabla
y.$

Hence, by adjunction, $\nabla(x\to y)\leq\nabla x\to\nabla y$. For $(4)$, by
the adjunction, we have to show

$\nabla\Box(x\to y)\wedge(z\to x)\leq(z\to y).$

By Theorem 3.10, part (iii), we have $\nabla\Box(x\to y)\leq(x\to y)$.
Therefore, using the fact that the operation $\to$ is an implication, Theorem
3.20, the claim easily follows. The proof for $(5)$ is similar to that of
$(4)$. The parts $(6)$ and $(7)$ are some easy consequences of $\nabla(x\to
y)\wedge x\leq y$. ∎

######  Theorem 4.6.

Let $\mathcal{A}$ be a normal distributive $\nabla$-algebra. Then, the
following operations provide a one-to-one correspondence between the poset of
the modal filters of $\mathcal{A}$ and the poset of the congruences on
$\mathcal{A}$, both ordered by the inclusion:

  * $\alpha:\mathcal{M}(\mathcal{A})\to\Theta(\mathcal{A})$, defined by $\alpha(F)=\\{(x,y)\in A^{2}\mid x\leftrightarrow y\in F\\}$,

  * $\beta:\Theta(\mathcal{A})\to\mathcal{M}(\mathcal{A})$, defined by $\beta(\theta)=\\{x\in A\mid(x,1)\in\theta\\}$.

where $x\leftrightarrow y$ is an abbreviation for $(x\to y)\wedge(y\to x)$.

###### Proof.

First, we show that $\alpha(F)$ is a congruence relation and $\beta(\theta)$
is a modal filter, for any modal filter $F$ and any congruence relation
$\theta$. For the former, by Theorem 3.20, $\to$ is an implication. Hence, we
have $x\to x=1$ and $(x\to y)\wedge(y\to z)\leq(x\to z)$, for any $x,y,z\in
A$. Using this fact and the symmetric definition of $\alpha(F)$, it is easy to
prove that $\alpha(F)$ is an equivalence relation. To prove that $\alpha(F)$
respects all the operations in the signature, it is enough to use Lemma 4.5
and the fact that $F$ is a filter closed under $\Box$ and $\nabla$. We only
prove the hardest case of implication, the rest are similar. To show that
$\alpha(F)$ respects the operation $\to$, we prove that
$(x,y),(z,w)\in\alpha(F)$ imply $(x\to z,y\to w)\in\alpha(F)$. By definition,
as $(x,y),(z,w)\in\alpha(F)$, we have $x\leftrightarrow y,z\leftrightarrow
w\in F$. Since $F$ is a filter, $y\rightarrow x,z\rightarrow w\in F$. Since
$F$ is a modal filter, $\Box(y\rightarrow x),\Box(z\rightarrow w)\in F$. By
Lemma 4.5, parts $(4)$ and $(5)$, we have

$\Box(y\rightarrow x)\wedge\Box(z\rightarrow w)\leq[(x\to z)\to(y\to
z)]\wedge[(y\to z)\to(y\to w)].$

Since $\to$ is an implication, we have

$[(x\to z)\to(y\to z)]\wedge[(y\to z)\to(y\to w)]\leq(x\to z)\to(y\to w),$

and as $F$ is a filter, we have $(x\to z)\to(y\to w)\in F$. Similarly, $(y\to
w)\to(x\to z)\in F$. Hence, $(x\to z,y\to w)\in\alpha(F)$.
To prove that $\beta(\theta)$ is a modal filter, the only thing to check is
the upward-closedness of $\beta(\theta)$. The rest is a clear consequence of
the equalities $1\wedge 1=\nabla 1=\Box 1=1$. Now, assume $x\leq y$ and
$x\in\beta(\theta)$. Since $x\leq y$, we have $x\to y=1$. Therefore, since
$\theta$ is a congruence relation and $(x,1)\in\theta$, we have $(1\to y,x\to
y)\in\theta$. Hence, $(1\to y,1)\in\theta$ and then $(\nabla(1\to y),\nabla
1)\in\theta$. By disjunction with $y$ on both sides, we have $(\nabla(1\to
y)\vee y,\nabla 1\vee y)\in\theta$. Since $\nabla(1\to y)\leq y$ and $\nabla
1=1$, we have $(y,1)\in\theta$. Therefore, $y\in\beta(\theta)$.
Notice that both $\alpha$ and $\beta$ are trivially monotone with respect to
the inclusion. To prove $\alpha(\beta(\theta))=\theta$ and
$\beta(\alpha(F))=F$, we have to show that

$x\in F\;\;\;\text{iff}\;\;\;1\leftrightarrow x\in
F\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;(x,y)\in\theta\;\;\;\text{iff}\;\;\;(x\leftrightarrow
y,1)\in\theta.$

For the left equivalence, if $x\in F$, since $x\to 1=1$, we have $x\to 1\in F$
and since $F$ is a modal filter, we have $\Box x=1\to x\in F$. Therefore,
$1\leftrightarrow x\in F$. For the converse, if $1\leftrightarrow x\in F$,
then $1\to x\in F$ and as $F$ is upward-closed and also closed under $\nabla$,
using the fact that $\nabla(1\to x)\leq x$, we have $x\in F$.
For the right equivalence, if $(x,y)\in\theta$, since $\theta$ is a congruence
relation, we have $(x\leftrightarrow y,x\leftrightarrow x)\in\theta$ which
implies $(x\leftrightarrow y,1)\in\theta$, by the fact that $\to$ is an
implication and hence $x\to x=1$. For the converse, if $(x\leftrightarrow
y,1)\in\theta$, then since $\beta(\theta)$ is a filter, we have $(x\to
y,1)\in\theta$ and hence $(y\vee[x\wedge\nabla(x\to y)],y\vee[x\wedge\nabla
1])\in\theta$. Therefore, as $x\wedge\nabla(x\to y)\leq y$ and $\nabla 1=1$,
we have $(y,y\vee x)\in\theta$. By symmetry, we also have $(x,x\vee
y)\in\theta$ and hence $(x,y)\in\theta$. ∎

######  Remark 4.7.

Theorem 4.6 shows that if $\mathcal{A}$ is also a Heyting algebra and $\theta$
is a congruence relation, then $\theta$ also respects the Heyting implication.
To prove this, assume $(x,y),(z,w)\in\theta$. Set $F=\beta(\theta)$. By
Theorem 4.6, we have $\theta=\alpha(F)$. Hence, $x\leftrightarrow
y,z\leftrightarrow w\in F$. Then, by the parts $(6)$ and $(7)$ in Lemma 4.5,
we have

$(y\rightarrow x)\wedge(z\rightarrow w)\leq[(x\supset z)\to(y\supset
z)]\wedge[(y\supset z)\to(y\supset w)].$

Since $\to$ is an implication, we have

$[(x\supset z)\to(y\supset z)]\wedge[(y\supset z)\to(y\supset w)]\leq(x\supset
z)\to(y\supset w).$

Hence, we have $(x\supset z)\to(y\supset w)\in F$. Similarly, $(y\supset
w)\to(x\supset z)\in F$. Hence, $(x\supset z)\leftrightarrow(y\supset w)\in F$
which implies $(x\supset z,y\supset w)\in\theta$. This remark ensures that all
the following theorems on congruence extension property, subdirectly
irreducible and simple normal distributive $\nabla$-algebras also hold for the
normal explicitly Heyting $\nabla$-algebras, where the Heyting implication is
explicitly mentioned in the signature of the algebras.

######  Remark 4.8.

By Theorem 4.6, the trivial modal filters $F=\\{1\\}$ and $F=A$ correspond to
the trivial congruence relations $\theta=\\{(x,x)\in A^{2}\mid x\in A\\}$ and
$\theta=A\times A$, respectively.

######  Definition 4.9.

A class $\mathfrak{C}$ of $\nabla$-algebras has the _congruence extension
property_ if for any $\mathcal{B}$ in $\mathfrak{C}$, any sub-algebra
$\mathcal{A}$ of $\mathcal{B}$ and any congruence relation $\theta$ over
$\mathcal{A}$, there exists a congruence relation $\phi$ over $\mathcal{B}$
such that $\phi|_{A}=\theta$.

######  Corollary 4.10.

The variety $\mathcal{V}(D,N)$ and all of its subclasses have the congruence
extension property. The same also holds for $\mathcal{V}_{H}(N)$.

###### Proof.

For the first part, let $\mathcal{A}$ and $\mathcal{B}$ be two normal
distributive $\nabla$-algebras, $\mathcal{A}$ be a sub-algebra of
$\mathcal{B}$ and $\theta$ be a congruence relation over $\mathcal{A}$. Define
$\phi$ on $\mathcal{B}$ by $\\{(x,y)\in B^{2}\mid x\leftrightarrow y\in
m_{\mathcal{B}}(\beta(\theta))\\}$, where $\beta(\theta)$ is the corresponding
modal filter to $\theta$ over $\mathcal{A}$ and
$m_{\mathcal{B}}(\beta(\theta))$ is the least modal filter in $\mathcal{B}$
that includes $\beta(\theta)$. By Theorem 4.6, $\phi$ is a congruence relation
over $\mathcal{B}$. Hence, the only thing remained to prove is that
$\phi|_{A}=\theta$. Let $a,b\in A$. Then, we have to show that $(a,b)\in\phi$
iff $(a,b)\in\theta$. Using Theorem 4.6 for $\mathcal{A}$, the latter is
equivalent to $a\leftrightarrow b\in\beta(\theta)$. Now, it is enough to show
that $a\leftrightarrow b\in m_{\mathcal{B}}(\beta(\theta))$ iff
$a\leftrightarrow b\in\beta(\theta)$. The latter is actually true in a more
general form: $c\in m_{\mathcal{B}}(F)$ iff $c\in F$, for any $c\in A$ and any
modal filter $F$ over $\mathcal{A}$. One direction is clear. For the other
direction, note that if $c\in m_{\mathcal{B}}(F)$, then by Lemma 4.4, there
exists a finite set $I$ such that for any $i\in I$, there are
$m_{i},n_{i}\in\mathbb{N}$ and $a_{i}\in F$ such that $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}a_{i}\leq_{\mathcal{B}}c$. Since, $\mathcal{A}$ is
a sub-algebra of $\mathcal{B}$, we have $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}a_{i}\leq_{\mathcal{A}}c$ which finally implies
$c\in F$. This completes the proof of the first part. For the second part, use
the first part and Remark 4.7. ∎

######  Corollary 4.11.

A non-trivial normal distributive $\nabla$-algebra $\mathcal{A}$ is
subdirectly irreducible iff there exists $x\in A-\\{1\\}$ such that for any
$y\in A-\\{1\\}$, there exists a finite set $I$ such that for any $i\in I$,
there are $m_{i},n_{i}\in\mathbb{N}$ satisfying $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}y\leq x$. The same also holds for any
$\mathcal{A}\in\mathcal{V}_{H}(N)$.

###### Proof.

For the first part, by Theorem 4.6 and Remark 4.8, it is enough to prove the
equivalence between the existence of the minimum modal filter satisfying
$F\neq\\{1\\}$ and the existence of an element $x\in A-\\{1\\}$ as presented.
First, assume that such an $x$ exists. Since $x\neq 1$ and $x\in m(x)$, then
$m(x)\neq\\{1\\}$. Therefore, it is enough to show that $m(x)\subseteq F$, for
any $F\neq\\{1\\}$. Since, $F\neq\\{1\\}$, there is $y\in F$ such that $y\neq
1$. By the condition, there exists a finite set $I$ such that for any $i\in
I$, there are $m_{i},n_{i}\in\mathbb{N}$ satisfying $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}y\leq x$. Since, $F$ is a modal filter and $y\in
F$, we have $x\in F$. Therefore, as $m(x)$ is the least modal filter
containing $x$, we reach $m(x)\subseteq F$. Conversely, assume that the family
of the modal filters different from $\\{1\\}$ has the minimum element. Denote
this element by $F$. Then, since $F\neq\\{1\\}$, there exists $x\in F$ such
that $x\neq 1$. Let $y$ be any arbitrary element in $A-\\{1\\}$. Then, as
$y\in m(y)$, we have $m(y)\neq\\{1\\}$ which by the minimality of $F$ implies
$F\subseteq m(y)$. Since $x\in F$, we have $x\in m(y)$. Therefore, by Lemma
4.4, there exists a finite set $I$ such that for any $i\in I$, there are
$m_{i},n_{i}\in\mathbb{N}$ satisfying $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}y\leq x$. This completes the proof of the first
part. For the second part, use the first part and Remark 4.7. ∎

######  Corollary 4.12.

$(i)$

A non-trivial normal distributive left $\nabla$-algebra $\mathcal{A}$ is
subdirectly irreducible iff there exists $x\in A-\\{1\\}$ such that for any
$y\in A-\\{1\\}$, there exists $k\in\mathbb{N}$ satisfying $\nabla^{k}y\leq
x$. The same also holds for any $\mathcal{A}\in\mathcal{V}_{H}(N,L)$.

$(ii)$

A non-trivial normal distributive right $\nabla$-algebra $\mathcal{A}$ is
subdirectly irreducible iff there exists $x\in A-\\{1\\}$ such that for any
$y\in A-\\{1\\}$, there exists $k\in\mathbb{N}$ satisfying $\Box^{k}y\leq x$.
The same also holds for any $\mathcal{A}\in\mathcal{V}_{H}(N,R)$.

###### Proof.

For $(i)$, by Theorem 3.12, we have $z\leq\Box z$ and
$\nabla^{l+1}z\leq\nabla^{l}z$, for any $z\in A$. Therefore, for any finite
set $I$, any $m_{i},n_{i}\in\mathbb{N}$ and any $y\in A$, we have
$\nabla^{k}y\leq\bigwedge_{i\in I}\nabla^{m_{i}}\Box^{n_{i}}y$, where $k$ is
the maximum of all $m_{i}$’s. Using this observation, it is easy to see that
the condition in Corollary 4.11 is equivalent to the existence of $x\neq 1$
such that for any $y\neq 1$, there exists a number $k\in\mathbb{N}$ satisfying
$\nabla^{k}y\leq x$. For $(ii)$, use a similar argument, considering the fact
that in any right $\nabla$-algebra, $z\leq\nabla z$ and
$\Box^{l+1}z\leq\Box^{l}z$, for any $z\in A$, as proved in Theorem 3.11. ∎

######  Corollary 4.13.

A non-trivial Heyting algebra $\mathcal{A}$ is subdirectly irreducible iff
there exists $x\in A-\\{1\\}$ such that $y\leq x$, for any $y\in A-\\{1\\}$.

###### Proof.

A Heyting algebra is a normal distributive $\nabla$-algebra with
$\nabla=\Box=id$. Now, apply Corollary 4.11. ∎

######  Corollary 4.14.

A normal distributive $\nabla$-algebra $\mathcal{A}$ is simple iff for any
$x\in A-\\{1\\}$, there exists a finite set $I$ such that for any $i\in I$,
there are $m_{i},n_{i}\in\mathbb{N}$ satisfying $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}x=0$. The same also holds for any
$\mathcal{A}\in\mathcal{V}_{H}(N)$.

###### Proof.

For the first part, by Theorem 4.6 and Remark 4.8, it is enough to show that
the condition in the statement of the corollary is equivalent to the non-
existence of non-trivial modal filters. First, assume the condition and
suppose that $F\neq\\{1\\}$ is an arbitrary modal filter. We have to show that
$F=A$. Since $F\neq\\{1\\}$, there is $x\in F$ such that $x\neq 1$. By the
condition, there exists a finite set $I$ such that for any $i\in I$, there are
$m_{i},n_{i}\in\mathbb{N}$ satisfying $\bigwedge_{i\in
I}\nabla^{m_{i}}\Box^{n_{i}}x=0$. Since $x\in F$, we have $0\in F$ and hence
$F=A$. Conversely, assume that $\mathcal{A}$ has no non-trivial modal filter.
Let $x\neq 1$. As $x\in m(x)$, we have $m(x)\neq\\{1\\}$. Therefore, $m(x)=A$,
which implies $0\in m(x)$. By Lemma 4.4, there exists a finite set $I$ such
that for any $i\in I$, there are $m_{i},n_{i}\in\mathbb{N}$ satisfying
$\bigwedge_{i\in I}\nabla^{m_{i}}\Box^{n_{i}}x=0$. This completes the proof of
the first part. For the second part, use the first part and Remark 4.7. ∎

######  Corollary 4.15.

$(i)$

A normal distributive left $\nabla$-algebra $\mathcal{A}$ is simple iff for
any $x\in A-\\{1\\}$, there exists $k\in\mathbb{N}$ satisfying
$\nabla^{k}x=0$. The same also holds for any
$\mathcal{A}\in\mathcal{V}_{H}(N,L)$.

$(ii)$

A normal distributive right $\nabla$-algebra $\mathcal{A}$ is simple iff for
any $x\in A-\\{1\\}$, there exists $k\in\mathbb{N}$ satisfying $\Box^{k}x=0$.
The same also holds for any $\mathcal{A}\in\mathcal{V}_{H}(N,R)$.

###### Proof.

For $(i)$, again use the facts $z\leq\Box z$ and
$\nabla^{l+1}z\leq\nabla^{l}z$, for any $z\in A$, proved in Theorem 3.12. For
$(ii)$, use $z\leq\nabla z$ and $\Box^{l+1}z\leq\Box^{l}z$, for any $z\in A$,
proved in Theorem 3.11. ∎

The following characterization of simple Heyting algebras is a well-known fact
and it can be obtained as a particular case of Corollary 4.15.

######  Corollary 4.16.

A Heyting algebra $\mathcal{A}$ is simple iff for any $x\in A$ either $x=1$ or
$x=0$.

The following theorem provides an infinite family of finite simple normal
Heyting $\nabla$-algebras to witness the relative complexity of the varieties
of $\nabla$-algebras compared to the variety of Heyting algebras, where there
is only one non-trivial simple element.

######  Theorem 4.17.

There are infinitely many finite simple normal Heyting $\nabla$-algebras.

###### Proof.

Let $n\geq 1$ be a natural number. Define the topological space
$X_{n}=\\{1,2,\cdots,n\\}\cup\\{\omega\\}$ with the following topology: A
subset $U\subseteq X_{n}$ is open if either $U=X_{n}$ or
$U\subseteq\\{1,2,\cdots,n\\}$. Define $f_{n}:X_{n}\to X_{n}$ as the function
mapping $x\neq n,\omega$ to $x+1$ and $f_{n}(n)=f_{n}(\omega)=\omega$. This
function is clearly continuous as $\omega\notin f_{n}^{-1}(U)$, for any
$U\subseteq\\{0,1,\cdots,n\\}$. Now, consider the normal Heyting
$\nabla$-algebra $\mathcal{A}_{n}$ associated to the dynamic topological
system $(X_{n},f_{n})$ as explained in Example 3.6 and recall that in that
$\nabla$-algebra $\nabla U=f^{-1}(U)$, for any open $U\subseteq X_{n}$. We
claim that $\mathcal{A}_{n}$ is simple. For that purpose, we show
$\nabla^{n}U=\varnothing$, for any $U\neq X_{n}$. Assume $U\neq X_{n}$. Hence,
$\omega\notin U$. It is easy to see that
$\nabla^{m}U=\\{x\in\\{1,2,\cdots,n\\}\mid x+m\in U\\}$, for any $m\leq n$.
Therefore, for $m=n$, we have $\nabla^{n}U=\varnothing$. Hence, by Corollary
4.14, the normal distributive $\nabla$-algebra $\mathcal{A}_{n}$ is simple.
Finally, note that the $\mathcal{A}_{n}$’s are different as their base
lattices have different cardinalities. ∎

##  5 Dedekind-MacNeille Completion

The Dedekind-MacNeille completion of a poset is its smallest complete
extension. In this section, we will show that starting from a $\nabla$-algebra
rather than a poset, there is a unique way to make its Dedekind-MacNeille
completion a $\nabla$-algebra. In this sense, one can say that the variety of
$\nabla$-algebras is closed under the Dedekind-MacNeille completion. This
closure will be useful later in the sequel of the present paper to prove a
completeness theorem showing that certain logics are complete for certain
families of _complete_ $\nabla$-algebras. The completion is also the main tool
to prove the completeness of the algebraic semantics for the predicate version
of the mentioned logics. Note that the closure under the Dedekind-MacNeille
completion is a rare property for a variety to have. For instance, the variety
of bounded distributive lattices lacks the property and between all the
varieties of Heyting algebras only the three varieties of all Heyting
algebras, all boolean algebras and the trivial variety has the property [25].
In this sense, the closure of many varieties of $\nabla$-algebras under the
Dedekind-MacNeille completion can be seen as a mathematical evidence to show
how well-behaved the notion of a $\nabla$-algebra is.

######  Definition 5.1.

Let $(P,\leq)$ be a poset and $S\subseteq P$. By $U(S)=\\{x\in P\mid\forall
y\in S,\;y\leq x\\}$ and $L(S)=\\{x\in P\mid\forall y\in S,\;x\leq y\\}$, we
mean the set of all upper bounds and all lower bounds of $S$, respectively. A
subset $N\subseteq P$ is called _normal_ iff $LU(N)=N$. Any set in the form
$(x]=\\{y\in P\mid y\leq x\\}$ is clearly normal. The Dedekind-MacNeille
completion of $(P,\leq)$, denoted by $\mathcal{N}(P,\leq)$, is the poset of
all normal subsets of $P$ ordered by inclusion. By the canonical map of the
completion, we mean $i:(P,\leq)\to\mathcal{N}(P,\leq)$ defined by $i(x)=(x]$.

It is well-known that the poset of all normal subsets is actually a complete
lattice with intersection as the meet and $\bigvee_{i\in
I}N_{i}=LU(\bigcup_{i\in I}N_{i})$ as the join. Moreover, the canonical map
$i$ is an order embedding that preserves all the existing meets and joins in
$(P,\leq)$ and if the poset $(P,\leq)$ is also a Heyting algebra, it also
preserves the Heyting implication, see Subsection A.6 in [19]. It is also easy
to see that if $\mathcal{A}$ is a bounded lattice itself, any normal subset is
actually an ideal. Therefore, as we work exclusively with $\nabla$-algebras
which are also bounded lattices, we use the term normal ideals for the normal
subsets. The following well-known lemma is a nice characterization of these
normal ideals. We will provide its simple proof for the sake of completeness.

######  Lemma 5.2.

A subset $N$ is normal iff $N$ is representable as an intersection of
principal ideals, i.e., the ideals in the form $(x]$, for some $x\in A$.

###### Proof.

If $N$ is normal, as $LU(N)=N$ and $LU(N)=\bigcap_{n\in U(N)}(n]$, the claim
is clear. Conversely, assume $N=\bigcap_{i\in I}(n_{i}]$. We show
$LU(N)\subseteq N$. The converse, i.e., $N\subseteq LU(N)$, always holds.
Since $N=\bigcap_{i\in I}(n_{i}]$, we have $n_{i}\in U(N)$, because if $x\in
N$ then $x\leq n_{i}$. Now, assume $y\in LU(N)$. Since, $n_{i}\in U(N)$, we
have $y\leq n_{i}$, for all $i\in I$. This implies $y\in\bigcap_{i\in
I}(n_{i}]=N$. ∎

Now, for any $\nabla$-algebra $\mathcal{A}$, define the operations $\nabla$
and $\to$ on its lattice of normal ideals, $\mathcal{N}(\mathsf{A})$, by
$\nabla N=\bigvee_{n\in N}(\nabla n]$ and $M\to N=\\{x\in A\mid\forall m\in
M,\nabla x\wedge m\in N\\}$. In the rest of this section, we show that this
pair of operations is the unique pair that makes the lattice
$\mathcal{N}(\mathsf{A})$ into a $\nabla$-algebra and the lattice embedding
$i$ into a $\nabla$-algebra morphism. The uniqueness is easy to prove. Let
$\nabla^{\prime}$ and $\to^{\prime}$ be another such pair. It is enough to
prove $\nabla=\nabla^{\prime}$. As $\nabla^{\prime}$ has a right adjoint, it
must preserve all joins in $\mathcal{N}(\mathsf{A})$. Moreover, as $i$ is a
$\nabla$-algebra morphism, we have $\nabla^{\prime}(n]=(\nabla n]$. Therefore,

$\nabla^{\prime}N=\nabla^{\prime}\bigvee_{n\in N}(n]=\bigvee_{n\in
N}\nabla^{\prime}(n]=\bigvee_{n\in N}(\nabla n]=\nabla N.$

This completes the proof of the uniqueness. For the rest, denote the tuple
$(\mathcal{N}(\mathsf{A}),\nabla,\to)$ by $\mathcal{N}(\mathcal{A})$. Then:

######  Theorem 5.3.

Let $C\subseteq\\{H,N,R,L,Fa,Fu\\}$. Then,
$\mathcal{N}(\mathcal{A})\in\mathcal{V}(C)$ and the canonical embedding
$i:\mathcal{A}\to\mathcal{N}(\mathcal{A})$ is also a $\nabla$-algebra
embedding, for any $\mathcal{A}\in\mathcal{V}(C)$. If $H\in C$, the embedding
is also a Heyting $\nabla$-algebra morphism. In this sense, $\mathcal{V}(C)$
is closed under the Dedekind-MacNeille completion.

###### Proof.

To show that the operations $\nabla$ and $\to$ are well-defined, the only
thing to prove is the normality of $M\to N$, when $M$ and $N$ are both normal
ideals. Since $N$ is normal, by Lemma 5.2, $N=\bigcap_{i\in I}(n_{i}]$, for
some $I$ and $n_{i}$’s. Therefore, using the definition, we know that $x\in
M\to N$ iff for any $m\in M$ and $i\in I$, we have $\nabla x\wedge m\leq
n_{i}$. Hence, $M\to N=\bigcap_{i\in I,m\in M}(m\to n_{i}]$ and by Lemma 5.2,
$M\to N$ is normal.

Now, we show that $i:\mathcal{A}\to\mathcal{N}(\mathcal{A})$ preserves
$\nabla$ and $\to$. For $\nabla$, by definition, $\nabla(a]=\bigvee_{b\leq
a}(\nabla b]$. Clearly, $(\nabla a]$ is one of the ideals we use join over.
Hence, $(\nabla a]\subseteq\bigvee_{b\leq a}(\nabla b]$. On the other hand,
$\nabla b\leq\nabla a$, for any $b\leq a$. Hence, $(\nabla b]\subseteq(\nabla
a]$ which implies $\bigvee_{b\leq a}(\nabla b]\subseteq(\nabla a]$. Therefore,
$\nabla(a]=\bigvee_{b\leq a}(\nabla b]=(\nabla a]$. For the implication, we
have the following series of equivalences

$x\in(a]\to(b]\;\;\;\text{iff}\;\;\;\forall y\in(a],\nabla x\wedge
y\in(b]\;\;\;\text{iff}$ $\nabla x\wedge a\leq b\;\;\;\text{iff}\;\;\;x\leq
a\to b\;\;\;\text{iff}\;\;\;x\in(a\to b].$

Therefore, $(a]\to(b]=(a\to b]$. We now prove the adjunction condition of a
$\nabla$-algebra, i.e.,

$\nabla M\cap N\subseteq K\;\;\;\text{iff}\;\;\;M\subseteq N\to K,$

for any normal ideals $M$, $N$ and $K$. For the left to right direction,
assume $\nabla M\cap N\subseteq K$ and $m\in M$. We have to show that $m\in
N\to K$ which means that for any arbitrary $n\in N$, we must have $\nabla
m\wedge n\in K$. For that purpose, note that $\nabla m\wedge n\in(\nabla
m]=\nabla(m]\subseteq\nabla M$ and $\nabla m\wedge n\in N$, and since $\nabla
M\cap N\subseteq K$, we have $\nabla m\wedge n\in K$.
For the right to left direction, assume that $M\subseteq N\to K$ and
$x\in\nabla M\cap N$. Then, we have to show that $x\in K$. Since $K$ is
normal, by Lemma 5.2, it is representable as $\bigcap_{i\in I}(k_{i}]$.
Therefore, it is enough to show that $x\leq k_{i}$, for any $i\in I$. First,
since $M\subseteq N\to K$, for any $m\in M$ and $n\in N$, we have $\nabla
m\wedge n\in K$ which implies $\nabla m\wedge n\leq k_{i}$, for any $i\in I$.
Now, as $x\in N$, for any $m\in M$, we have $\nabla m\wedge x\leq k_{i}$.
Hence, $m\leq x\to k_{i}$ which implies $\nabla m\leq\nabla(x\to k_{i})$.
Therefore, $\nabla(x\to k_{i})$ is an upper bound for $\bigcup_{m\in M}(\nabla
m]$. Hence, $\nabla(x\to k_{i})\in U(\bigcup_{m\in M}(\nabla m])$. On the
other hand, by definition, $x\in\nabla M=\bigvee_{m\in M}(\nabla
m]=LU(\bigcup_{m\in M}(\nabla m])$ which implies $x\leq\nabla(x\to k_{i})$.
Therefore, $x\leq x\wedge\nabla(x\to k_{i})\leq k_{i}$ which is what we
wanted.

Finally, we have to check that the conditions $\\{H,N,R,L,Fa,Fu\\}$ are
preserved under the Dedekind-MacNeille completion. The Heyting case and the
fact that the embedding $i$ preserves the Heyting implication is well-known
[19]. For $(N)$, we first prove $\nabla A=A$. For that purpose, as $\nabla
1=1$, we have $A\subseteq(\nabla 1]$. Now, since $\nabla A=\bigvee_{a\in
A}(\nabla a]$, we have $A\subseteq\nabla A$. To prove that $\nabla$ commutes
with the binary meet, it is enough to show that $\nabla M\cap\nabla
N\subseteq\nabla(M\cap N)$, for any two normal ideals $M$ and $N$. The other
direction always holds in a $\nabla$-algebra. Assume $x\in\nabla M\cap\nabla
N$. Since $\nabla M=\bigvee_{m\in M}(\nabla m]=LU(\bigcup_{m\in M}(\nabla
m])$, we know that “ _for any $y$, if $y\geq\nabla m$, for all $m\in M$, we
have $x\leq y$_”. Call the property inside the quotation mark the $(*)$
property for $M$. The $(*)$ property is also true for $N$, because we also
have $x\in\nabla N$. To prove $x\in\nabla(M\cap N)=LU(\bigcup_{k\in M\cap
N}(\nabla k])$, we assume $z\in U(\bigcup_{k\in M\cap N}(\nabla k])$ and we
show that $x\leq z$. Since $z\in U(\bigcup_{k\in M\cap N}(\nabla k])$, for any
arbitrary $m\in M$ and $n\in N$, we have $z\geq\nabla(m\wedge n)$. Since
$\mathcal{A}$ is normal, we have $z\geq\nabla m\wedge\nabla n$. Hence,
$m\leq\nabla n\to z$ which implies $\nabla m\leq\nabla(\nabla n\to z)$.
Therefore, by the $(*)$ property for $M$, we have $x\leq\nabla(\nabla n\to
z)$. Thus, $\nabla n\wedge x\leq\nabla n\wedge\nabla(\nabla n\to z)\leq z$.
Since, $\nabla n\wedge x\leq z$, we have $n\leq x\to z$ and hence $\nabla
n\leq\nabla(x\to z)$. Therefore, by the $(*)$ property for $N$, we have
$x\leq\nabla(x\to z)$ which implies $x\leq x\wedge\nabla(x\to z)\leq z$.
The cases for $(L)$ and $(R)$ are easy, using the explicit definition of
$\Box$ as $\Box N=\\{x\in A\mid\nabla x\in N\\}$ and Theorem 3.12 and Theorem
3.11 that rephrase the leftness and rightness of a $\nabla$-algebra in terms
of its $\Box$. For $(Fa)$, by Theorem 3.13, it is enough to show $\nabla\Box
N=N$. We only prove $N\subseteq\nabla\Box N$. The other direction is a
consequence of the adjunction $\nabla\dashv\Box$. If $n\in N$, then by $(Fa)$
for $\mathcal{A}$, we have $n\leq\nabla\Box n$. Hence, $n\in(\nabla\Box
n]=\nabla\Box(n]\subseteq\nabla\Box N$. For $(Fu)$, by Theorem 3.16, it is
enough to show $\Box\nabla N=N$. We only prove $\Box\nabla N\subseteq N$. The
other direction is again a consequence of the adjunction $\nabla\dashv\Box$.
Assume that $x\in\Box\nabla N$. By definition, we have $\nabla x\in\nabla N$.
To prove that $x\in LU(N)=N$, it is enough to pick an arbitrary $y\in U(N)$
and show that $x\leq y$. Since $y\in U(N)$, for any $n\in N$, we have $y\geq
n$ which implies $\nabla y\geq\nabla n$ and hence $\nabla y\in U(\bigcup_{n\in
N}(\nabla n])$. Since $\nabla x\in\nabla N=LU(\bigcup_{n\in N}(\nabla n])$, we
have $\nabla x\leq\nabla y$. Since $\mathcal{A}$ satisfies $(Fu)$, by Theorem
3.16, the operation $\nabla$ is an order embedding and hence $x\leq y$.
Therefore, $x\in LU(N)=N$. ∎

##  6 Kripke Frames

In this section, we will first recall a variant of intuitionistic Kripke
frames, employed in [38, 22, 34] to capture different intuitionistic modal
logics. This variant provides a natural family of $\nabla$-algebras, as
explained in [1] and Example 3.8. Using the usual prime filter construction,
also employed in [1], it is not hard to represent different classes of
distributive $\nabla$-algebras by their corresponding classes of Kripke
frames. Here, we recall the prime filter construction to expand the
characterization of [1] to also cover the case of full and faithful
distributive $\nabla$-algebras and prove the amalgamation property for some
varieties of distributive normal $\nabla$-algebras. The machinery is also
required for the Kripke and topological completeness theorems and the duality
theory for some families of distributive $\nabla$-algebras planned to be
covered in the sequel of the present paper.

######  Definition 6.1.

Let $(W,\leq)$ be a poset. The tuple $(W,\leq,R)$ is called a _Kripke frame_
if $R$ is compatible with $\leq$, i.e., if $k^{\prime}\leq k$, $(k,l)\in R$
and $l\leq l^{\prime}$, then $(k^{\prime},l^{\prime})\in R$:

${k}$${l}$${{k^{\prime}}}$${{l^{\prime}}}$$\scriptstyle{\leq}$$\scriptstyle{R}$$\scriptstyle{\leq}$$\scriptstyle{R}$

for any $k,l,k^{\prime},l^{\prime}\in W$. Moreover,

$(N)$

if there exists an order-preserving function $\pi:W\to W$, called the
_normality witness_ , such that $(x,y)\in R$ iff $x\leq\pi(y)$, then the
Kripke frame is called _normal_ ,

$(R)$

if $R$ is reflexive or equivalently $\leq\,\subseteq R$, then the Kripke frame
is called _right_ ,

$(L)$

if $R\;\subseteq\;\leq$, then the Kripke frame is called _left_ ,

$(Fa)$

if for any $x\in W$, there exists $y\in W$ such that $(y,x)\in R$ and for any
$z\in W$ such that $(y,z)\in R$ we have $x\leq z$, then the Kripke frame is
called _faithful_ ,

${z}$${x}$${y}$$\scriptstyle{R}$$\scriptstyle{R}$$\scriptstyle{\leq}$

$(Fu)$

if for any $x\in W$, there exists $y\in W$ such that $(x,y)\in R$ and for any
$z\in W$ such that $(z,y)\in R$ we have $z\leq x$, then the Kripke frame is
called _full_.

${y}$${x}$${z}$$\scriptstyle{R}$$\scriptstyle{R}$$\scriptstyle{\leq}$

For any $C\subseteq\\{N,R,L,Fa,Fu\\}$, by $\mathbf{K}(C)$, we mean the class
of all Kripke frames with the properties described in the set $C$. For
instance, $\mathbf{K}(\\{N,Fa\\})$ is the class of all normal faithful Kripke
frames.
If $\mathcal{K}=(W,\leq,R)$ and
$\mathcal{K}^{\prime}=(W^{\prime},\leq^{\prime},R^{\prime})$ are two Kripke
frames, then by a Kripke morphism $f:\mathcal{K}\to\mathcal{K}^{\prime}$, we
mean an order-preserving function from $W$ to $W^{\prime}$ such that:

  * $\bullet$

For any $k,l\in W$, if $(k,l)\in R$ then $(f(k),f(l))\in R^{\prime}$,

  * $\bullet$

for any $k\in W$ and any $l^{\prime}\in W^{\prime}$ such that
$(f(k),l^{\prime})\in R^{\prime}$, there exists $l\in W$ such that $(k,l)\in
R$ and $f(l)=l^{\prime}$,

  * $\bullet$

for any $k\in W$ and any $l^{\prime}\in W^{\prime}$ such that
$(l^{\prime},f(k))\in R^{\prime}$, there exists $l\in W$ such that $(l,k)\in
R$ and $f(l)\geq^{\prime}l^{\prime}$.

If we also have the following condition:

  * $\bullet$

for any $k\in W$ and any $l^{\prime}\in W^{\prime}$ such that
$f(k)\leq^{\prime}l^{\prime}$, there exists $l\in W$ such that $k\leq l$ and
$f(l)=l^{\prime}$,

then the Kripke morphism $f$ is called a _Heyting Kripke morphism_. Kripke
frames and Kripke morphisms form a category that we loosely denote by its
class of objects $\mathbf{K}(C)$. If we use the Heyting Kripke morphisms,
instead, then we denote the subcategory by $\mathbf{K}^{H}(C)$.

If the Kripke frame is normal, we can rewrite the conditions $\\{R,L,Fa,Fu\\}$
purely in terms of the normality witness of the frame. We will need these
characterizations to prove the amalgamation property for some varieties of
normal $\nabla$-algebras in Subsection 6.1. They are also required in the
duality theory planned to be covered in the sequel of the present paper.

######  Lemma 6.2.

Let $\mathcal{K}=(W,\leq,R)$ be a normal Kripke frame with the normality
witness $\pi$. Then:

$(i)$

$(R)$ is equivalent to the condition that $w\leq\pi(w)$, for any $w\in W$,

$(ii)$

$(L)$ is equivalent to the condition that $\pi(w)\leq w$, for any $w\in W$,

$(iii)$

$(Fa)$ is equivalent to the condition that $\pi$ is an order embedding, i.e.,
if $\pi(u)\leq\pi(v)$ then $u\leq v$, for any $u,v\in W$,

$(iv)$

$(Fu)$ is equivalent to the surjectivity of $\pi$.

###### Proof.

First, recall that by normality, $(x,y)\in R$ iff $x\leq\pi(y)$. We use this
equivalence to rewrite all the aforementioned conditions in terms of $\pi$.
For $(i)$, by normality, it is clear that $(w,w)\in R$ iff $w\leq\pi(w)$.
Hence, there is nothing to prove. For $(ii)$, by normality, the condition
$(L)$, i.e., $R\subseteq\;\leq$ simply states that for all $u,v\in W$ if
$v\leq\pi(u)$ then $v\leq u$. This is trivially equivalent to $\pi(u)\leq u$,
for all $u\in W$. For $(iii)$, assume $(Fa)$. To prove that $\pi$ is an order
embedding, suppose that $\pi(u)\leq\pi(v)$. By $(Fa)$, there exists $y\in W$
such that $(y,u)\in R$ and for any $z\in W$ if $(y,z)\in R$ then $u\leq z$. By
normality, $y\leq\pi(u)$. Put $z=v$. Since $\pi(u)\leq\pi(v)$, we have
$y\leq\pi(v)$. Again, by normality, $(y,v)\in R$. Hence, $u\leq v$, by $(Fa)$.
For the converse, suppose that $\pi$ is an order embedding. To prove $(Fa)$,
we have to show that for any $x\in W$, there exists $y\in W$ such that
$(y,x)\in R$ and for any $z\in W$, if $(y,z)\in R$ then $x\leq z$. Set
$y=\pi(x)$. Since $y\leq\pi(x)$, by normality, $(y,x)\in R$ and if $(y,z)\in
R$, meaning $y\leq\pi(z)$, we have $\pi(x)\leq\pi(z)$ which implies $x\leq z$,
by the assumption that $\pi$ is an order embedding. For $(iv)$, assume that
$(Fu)$ holds. We show that $\pi$ is surjective. By $(Fu)$, for any $x\in W$,
there exists $y\in W$ such that $(x,y)\in R$ and for any $z\in W$ such that
$(z,y)\in R$, we have $z\leq x$. We claim that $\pi(y)=x$. Since $(x,y)\in R$,
we have $x\leq\pi(y)$. To show $\pi(y)\leq x$, put $z=\pi(y)$. Then, by
normality, $(z,y)\in R$ and hence by $(Fu)$, we have $\pi(y)=z\leq x$.
Therefore, $\pi(y)=x$. Conversely, assume that $\pi$ is surjective. We show
that $(Fu)$ holds. By surjectivity, for any $x\in W$, there exists $y\in W$
such that $\pi(y)=x$. We claim this $y$ works for the condition $(Fu)$. First,
by normality, it is clear that $(x,y)\in R$. Now, if $z\in W$ such that
$(z,y)\in R$ then, by normality $z\leq\pi(y)=x$. Hence, $z\leq x$. ∎

Using Theorem 6.2, one can interpret the normal Kripke frame $(W,\leq,R)$ with
the normality witness $\pi:W\to W$ as the _dynamic poset_ $(W,\leq,\pi)$
consisting of the state space $(W,\leq)$ and the dynamism $\pi$. Then, the
faithfulness and fullness conditions that we abstracted from dynamic
topological systems in Example 3.6 play a similar role here. The former means
that the dynamism $\pi$ is an order embedding while the latter is its
surjectivity.

Similar to the previous lemma, when the Kripke frames are normal, we can
rewrite the conditions of being a Kripke morphism purely in terms of the
normality witnesses of the frames.

######  Lemma 6.3.

Let $\mathcal{K}=(W,\leq,R)$ and
$\mathcal{K}^{\prime}=(W^{\prime},\leq^{\prime},R^{\prime})$ be two normal
Kripke frames with the normality witnesses $\pi$ and $\pi^{\prime}$,
respectively. Then, for an order-preserving map $f:W\to W^{\prime}$, the
following are equivalent:

$(i)$

$f$ is a Kripke morphism,

$(ii)$

$f\circ\pi=\pi^{\prime}\circ f$ and
$\pi^{\prime-1}(\uparrow\\!\\!f(k))=f[\pi^{-1}(\uparrow\\!\\!k)]$, for any
$k\in W$.

###### Proof.

To prove $(ii)$ from $(i)$, we first prove $f(\pi(k))=\pi^{\prime}(f(k))$, for
any $k\in W$. By definition, $f$ maps $R$ into $R^{\prime}$, which by
normality means that if $x\leq\pi(y)$ then
$f(x)\leq^{\prime}\pi^{\prime}(f(y))$. Hence, putting $x=\pi(k)$ and $y=k$, we
reach $f(\pi(k))\leq^{\prime}\pi^{\prime}(f(k))$. To prove
$\pi^{\prime}(f(k))\leq^{\prime}f(\pi(k))$, by the third condition in the
definition of a Kripke morphism, we know that for any $l^{\prime}\in
W^{\prime}$ such that $(l^{\prime},f(k))\in R^{\prime}$, there exists $l\in W$
such that $(l,k)\in R$ and $f(l)\geq^{\prime}l^{\prime}$. Put
$l^{\prime}=\pi^{\prime}(f(k))$. It is clear that
$l^{\prime}\leq^{\prime}\pi^{\prime}(f(k))$ and hence $(l^{\prime},f(k))\in
R^{\prime}$. Therefore, there exists $l\in W$ such that $l\leq\pi(k)$ and
$l^{\prime}\leq^{\prime}f(l)$. Since, $f$ is order-preserving, we have
$f(l)\leq^{\prime}f(\pi(k))$. Therefore,
$\pi^{\prime}(f(k))=l^{\prime}\leq^{\prime}f(\pi(k))$ which implies
$\pi^{\prime}(f(k))=f(\pi(k))$.
For the second part of $(ii)$, we first prove the equivalence between
$(f(k),l^{\prime})\in R^{\prime}$ and $l^{\prime}\in
f[\pi^{-1}(\uparrow\\!\\!k)]$, for any $k\in W$ and any $l^{\prime}\in
W^{\prime}$. The forward direction simply is the second condition in the
definition of a Kripke morphism. For the other direction, if there exists
$l\in W$ such that $f(l)=l^{\prime}$ and $k\leq\pi(l)$, then $(k,l)\in R$, by
the normality condition and as $f$ is a Kripke morphism, we have
$(f(k),f(l))\in R^{\prime}$ which implies $(f(k),l^{\prime})\in R^{\prime}$.
Now, to prove the second part of $(ii)$, it is enough to note that for any
$k\in W$ and any $l^{\prime}\in W^{\prime}$, we have the following sequence of
equivalences: $l^{\prime}\in\pi^{\prime-1}(\uparrow\\!\\!f(k))$ iff
$f(k)\leq^{\prime}\pi^{\prime}(l^{\prime})$ iff $(f(k),l^{\prime})\in
R^{\prime}$ iff $l^{\prime}\in f[\pi^{-1}(\uparrow\\!\\!k)]$. Therefore,
$\pi^{\prime-1}(\uparrow\\!\\!f(k))=f[\pi^{-1}(\uparrow\\!\\!k)]$, for any
$k\in W$.
To prove $(i)$ from $(ii)$, we have to check the three conditions in the
definition of a Kripke morphism. For the first condition, if $(k,l)\in R$ then
$k\leq\pi(l)$ which implies $f(k)\leq^{\prime}f(\pi(l))=\pi^{\prime}(f(l))$.
Hence, $(f(k),f(l))\in R^{\prime}$. For the second condition, if
$(f(k),l^{\prime})\in R^{\prime}$, then
$f(k)\leq^{\prime}\pi^{\prime}(l^{\prime})$. Hence,
$l^{\prime}\in\pi^{\prime-1}(\uparrow\\!\\!f(k))$ which implies $l^{\prime}\in
f[\pi^{-1}(\uparrow\\!\\!k)]$. Therefore, there exists $l\in W$ such that
$l^{\prime}=f(l)$ and $k\leq\pi(l)$ which implies $(k,l)\in R$. For the third
condition, if $(l^{\prime},f(k))\in R^{\prime}$, we have
$l^{\prime}\leq^{\prime}\pi^{\prime}(f(k))=f(\pi(k))$. Put $l=\pi(k)$. Then,
$f(l)\geq^{\prime}l^{\prime}$ and $(l,k)\in R$. ∎

As we already observed in Example 3.8, any Kripke frame gives rise to a
$\nabla$-algebra in a canonical way. We now show that this canonical
assignment is a functor and it preserves the conditions $\\{N,R,L,Fa,Fu\\}$.
For that purpose, define the assignment $\mathfrak{U}$ on the object
$\mathcal{K}=(W,\leq,R)$ of the category $\mathbf{K}$ by
$\mathfrak{U}(\mathcal{K})=(U(W,\leq),\nabla_{\mathcal{K}},\to_{\mathcal{K}})$,
where $\nabla_{\mathcal{K}}(U)=\\{x\in X\mid\exists y\in U,(y,x)\in R\\}$ and
$U\to_{\mathcal{K}}V=\\{x\in X\mid\forall y\in U,[(x,y)\in R\Rightarrow y\in
V]\\}$. Moreover, define $\mathfrak{U}$ on the morphism
$f:\mathcal{K}\to\mathcal{K}^{\prime}$ of $\mathbf{K}$ by
$\mathfrak{U}(f)=f^{-1}:\mathfrak{U}(\mathcal{K}^{\prime})\to\mathfrak{U}(\mathcal{K})$.

######  Theorem 6.4.

The assignment $\mathfrak{U}:\mathbf{K}^{op}\to\mathbf{Alg}_{\nabla}(H)$ is a
functor and for any $C\subseteq\\{N,R,L,Fa,Fu\\}$, if
$\mathcal{K}\in\mathbf{K}(C)$, then $\mathfrak{U}(\mathcal{K})$ lands in
$\mathbf{Alg}_{\nabla}(C,H)$. Moreover, the restriction of the functor
$\mathfrak{U}$ to $[\mathbf{K}^{H}(C)]^{op}$ lands in
$\mathbf{Alg}^{H}_{\nabla}(C)$.

###### Proof.

First, we study the object part of the functor. As explained in Example 3.8,
the structure $\mathfrak{U}(W,\leq,R)$ is a Heyting $\nabla$-algebra. For the
conditions $\\{N,R,L\\}$, we refer the reader to [1]. For $(Fa)$, by Theorem
3.13, it is enough to prove $\nabla\Box U=U$, for any upset $U\subseteq W$.
From the adjunction $\nabla\dashv\Box$, it is clear that $\nabla\Box
U\subseteq U$. For the converse, assume $x\in U$. Then, since $(W,\leq,R)$
satisfies $(Fa)$, there exists $y\in W$ such that $(y,x)\in R$ and for any
$z\in W$ such that $(y,z)\in R$, we have $x\leq z$. We claim $y\in\Box U$,
because for any $z\in W$ such that $(y,z)\in R$, we have $x\leq z$ and as $U$
is upward-closed and $x\in U$, we reach $z\in U$. Now, as $(y,x)\in R$ and
$y\in\Box U$, we can conclude $x\in\nabla\Box U$.
For $(Fu)$, using Theorem 3.16, it is enough to prove $\Box\nabla U=U$. Again,
from the adjunction $\nabla\dashv\Box$, it is clear that $U\subseteq\Box\nabla
U$. For the converse, assume $x\in\Box\nabla U$. Since $(W,\leq,R)$ satisfies
$(Fu)$, there exists $y\in W$ such that $(x,y)\in R$ and for any $z\in W$ such
that $(z,y)\in R$, we have $z\leq x$. Since $(x,y)\in R$, we have $y\in\nabla
U$. Therefore, there exists $w\in W$ such that $(w,y)\in R$ and $w\in U$.
Therefore, by $(Fu)$, we have $w\leq x$. Since $U$ is upward-closed, we have
$x\in U$.
For the morphisms, we have to prove that if
$f:(W,\leq,R)\to(W^{\prime},\leq^{\prime},R^{\prime})$ is a Kripke morphism,
then $\mathfrak{U}(f)=f^{-1}$ preserves $\nabla$ and the implication and if
$f$ is also Heyting, $\mathfrak{U}(f)$ also preserves the Heyting implication.
For $\nabla$, consider the following two series of equivalences:

$x\in f^{-1}(\nabla U)\;\;\;\text{iff}\;\;\;f(x)\in\nabla
U\;\;\;\text{iff}\;\;\;\exists y^{\prime}\in U,[(y^{\prime},f(x))\in
R^{\prime}],$

and

$x\in\nabla f^{-1}(U)\;\;\;\text{iff}\;\;\;\exists y\in f^{-1}(U),[(y,x)\in
R].$

Therefore, it is enough to show the equivalence between $\exists y^{\prime}\in
U,[(y^{\prime},f(x))\in R^{\prime}]$ and $\exists y\in f^{-1}(U),[(y,x)\in
R]$. The latter proves the former easily, because $(y,x)\in R$ implies
$(f(y),f(x))\in R^{\prime}$ and it is sufficient to put $y^{\prime}=f(y)$. For
the converse, if there exists $y^{\prime}\in U$ such that
$(y^{\prime},f(x))\in R^{\prime}$, then by part $(iii)$ of the definition of
Kripke morphisms, there exists $y\in W$ such that
$f(y)\geq^{\prime}y^{\prime}$ and $(y,x)\in R$. The only thing to prove is
$f(y)\in U$ which is a consequence of $y^{\prime}\in U$,
$f(y)\geq^{\prime}y^{\prime}$, and the upward-closedness of $U$.
The proof for the Heyting implication is well-known and the case for
implication is similar to that of Heyting implication. Finally, it is clear by
its definition that $\mathfrak{U}$ preserves the identity and the composition.
∎

There is another functor transforming a distributive $\nabla$-algebra to a
Kripke frame. To introduce this functor, we use the usual prime filter
construction, extensively explained in [1]. Here, we recall the construction,
as we need the detailed explanation to establish the construction for faithful
and full distributive $\nabla$-algebras and also to address the morphisms that
are missing in [1]. More importantly, the construction also plays the main
role in the duality theory planned to be covered in the sequel of the present
paper and hence deserves its comprehensive presentation.

Prime Filter Construction. Let $\mathcal{A}=(\mathsf{A},\nabla,\to)$ be a
distributive $\nabla$-algebra. Define
$\mathfrak{P}(\mathcal{A})=(\mathcal{F}_{p}(\mathsf{A}),\subseteq,R_{\mathcal{A}})$,
where $\mathcal{F}_{p}(\mathsf{A})$ is the set of all prime filters of
$\mathsf{A}$ and the relation $R_{\mathcal{A}}$ defined by

$(P,Q)\in R_{\mathcal{A}}$ iff [($a\to b\in P$ and $a\in Q$) implies $b\in
Q$], for any $a,b\in A$.

Moreover, for any $\nabla$-algebra morphism $f:\mathcal{A}\to\mathcal{B}$
define
$\mathfrak{P}(f)=f^{-1}:\mathfrak{P}(\mathcal{B})\to\mathfrak{P}(\mathcal{A})$
and set $i_{\mathcal{A}}:\mathsf{A}\to
U(\mathcal{F}_{p}(\mathsf{A}),\subseteq)$ as
$i_{\mathcal{A}}(a)=\\{P\in\mathcal{F}_{p}(\mathsf{A})\mid a\in P\\}$.

######  Lemma 6.5.

$(P,Q)\in R_{\mathcal{A}}$ iff $\nabla[P]=\\{\nabla x\mid x\in P\\}\subseteq
Q$, for any two prime filters $P$ and $Q$ of $\mathsf{A}$.

###### Proof.

If $(P,Q)\in R_{\mathcal{A}}$ and $x\in P$, since $x\leq 1\to\nabla x$ and $P$
is a filter, $1\to\nabla x\in P$. Therefore, as $1\in Q$ and $(P,Q)\in
R_{\mathcal{A}}$, we reach $\nabla x\in Q$. Conversely, if $\nabla[P]\subseteq
Q$, $a\to b\in P$ and $a\in Q$, then $\nabla(a\to b)\in\nabla[P]\subseteq Q$
and since $a\wedge\nabla(a\to b)\leq b$, we have $b\in Q$. ∎

######  Theorem 6.6.

The assignment $\mathfrak{P}:\mathbf{Alg}_{\nabla}(D)\to\mathbf{K}^{op}$ is a
functor and
$i_{\mathcal{A}}:\mathcal{A}\to\mathfrak{U}\mathfrak{P}(\mathcal{A})$ is a
$\nabla$-algebra embedding, natural in $\mathcal{A}$. Moreover, for any
$C\subseteq\\{N,R,L,Fa,Fu\\}$, if $\mathcal{A}\in\mathbf{Alg}_{\nabla}(C,D)$,
then $\mathfrak{P}(\mathcal{A})$ lands in $[\mathbf{K}(C)]^{op}$. It also maps
$\mathbf{Alg}^{H}_{\nabla}(C)$ to $[\mathbf{K}^{H}(C)]^{op}$ where
$i_{\mathcal{A}}$ becomes a Heyting $\nabla$-algebra morphism.

###### Proof.

For the sake of readability, we split the proof into some parts. First, we
focus on the objects and then we will cover the morphisms.

I. First, note that by Lemma 6.5, it is easy to prove that $R_{\mathcal{A}}$
is compatible with the relation $\subseteq$ which implies that the structure
$\mathfrak{P}(\mathcal{A})$ is actually a Kripke frame. To show that
$i_{\mathcal{A}}$ is a $\nabla$-algebra embedding, note that the following
three facts are well-known: first, $i_{\mathcal{A}}$ is a bounded lattice
embedding, second, it is natural even on all distributive bounded lattices and
the third, if $\mathcal{A}$ is a Heyting algebra, $i_{\mathcal{A}}$ also
preserves the Heyting implication [19, 23]. Therefore, the only thing to check
is the preservation of $\nabla$ and $\to$ which can be found in full detail in
the proof of Theorem 17 in [1].

II. We show that $\mathfrak{P}$ preserves the conditions in the set
$\\{N,R,L,Fa,Fu\\}$. For the conditions $\\{N,R,L\\}$, we refer the reader to
the proof of Theorem 17 in [1]. For the other two conditions, i.e., $(Fa)$ and
$(Fu)$, we have the following:
For $(Fa)$, assume that $\mathcal{A}$ satisfies $(Fa)$. We first show that for
any $P\in\mathcal{F}_{p}(\mathsf{A})$, there exists
$Q\in\mathcal{F}_{p}(\mathsf{A})$ such that $\Box[P]\subseteq
Q\subseteq\nabla^{-1}(P)$, where $\Box[P]=\\{\Box a\mid a\in P\\}$. Define $F$
as the filter generated by $\Box[P]$ and $I$ as the ideal generated by
$(\nabla^{-1}P)^{c}$. We have $F\cap I=\varnothing$. Because, if $x\in F\cap
I$, there are $p_{1},\cdots,p_{n}\in P$ and
$y_{1},\cdots,y_{m}\in(\nabla^{-1}P)^{c}$ such that $\bigwedge_{i=1}^{n}\Box
p_{i}\leq x\leq\bigvee_{j=1}^{m}y_{j}$. Define $p=\bigwedge_{i=1}^{n}p_{i}$.
Since $P$ is a filter, we have $p\in P$. Since $\Box$ commutes with the meets,
we have $\Box p\leq\bigvee_{j=1}^{m}y_{j}$. Hence, $p=\nabla\Box
p\leq\bigvee_{j=1}^{m}\nabla y_{j}$ and as $p\in P$ and $P$ is a filter, we
have $\bigvee_{j=1}^{m}\nabla y_{j}\in P$. Since $P$ is a prime filter, for at
least one $1\leq j\leq m$, we have $\nabla y_{j}\in P$ which is impossible as
$y_{j}\in(\nabla^{-1}P)^{c}$. Hence, $F\cap I=\varnothing$. Therefore, by the
prime filter theorem, Theorem 2.1, there exists a prime filter $Q$ such that
$F\subseteq Q$ and $Q\cap I=\varnothing$. By the first, we can prove
$\Box[P]\subseteq Q$. By the second, we have $Q\subseteq\nabla^{-1}(P)$.
Now, we are ready to prove that $\mathfrak{P}({\mathcal{A}})$ satisfies the
condition $(Fa)$. We have to show that for any prime filter $P$, there exists
a prime filter $Q$ such that $(Q,P)\in R_{\mathcal{A}}$ and for any prime
filter $M$, if $(Q,M)\in R_{\mathcal{A}}$, then $P\subseteq M$. To prove that,
pick an arbitrary prime filter $P$ and set $Q$ as the prime filter constructed
above. Since $Q\subseteq\nabla^{-1}(P)$, we have $\nabla[Q]\subseteq P$ which
implies $(Q,P)\in R_{\mathcal{A}}$, by Lemma 6.5. Let $M$ be a prime filter
such that $(Q,M)\in R_{\mathcal{A}}$. Hence, $\nabla[Q]\subseteq M$, by Lemma
6.5. To show that $P\subseteq M$, let $p\in P$. Then $p=\nabla\Box p$. Hence,
$p\in\nabla[\Box[P]]\subseteq\nabla[Q]\subseteq M$. Therefore, $P\subseteq M$.
For $(Fu)$, assume that $\mathcal{A}$ satisfies $(Fu)$. We first show that for
any $P\in\mathcal{F}_{p}(\mathsf{A})$, there exists
$Q\in\mathcal{F}_{p}(\mathsf{A})$ such that $\nabla[P]\subseteq Q$ and
$\nabla^{-1}(Q)\subseteq P$. Define $F$ as the filter generated by $\nabla[P]$
and $I$ as the ideal generated by $\nabla[P^{c}]$. We have $F\cap
I=\varnothing$. Because, if $x\in F\cap I$, there are $p_{1},\cdots,p_{n}\in
P$ and $y_{1},\cdots,y_{m}\in P^{c}$ such that $\bigwedge_{i=1}^{n}\nabla
p_{i}\leq x\leq\bigvee_{j=1}^{m}\nabla y_{j}$. Define
$p=\bigwedge_{i=1}^{n}p_{i}$. Since $P$ is a filter, we have $p\in P$. Since
$\nabla$ commutes with the joins and $\nabla p\leq\bigwedge_{i=1}^{n}\nabla
p_{i}$, we have $\nabla p\leq\nabla(\bigvee_{j=1}^{m}y_{j})$. Since
$\mathcal{A}$ satisfies $(Fu)$, $\nabla$ is an order embedding by Theorem
3.16. Hence, we have $p\leq\bigvee_{j=1}^{m}y_{j}$. Since $P$ is a prime
filter, for at least one $1\leq j\leq m$, we have $y_{j}\in P$ which is
impossible as $y_{j}\in P^{c}$. Hence, $F\cap I=\varnothing$. Therefore, by
the prime filter theorem, Theorem 2.1, there exists a prime filter $Q$ such
that $F\subseteq Q$ and $Q\cap I=\varnothing$. By the first, we can prove
$\nabla[P]\subseteq Q$. By the second, we have $\nabla^{-1}(Q)\subseteq P$,
because if $x\in\nabla^{-1}(Q)$ and $x\notin P$, then $\nabla x\in
Q\cap\nabla[P^{c}]$ which is impossible.
Now, we can prove that $\mathfrak{P}({\mathcal{A}})$ satisfies the condition
$(Fu)$. We have to show that for any prime filter $P$, there exists a prime
filter $Q$ such that $(P,Q)\in R_{\mathcal{A}}$ and for any prime filter $M$,
if $(M,Q)\in R_{\mathcal{A}}$, then $M\subseteq P$. Let $P$ be an arbitrary
prime filter. Pick $Q$ as the prime filter constructed above. Since
$\nabla[P]\subseteq Q$, we have $(P,Q)\in R_{\mathcal{A}}$, by Lemma 6.5. Let
$M$ be a prime filter such that $(M,Q)\in R_{\mathcal{A}}$. We have to show
that $M\subseteq P$. Since $(M,Q)\in R_{\mathcal{A}}$, by Lemma 6.5, we have
$\nabla[M]\subseteq Q$ and hence $M\subseteq\nabla^{-1}(Q)\subseteq P$.

III. To address the morphisms, i.e., to show that if
$f:\mathcal{A}\to\mathcal{B}$ is a $\nabla$-algebra morphism,
$\mathfrak{P}(f)=f^{-1}:(\mathcal{F}_{p}(\mathsf{B}),\subseteq,R_{\mathcal{B}})\to(\mathcal{F}_{p}(\mathsf{A}),\subseteq,R_{\mathcal{A}})$
is a Kripke morphism, we have to check the three conditions in the definition
of a Kripke morphism. First, we show that $(P,Q)\in R_{\mathcal{B}}$ implies
$(f^{-1}(P),f^{-1}(Q))\in R_{\mathcal{A}}$, for any
$P,Q\in\mathcal{F}_{p}(\mathsf{B})$. First, note that by the fact that $f$
preserves $\nabla$, we have $\nabla_{\mathcal{A}}[f^{-1}(P)]\subseteq
f^{-1}(\nabla_{\mathcal{B}}[P])$. The reason is that if $x\in f^{-1}(P)$, then
as
$f(\nabla_{\mathcal{A}}x)=\nabla_{\mathcal{B}}f(x)\in\nabla_{\mathcal{B}}[P]$,
we have $\nabla_{\mathcal{A}}x\in f^{-1}(\nabla_{\mathcal{B}}[P])$. Now,
assume $(P,Q)\in R_{\mathcal{B}}$. By Lemma 6.5, we have
$\nabla_{\mathcal{B}}[P]\subseteq Q$ which implies
$\nabla_{\mathcal{A}}[f^{-1}(P)]\subseteq
f^{-1}(\nabla_{\mathcal{B}}[P])\subseteq f^{-1}(Q)$, and hence
$(f^{-1}(P),f^{-1}(Q))\in R_{\mathcal{A}}$, by Lemma 6.5.
For the second condition, assume $(f^{-1}(P^{\prime}),Q)\in R_{\mathcal{A}}$,
for some $P^{\prime}\in\mathcal{F}_{p}(\mathsf{B})$ and
$Q\in\mathcal{F}_{p}(\mathsf{A})$. We have to provide
$Q^{\prime}\in\mathcal{F}_{p}(\mathsf{B})$ such that
$(P^{\prime},Q^{\prime})\in R_{\mathcal{B}}$ and $f^{-1}(Q^{\prime})=Q$.
Define $I$ as the ideal generated by $f[Q^{c}]$ and $F$ as the filter
generated by $\nabla_{\mathcal{B}}[P^{\prime}]\cup f[Q]$. We claim that $F\cap
I=\varnothing$. Assume $x\in F\cap I$. Then, there exist
$y_{1},\cdots,y_{m}\in Q^{c}$, $z_{1},\cdots,z_{n}\in Q$ and
$w_{1},\cdots,w_{k}\in P^{\prime}$ such that
$\bigwedge_{j=1}^{n}f(z_{j})\wedge\bigwedge_{r=1}^{k}\nabla_{\mathcal{B}}w_{r}\leq
x\leq\bigvee_{i=1}^{m}f(y_{i})$. Define $z=\bigwedge_{j=1}^{n}z_{j}$,
$w=\bigwedge_{r=1}^{k}w_{r}$ and note that $z\in Q$ and $w\in P^{\prime}$,
since both $Q$ and $P^{\prime}$ are filters. Then, by the monotonicity of
$\nabla_{\mathcal{B}}$ and the fact that $f$ is a $\nabla$-algebra morphism,
we have $\nabla_{\mathcal{B}}w\wedge f(z)\leq f(\bigvee_{i=1}^{m}y_{i})$.
Therefore,
$w\leq_{\mathcal{B}}f(z)\to_{\mathcal{B}}f(\bigvee_{i=1}^{m}y_{i})=f(z\to_{\mathcal{A}}\bigvee_{i=1}^{m}y_{i})$.
Since $w\in P^{\prime}$, we have
$f(z\to_{\mathcal{A}}\bigvee_{i=1}^{m}y_{i})\in P^{\prime}$ which implies
$z\to_{\mathcal{A}}\bigvee_{i=1}^{m}y_{i}\in f^{-1}(P^{\prime})$ and hence
$\nabla_{\mathcal{A}}(z\to_{\mathcal{A}}\bigvee_{i=1}^{m}y_{i})\in\nabla_{\mathcal{A}}[f^{-1}(P^{\prime})]$.
Since $(f^{-1}(P^{\prime}),Q)\in R_{\mathcal{A}}$, by Lemma 6.5, we have
$\nabla_{\mathcal{A}}[f^{-1}(P^{\prime})]\subseteq Q$. Hence,
$\nabla_{\mathcal{A}}(z\to_{\mathcal{A}}\bigvee_{i=1}^{m}y_{i})\in Q$. Since
$z\in Q$ and
$z\wedge\nabla_{\mathcal{A}}(z\to_{\mathcal{A}}\bigvee_{i=1}^{m}y_{i})\leq\bigvee_{i=1}^{m}y_{i}$,
we have $\bigvee_{i=1}^{m}y_{i}\in Q$. Since $Q$ is prime, for some $1\leq
i\leq m$, we must have $y_{i}\in Q$ which is a contradiction with the choice
of $y_{i}$. Therefore, $F\cap I=\varnothing$. Now, by the prime filter
theorem, Theorem 2.1, there exists a prime filter
$Q^{\prime}\in\mathcal{F}_{p}(\mathsf{B})$ such that $F\subseteq Q^{\prime}$
and $Q^{\prime}\cap I=\varnothing$. The first implies
$\nabla_{\mathcal{B}}[P^{\prime}]\cup f[Q]\subseteq Q^{\prime}$ which also
implies $(P^{\prime},Q^{\prime})\in R_{\mathcal{B}}$ and $Q\subseteq
f^{-1}(Q^{\prime})$. From the second, we have $f^{-1}(Q^{\prime})\subseteq Q$,
because if $x\in f^{-1}(Q^{\prime})$ and $x\notin Q$, then $x\in Q^{c}$ and
hence $f(x)\in I$ which implies the contradictory result $f(x)\in
Q^{\prime}\cap I$. Hence, $f^{-1}(Q^{\prime})=Q$.
For the third condition, let us assume $(Q,f^{-1}(P^{\prime}))\in
R_{\mathcal{A}}$, for some $P^{\prime}\in\mathcal{F}_{p}(\mathsf{B})$ and
$Q\in\mathcal{F}_{p}(\mathsf{A})$. We have to find a prime filter
$Q^{\prime}\in\mathcal{F}_{p}(\mathsf{B})$ such that
$(Q^{\prime},P^{\prime})\in R_{\mathcal{B}}$ and $Q\subseteq
f^{-1}(Q^{\prime})$. Define $I$ as the ideal generated by
$(\nabla^{-1}_{\mathcal{B}}[P^{\prime}])^{c}$ and $F$ as the filter generated
by $f[Q]$. We have $F\cap I=\varnothing$, because if $x\in I\cap F$, then,
there exist $y_{1},\cdots,y_{m}\notin\nabla^{-1}_{\mathcal{B}}[P^{\prime}]$
and $z_{1},\cdots,z_{n}\in Q$ such that $\bigwedge_{i=1}^{n}f(z_{i})\leq
x\leq\bigvee_{j=1}^{m}y_{j}$. Define $z=\bigwedge_{i=1}^{n}z_{i}$ and note
that $z\in Q$, since $Q$ is a filter. Since $f$ is a $\nabla$-algebra
morphism, $f(z)\leq\bigvee_{j=1}^{m}y_{j}$. Therefore,
$f(\nabla_{\mathcal{A}}z)=\nabla_{\mathcal{B}}f(z)\leq\bigvee_{j=1}^{m}\nabla_{\mathcal{B}}y_{j}$.
Since $(Q,f^{-1}(P^{\prime}))\in R_{\mathcal{A}}$, by Lemma 6.5, we have
$\nabla_{\mathcal{A}}[Q]\subseteq f^{-1}(P^{\prime})$. Since $z\in Q$, we have
$f(\nabla_{\mathcal{A}}z)\in P^{\prime}$ and hence
$\bigvee_{j=1}^{m}\nabla_{\mathcal{B}}y_{j}\in P^{\prime}$. Since $P^{\prime}$
is prime, for some $1\leq j\leq m$, we have $\nabla_{\mathcal{B}}y_{j}\in
P^{\prime}$ which contradicts
$y_{j}\notin\nabla^{-1}_{\mathcal{B}}[P^{\prime}]$. Hence, $F\cap
I=\varnothing$. Therefore, by the prime filter theorem, Theorem 2.1, there
exists a prime filter $Q^{\prime}\in\mathcal{F}_{p}(\mathcal{B})$ such that
$F\subseteq Q^{\prime}$ and $Q^{\prime}\cap I=\varnothing$. The first implies
$f[Q]\subseteq Q^{\prime}$ and hence $Q\subseteq f^{-1}(Q^{\prime})$ and the
second implies $Q^{\prime}\subseteq\nabla^{-1}_{\mathcal{B}}(P^{\prime})$
which means $\nabla_{\mathcal{B}}[Q^{\prime}]\subseteq P^{\prime}$ and by
Lemma 6.5, $(Q^{\prime},P^{\prime})\in R_{\mathcal{B}}$.
For the Heyting $\nabla$-algebra morphisms, it is a well-known fact that if
$f$ preserves the Heyting implication, then $f^{-1}$ satisfies the fourth
condition in the definition of Heyting Kripke morphisms, see Theorem 3.3.4 in
[19]. Finally, note that $\mathfrak{P}$ clearly preserves the identity and the
composition. ∎

###  6.1 Amalgamation Property

In this subsection, we use the provided Kripke representation of distributive
$\nabla$-algebras to prove the amalgamation property for the varieties
$\mathcal{V}(C,D,N)$ and $\mathcal{V}_{H}(C,N)$, for any
$C\subseteq\\{R,L,Fa\\}$.

######  Definition 6.7.

A class $\mathfrak{C}$ of $\nabla$-algebras has the amalgamation property if
for any $\mathcal{A}_{0},\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ in
$\mathfrak{C}$ and any $\nabla$-algebra embeddings
$f_{1}:\mathcal{A}_{0}\longrightarrow\mathcal{A}_{1}$ and
$f_{2}:\mathcal{A}_{0}\longrightarrow\mathcal{A}_{2}$, there exist a
$\nabla$-algebra $\mathcal{B}$ in $\mathfrak{C}$ and $\nabla$-algebra
embeddings $g_{1}:\mathcal{A}_{1}\longrightarrow\mathcal{B}$ and
$g_{2}:\mathcal{A}_{2}\longrightarrow\mathcal{B}$ such that $g_{1}\circ
f_{1}=g_{2}\circ f_{2}$:

${{\mathcal{A}_{1}}}$${{\mathcal{A}_{0}}}$${{\mathcal{B}}}$${{\mathcal{A}_{2}}}$$\scriptstyle{f_{1}}$$\scriptstyle{f_{2}}$$\scriptstyle{g_{1}}$$\scriptstyle{g_{2}}$

The amalgamation property for a class of explicitly Heyting $\nabla$-algebras
is defined similarly, replacing $\nabla$-algebra morphisms by Heyting
$\nabla$-algebra morphisms, everywhere.

Our strategy to prove the amalgamation property is to transform the property
to the dual property for the Kripke frames where constructing the new frames
is rather easier. For that purpose, we need the following well-known fact for
which we also provide a proof for the sake of completeness:

######  Lemma 6.8.

Let $\mathsf{A}$ and $\mathsf{B}$ be two bounded distributive lattices and
$f:\mathsf{A}\to\mathsf{B}$ be an injective bounded lattice map. Then, the map
$f^{-1}:\mathcal{F}_{p}(\mathsf{B)}\to\mathcal{F}_{p}(\mathsf{A)}$ is
surjective. Therefore, the functor $\mathfrak{P}$ maps the injective
$\nabla$-algebra morphisms to surjective Kripke morphisms. Conversely, the
functor $\mathfrak{U}$ maps surjective Kripke morphisms to injective
$\nabla$-algebra morphisms.

###### Proof.

The last part is an easy consequence of the fact that if $f:W_{1}\to W_{2}$ is
surjective, then $\mathfrak{U}(f)=f^{-1}$ is one-to-one. For the first part,
assume that $f:\mathsf{A}\to\mathsf{B}$ is a one-to-one bounded lattice
morphism. Then, we want to prove that for any
$P\in\mathcal{F}_{p}(\mathsf{A})$, there exists
$Q\in\mathcal{F}_{p}(\mathsf{B})$ such that $f^{-1}(Q)=P$. Define $F$ as the
filter generated by $f[P]$ and $I$ as the ideal generated by $f[P^{c}]$. We
have $F\cap I=\varnothing$, because if $x\in F\cap I$, then there exist
$p_{1},\cdots,p_{m}\in P$ and $y_{1},\cdots,y_{n}\in P^{c}$ such that
$\bigwedge_{i=1}^{m}f(p_{i})\leq x\leq\bigvee_{j=1}^{n}f(y_{j})$. Since $f$ is
a bounded lattice morphism, we have $f(\bigwedge_{i=1}^{m}p_{i})\leq
f(\bigvee_{j=1}^{n}y_{j})$. Since $f$ is one-to-one, it is an order embedding
and hence, we have $\bigwedge_{i=1}^{m}p_{i}\leq\bigvee_{j=1}^{n}y_{j}$. Since
$P$ is a prime filter, for at least one $1\leq j\leq n$, we must have
$y_{j}\in P$ which contradicts with the choice of $y_{j}$. Hence, $F\cap
I=\varnothing$. Now, by the prime filter theorem, Theorem 2.1, there exists a
prime filter $Q\in\mathcal{F}_{p}(\mathsf{B})$ such that $F\subseteq Q$ and
$Q\cap I=\varnothing$. From the first, we have $f[P]\subseteq Q$ which implies
$P\subseteq f^{-1}(Q)$ and from the second $f^{-1}(Q)\subseteq P$. Hence,
$f^{-1}(Q)=P$. ∎

The next lemma is the dual property we promised to prove.

######  Lemma 6.9.

Let $C\subseteq\\{R,L,Fa\\}$. Then, for any normal Kripke frames
$\mathcal{K}_{0}=(W_{0},\leq_{0},R_{0})$,
$\mathcal{K}_{1}=(W_{1},\leq_{1},R_{1})$ and
$\mathcal{K}_{2}=(W_{2},\leq_{2},R_{2})$ in $\mathbf{K}(C,N)$ and any
surjective Kripke morphisms $f:\mathcal{K}_{1}\to\mathcal{K}_{0}$ and
$g:\mathcal{K}_{2}\to\mathcal{K}_{0}$, there exist a Kripke frame
$\mathcal{K}\in\mathbf{K}(C,N)$ and surjective Kripke morphisms
$p:\mathcal{K}\to\mathcal{K}_{1}$ and $q:\mathcal{K}\to\mathcal{K}_{2}$ such
that $f\circ p=g\circ q$:

${{\mathcal{K}_{1}}}$${{\mathcal{K}}}$${{\mathcal{K}_{0}}}$${{\mathcal{K}_{2}}}$$\scriptstyle{p}$$\scriptstyle{q}$$\scriptstyle{f}$$\scriptstyle{g}$

Moreover, if $f$ and $g$ are Heyting, so are $p$ and $q$.

###### Proof.

Define $W=\\{(y,z)\in W_{1}\times W_{2}\mid f(y)=g(z)\\}$,
$\leq\;=(\leq_{1}\times\leq_{2})|_{W}$ and $R=(R_{1}\times R_{2})|_{W}$. It is
easy to see that $\mathcal{K}=(W,\leq,R)$ is a Kripke frame, as $R$ is clearly
compatible with $\leq$. To prove that $\mathcal{K}$ is normal, assume that
$\pi_{1}:W_{1}\to W_{1}$ and $\pi_{2}:W_{2}\to W_{2}$ are the normality
witnesses of $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$, respectively. Define
$\pi:W\to W$ by $\pi(y,z)=(\pi_{1}(y),\pi_{2}(z))$. It is well-defined, i.e.,
$\pi(y,z)\in W$, for any $(y,z)\in W$. Because, $(y,z)\in W$ implies
$f(y)=g(z)$ and since $f$ and $g$ are Kripke morphisms, by Lemma 6.3, we have
$f(\pi_{1}(y))=\pi_{0}(f(y))=\pi_{0}(g(z))=g(\pi_{2}(z))$ which implies
$(\pi_{1}(y),\pi_{2}(z))\in W$. The function $\pi$ also respects the order
$\leq$ and we have $((y,z),(y^{\prime},z^{\prime}))\in R$ iff
$(y,z)\leq\pi(y^{\prime},z^{\prime})$. Hence, $\mathcal{K}$ is normal. To show
that $\mathcal{K}\in\mathbf{K}(C)$, using Lemma 6.2, the conditions
$\\{L,R,Fa\\}$ for $\mathcal{K}$ are equivalent to $\pi(y,z)\leq(y,z)$,
$(y,z)\leq\pi(y,z)$ and the condition that $\pi$ is an order embedding,
respectively. All the three are inherited from $\mathcal{K}_{1}$ and
$\mathcal{K}_{2}$ to their product and since they are universal conditions, to
the frame $\mathcal{K}$.
Now, set $p:W\to W_{1}$ and $q:W\to W_{2}$ as the projection functions. By the
definition of $W$, it is clear that $f\circ p=g\circ q$. We only need to prove
that $p$ and $q$ are surjective Kripke morphisms. We prove the claim for $p$.
The case for $q$ is similar. First, note that $p$ is surjective, because for
any $y\in W_{1}$, there exists $z\in W_{2}$ such that $f(y)=g(z)$, simply
because $g$ is surjective. Therefore, $(y,z)\in W$ and as $p(y,z)=y$, the
surjectivity of $p$ is established. Secondly, $p$ is a Kripke morphism. To
prove, by Lemma 6.3, it is enough to show that $p\circ\pi=\pi_{1}\circ p$ and
$\pi_{1}^{-1}(\uparrow\\!\\!p(x,y))=p[\pi^{-1}(\uparrow\\!\\!(x,y))]$, for any
$(x,y)\in W$. The first part, i.e., $p\circ\pi=\pi_{1}\circ p$ is clear from
the definition. For the second, for any $(x,y)\in W$ and $z\in W_{1}$, note
that we have the following equivalences:

$z\in\pi_{1}^{-1}(\uparrow\\!\\!p(x,y))\quad\text{iff}\quad
x\leq_{1}\pi_{1}(z),$ $z\in
p[\pi^{-1}(\uparrow\\!\\!(x,y))]\quad\text{iff}\quad\exists u\in
W_{2}[(z,u)\in W\,\&\,(x,y)\leq(\pi_{1}(z),\pi_{2}(u))].$

Therefore, it is enough to prove the equivalence between the two right hand
sides. The upward direction is clear. For the downward direction, if
$x\leq_{1}\pi_{1}(z)$, then $(x,z)\in R_{1}$. As $f$ is a Kripke morphim,
$(f(x),f(z))\in R_{0}$. As $(x,y)\in W$, we have $f(x)=g(y)$. Hence,
$(g(y),f(z))\in R_{0}$. As $g$ is a Kripke morphism, there must be $u\in
W_{2}$ such that $(y,u)\in R_{2}$ and $g(u)=f(z)$. Therefore, $(z,u)\in W$ and
$y\leq_{2}\pi_{2}(u)$ which completes the proof. The proof to show that $p$
and $q$ are Heyting, if $f$ and $g$ are Heyting is similar. ∎

######  Theorem 6.10.

(Amalgamation) Let $C\subseteq\\{R,L,Fa\\}$. Then, the varieties
$\mathcal{V}(C,D,N)$ and $\mathcal{V}_{H}(C,N)$ have the amalgamation
property.

###### Proof.

We first prove the claim for $\mathcal{V}(C,D,N)$. Let
$\mathcal{A}_{0},\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ be some
$\nabla$-algebras in $\mathcal{V}(C,D,N)$ and
$f_{1}:\mathcal{A}_{0}\longrightarrow\mathcal{A}_{1}$ and
$f_{2}:\mathcal{A}_{0}\longrightarrow\mathcal{A}_{2}$ are some embeddings.
Applying the functor $\mathfrak{P}$, by Theorem 6.6, we reach the normal
Kripke models $\mathcal{K}_{i}=\mathfrak{P}(\mathcal{A}_{i})$ in
$\mathbf{K}(C,N)$, for $i=0,1,2$ and Kripke morphisms
$f=\mathfrak{P}(f_{1}):\mathcal{K}_{1}\to\mathcal{K}_{0}$ and
$g=\mathfrak{P}(f_{2}):\mathcal{K}_{2}\to\mathcal{K}_{0}$. By Lemma 6.8, we
know that the maps $f$ and $g$ are surjective. By Lemma 6.9, there exist a
Kripke frame $\mathcal{K}\in\mathbf{K}(C,N)$ and surjective Kripke morphisms
$p:\mathcal{K}\to\mathcal{K}_{1}$ and $q:\mathcal{K}\to\mathcal{K}_{2}$ such
that $f\circ p=g\circ q$:

${{\mathcal{K}_{1}=\mathfrak{P}(\mathcal{A}_{1})}}$${{\mathcal{K}}}$${{\mathcal{K}_{0}=\mathfrak{P}(\mathcal{A}_{0})}}$${{\mathcal{K}_{2}=\mathfrak{P}(\mathcal{A}_{2})}}$$\scriptstyle{p}$$\scriptstyle{q}$$\scriptstyle{f=\mathfrak{P}(f_{1})}$$\scriptstyle{g=\mathfrak{P}(f_{2})}$

Now, apply the functor $\mathfrak{U}$ to the previous diagram and use Thoerem
6.4 to land inside $\mathcal{V}(C,D,N)$. By Lemma 6.8, the maps
$\mathfrak{U}(p)$ and $\mathfrak{U}(q)$ are embeddings. Therefore, as
$i_{\mathcal{A}}:\mathcal{A}\to\mathfrak{U}\mathfrak{P}(\mathcal{A})$ is an
embedding and also natural in $\mathcal{A}$, we have the following commutative
diagram of $\nabla$-algebras in $\mathcal{V}(C,D,N)$:

${{\mathcal{A}_{0}}}$${{\mathcal{A}_{2}}}$${{\mathfrak{UP}(\mathcal{A}_{0})}}$${{\mathfrak{UP}(\mathcal{A}_{2})}}$${{\mathcal{A}_{1}}}$${{\mathfrak{UP}(\mathcal{A}_{1})}}$${{\mathfrak{U}(\mathcal{K})}}$$\scriptstyle{\mathfrak{UP}(f_{2})}$$\scriptstyle{\mathfrak{UP}(f_{1})}$$\scriptstyle{\mathfrak{U}(q)}$$\scriptstyle{\mathfrak{U}(p)}$$\scriptstyle{i_{\mathcal{A}_{0}}}$$\scriptstyle{i_{\mathcal{A}_{1}}}$$\scriptstyle{i_{\mathcal{A}_{2}}}$$\scriptstyle{f_{1}}$$\scriptstyle{f_{2}}$

Now, it is enough to set $\mathcal{A}=\mathfrak{U}(\mathcal{K})$ and
$g_{1}=\mathfrak{U}(p)\circ i_{\mathcal{A}_{1}}$ and
$g_{2}=\mathfrak{U}(q)\circ i_{\mathcal{A}_{2}}$.
Finally, to address the case $\mathcal{V}_{H}(C,N)$, note that if $f_{1}$ and
$f_{2}$ preserve the Heyting implication, then by Theorem 6.6, the maps
$\mathfrak{P}(f_{1})$ and $\mathfrak{P}(f_{2})$ are Heyting. Then, by Lemma
6.9, the maps $p$ and $q$ are Heyting Kripke morphisms which implies that the
maps $\mathfrak{U}(p)$ and $\mathfrak{U}(q)$ preserve the Heyting implication,
by Theorem 6.4. Finally, as $i_{\mathcal{A}_{1}}$ and $i_{\mathcal{A}_{2}}$
also preserve the Heyting implication, by Theorem 6.6, the maps $g_{1}$ and
$g_{2}$ preserve the Heyting implication, as well. ∎

Acknowledgments: We wish to thank Nick Bezhanishvili for his helpful
suggestions and the anonymous referees whose suggestions helped to improve our
presentation. The first author also gratefully acknowledges the support of the
FWF project P 33548. He is also supported by the Czech Academy of Sciences
(RVO 67985840).

## References

  * [1] Amirhossein Akbar Tabatabai.  Implication via spacetime.  Mathematics, Logic, and their Philosophies: Essays in Honour of Mohammad Ardeshir, pages 161–216, 2021.
  * [2] Ethan Akin.  The general topology of dynamical systems.  Graduate Studies in Mathematics, 2010.
  * [3] Mohammad Ardeshir.  Aspects of Basic Logic.  PhD thesis, Marquette University, 1995.
  * [4] Mohammad Ardeshir and Wim Ruitenburg.  Basic propositional calculus. I.  MLQ Math. Log. Q., 44(3):317–343, 1998.
  * [5] Mohammad Ardeshir and Wim Ruitenburg.  Latarres, lattices with an arrow.  Studia Logica, 106(4):757–788, 2018.
  * [6] SN Artemov, JM Davoren, and A Nerode.  Modal logics and topological semantics for hybrid systems.  1997\.
  * [7] Philippe Balbiani, Joseph Boudou, Martín Diéguez, and David Fernández-Duque.  Bisimulations for intuitionistic temporal logics.  J. Appl. Logics, 8(8):2265–2285, 2021.
  * [8] Guram Bezhanishvili, Nick Bezhanishvili, David Gabelaia, and Alexander Kurz.  Bitopological duality for distributive lattices and Heyting algebras.  Math. Structures Comput. Sci., 20(3):359–393, 2010.
  * [9] Francis Borceux.  Handbook of categorical algebra 1.  Encyclopedia of Mathematics and its Applications, Vol. 50, Cambridge University Press, Cambridge, 1994.
  * [10] Joseph Boudou, Martín Diéguez, and David Fernández-Duque.  A decidable intuitionistic temporal logic.  In 26th EACSL annual conference on Computer Science Logic (CSL 2017), volume 82. Schloss Dagstuhl. Leibniz-Zentrum für Informatik, 2017.
  * [11] Stanley Burris and H. P. Sankappanavar.  A course in universal algebra.  Graduate Texts in Mathematics, Vol. 78, Springer-Verlag, New York-Berlin, 1981.
  * [12] Sergio Celani and Ramon Jansana.  Bounded distributive lattices with strict implication.  MLQ Math. Log. Q., 51(3):219–246, 2005.
  * [13] Ivan Chajda.  Algebraic axiomatization of tense intuitionistic logic.  Cent. Eur. J. Math., 9(5):1185–1191, 2011.
  * [14] Willem Conradie, Alessandra Palmigiano, Sumit Sourabh, and Zhiguang Zhao.  Canonicity and relativized canonicity via pseudo-correspondence: an application of alba.  arXiv preprint arXiv:1511.04271, 2015.
  * [15] Charles B Cross.  Nute donald. conditional logic. handbook of philosophical logic, volume ii, extensions of classical logic, edited by gabbay d. and guenthner f., synthese library, vol. 165, d. reidel publishing company, dordrecht, boston, and lancaster, 1984, pp. 387–439.  1989\.
  * [16] Rowan Davies.  A temporal logic approach to binding-time analysis.  J. ACM, 64(1):Art. 1, 45, 2017.
  * [17] Valeria de Paiva and Harley Eades III.  Constructive temporal logic, categorically.  IfCoLog Journal of Logics and their Applications, page 1287, 2017.
  * [18] Leo Esakia.  The modalized Heyting calculus: a conservative modal extension of the intuitionistic logic.  J. Appl. Non-Classical Logics, 16(3-4):349–366, 2006.
  * [19] Leo Esakia.  Heyting algebras.  Trends in Logic—Studia Logica Library, Vol. 50, 2019.
  * [20] W. B. Ewald.  Intuitionistic tense and modal logic.  J. Symbolic Logic, 51(1):166–179, 1986.
  * [21] David Fernández-Duque.  The intuitionistic temporal logic of dynamical systems.  Log. Methods Comput. Sci., 14(3):Paper No. 3, 35, 2018.
  * [22] Gisèle Fischer-Servi.  On modal logic with an intuitionistic base.  Studia Logica, 36(3):141–149, 1977.
  * [23] Melvin Chris Fitting.  Intuitionistic logic, model theory and forcing.  Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam-London, page 191, 1969.
  * [24] Silvio Ghilardi and Giancarlo Meloni.  Constructive canonicity in non-classical logics.  Ann. Pure Appl. Logic, 86(1):1–32, 1997.
  * [25] John Harding and Guram Bezhanishvili.  MacNeille completions of Heyting algebras.  Houston J. Math., 30(4):937–952, 2004.
  * [26] Rosalie Iemhoff.  Preservativity logic: an analogue of interpretability logic for constructive theories.  MLQ Math. Log. Q., 49(3):230–249, 2003.
  * [27] Rosalie Iemhoff, Dick de Jongh, and Chunlai Zhou.  Properties of intuitionistic provability and preservativity logics.  Log. J. IGPL, 13(6):615–636, 2005.
  * [28] Peter T. Johnstone.  Stone spaces.  Cambridge Studies in Advanced Mathematics, Vol. 3, Cambridge University Press, Cambridge, 1982.
  * [29] Norihiro Kamide and Heinrich Wansing.  Combining linear-time temporal logic with constructiveness and paraconsistency.  J. Appl. Log., 8(1):33–61, 2010.