On the free frontal implicative semilattice extension of a frontal Hilbert algebra

Abstract

In this paper, we define a functor which is left adjoint to the forgetful functor from the category of frontal implicative semilattices to that of frontal Hilbert algebras.

1 Introduction

Frontal Heyting algebras were introduced by Esakia in Esakia (2006) as the algebraic models of the modalized Heyting calculus mHC. They are Heyting algebras expanded with a unary modal box-like operation with the algebraic properties of the co-derivative operator¹ of a topological space when it is applied to the Heyting algebra of its open sets.

In Castiglioni and San Martín (2015), the notion of frontal operator is generalized to Hilbert algebras, and hence to implicative semilattices, as well as are the frontal operators $\gamma$, S and G considered in the framework of Heyting algebras by Caicedo and Cignoli (2001) (Examples 3.1, 5.2 and 5.3, respectively). The operators $\gamma$, S and G are particular examples of implicitly definable compatible functions (see also Kaarli and Pixley 2001 for information on compatible functions).

The variety of Hilbert algebras is the class of the subreducts to the language $\{\rightarrow , 1\}$ of the Heyting algebras as well as of the implicative semilattices. Similarly, the variety of frontal Hilbert algebras is the class of the subreducts to the language $\{\rightarrow , \tau , 1\}$ of the frontal Heyting algebras and of the frontal implicative semilattices, as follows from Corollary 24.

Mal’cev (1971) showed that if ${\mathcal {L}}'$ is a sublanguage of the language ${\mathcal {L}}$ of a quasivariety ${\mathsf {K}}$, then the class ${\mathsf {M}}$ of the ${\mathcal {L}}'$-subreducts of the members of ${\mathsf {K}}$ is also a quasivariety. When equipped with homomorphisms, the quasivarieties ${\mathsf {K}}$ and ${\mathsf {M}}$ can be viewed as concrete categories. It is then immediate to see that the obvious forgetful construction ${\mathrm {U}}$ from ${\mathsf {K}}$ to ${\mathsf {M}}$ is a right adjoint functor. Then, if $\mathrm {F}: {\mathsf {M}} \rightarrow {\mathsf {K}}$ is a left adjoint functor to ${\mathrm {U}}$, for every algebra $A \in {\mathsf {M}}$, the algebra $\mathrm {F}(A)$ is the most generic member B of ${\mathsf {K}}$ such that A is isomorphic to a subalgebra C of the ${\mathcal {L}}'$-reduct of B and B is generated (in the full language ${\mathcal {L}}$) by C. The algebra $\mathrm {F}(A)$ is sometimes called the free ${\mathsf {K}}$-extension of A. A natural quest is then to find concrete descriptions of a functor $\mathrm {F}: {\mathsf {M}} \rightarrow {\mathsf {K}}$ which is left adjoint to U that accordingly provides concrete descriptions of the free ${\mathsf {K}}$-extensions of the members of ${\mathsf {M}}$.

In Celani and Jansana (2012), an explicit definition of a left adjoint to the forgetful functor from the category of implicative semilattices to the category of Hilbert algebras is given. In Castiglioni and San Martín (2018), another explicit description of such an adjoint functor was presented following an alternative path. The main goal of this paper is to obtain an explicit definition of a left adjoint functor to the forgetful functor from the category of frontal implicative semilattices to the category of frontal Hilbert algebras, thus providing for every frontal Hilbert algebra a specific construction of its free extension to a frontal implicative semilattice. Building on it, we also obtain left adjoint functors to the forgetful functors from the categories of bounded implicative semilattices with a $\gamma$-function, implicative semilattices with a successor function, and bounded implicative semilattices with a Gabbay function to the categories of bounded Hilbert algebras augmented, respectively, with a $\gamma$-function, a successor function, and a Gabbay function.

The paper is organized as follows. In Sect. 2, we introduce the preliminaries we need; they include the main properties concerning frontal operators in Heyting algebras and in Hilbert algebras we use. We also present the explicit description of a left adjoint to the forgetful functor from the category of implicative semilattices to the category of Hilbert algebras: we use it in Sect. 3 to obtain our left adjoint functor to the forgetful functor from the category of frontal implicative semilattices to the category of frontal Hilbert algebras. In Sects. 4, 5 and 6, we use the adjunctions presented in Sect. 3 in order to obtain a similar result for some categories of frontal implicative semilattices and frontal Hilbert algebras determined by the notions of $\gamma$-function, successor function, and Gabbay function.

2 Preliminaries

We start with the basic notions on posets we need along the paper. Let $P = (P,\le )$ be a poset. A subset $U\subseteq P$ is said to be an upset if for all $x, y \in P$ such that $x\in U$ and $x\le y$ we have $y\in U$. The notion of downset is defined dually. The upset generated by a set $Y \subseteq P$ is the set $[Y) := \{x\in P: (\exists y\in Y)\ y\le x\}$ and the downset generated by Y is the set $(Y] := \{x\in P:(\exists y\in Y)\ x\le y\}$. If $Y = \{y\}$, then we write [y) and (y] instead of $[\{y\})$ and $(\{y\}]$, respectively. A set $I \subseteq P$ is an order-ideal if I is a nonempty downset that is up-directed, namely that for every $x, y \in I$ there is $z \in I$ such that $x \le z$ and $y \le z$. Dually, we have the notion of order-filter, but we will not use this notion in the paper.

Given a set X and a set $Y \subseteq X$, we denote the relative complement of Y to X, i.e., $X{\setminus }Y$, by $Y^{c}$, that is $Y^{c}:=\{x \in X: x \not \in Y\}$. The context will always make it clear with respect to which set we are taking the relative complement.

We assume the reader is familiar with the theory of Heyting algebras (Balbes and Dwinger 1974; Esakia 2019; Rasiowa 1974) and propositional intuitionistic calculus, of which the variety of Heyting algebras is the algebraic counterpart. We recall that the lattice of all open sets of a topological space X is a Heyting algebra where the implication from an open set U to an open set V is defined as the interior of $U^{c} \cup V$. We denote that Heyting algebra of open sets by ${\mathcal {O}}(X)$.

Let $(P,\le )$ be a poset. We denote by $P^{+}$ the set of all upsets of $(P,\le )$ as well as the poset we obtain by ordering $P^{+}$ by the inclusion relation. The set $P^{+}$ is closed under intersections and unions of arbitrary families and contains P and $\emptyset$. Therefore, we have a complete distributive lattice. We can define the binary operation $\Rightarrow$ on $P^{+}$ by setting for every $U, V \in P^{+}$,

$$\begin{aligned} U\Rightarrow V =(U\cap V^{c}]^{c}. \end{aligned}$$

(1)

Together with $\Rightarrow$ and $\emptyset$, the complete distributive lattice $P^{+}$ is a Heyting algebra. In fact, we can look at $P^{+}$ as a topology on P. In this topology, $U \Rightarrow V$ is precisely the interior of $U^{c} \cup V$.

Hilbert algebras were introduced in the early 1950s by Henkin for some investigations of the implication of intuitionistic and other non-classical logics (Rasiowa 1974, pp. 16). In the 1960s, they were studied especially by Horn (1962) and Diego (1965).

Definition 1

A Hilbert algebra is an algebra $H = (H,\rightarrow ,1)$ of type (2, 0) that satisfies the following conditions for every $a,b,c\in H$:

• (1) $a\rightarrow (b\rightarrow a) = 1$,

• (2) $(a\rightarrow (b\rightarrow c)) \rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)) = 1$,

• (3) if $a\rightarrow b = b\rightarrow a = 1$, then $a = b$.

In every Hilbert algebra H, the relation $\le$ defined by setting for every $a, b \in H$

$$\begin{aligned} a\le b \quad \Longleftrightarrow \quad a\rightarrow b = 1 \end{aligned}$$

is a partial order, which is called the natural order of H, and with 1 as its greatest (or top) element.

In Diego (1965), it was proved that the class of Hilbert algebras is a variety. We write $\mathsf {Hil}$ for the variety of Hilbert algebras as well as for the category whose objects are Hilbert algebras and whose morphisms are the homomorphisms between them. Several properties of Hilbert algebras can be found in Buşneag and Ghiţǎ (2010), Diego (1965).

A semilattice is an algebra $(A, \wedge )$ of type (2) where $\wedge$ is associative, commutative and idempotent. Given a semilattice $(A, \wedge )$, the binary relation $\le$ defined by

$$\begin{aligned} a \le b \quad \Longleftrightarrow \quad a \wedge b = a, \end{aligned}$$

for every $a,b \in A$, is a partial order where any two elements $a,b \in A$ have a greatest lower bound $a\wedge b$ (i.e., an infimum or meet). We say that a semilattice $(A, \wedge )$ is a meet-semilattice when we consider the partial order just defined. Every poset $(P,\le )$ with the property that any two elements $a,b \in P$ have a greatest lower bound defines a meet-semilattice by taking on P the operation $\wedge$ defined by setting for every $a, b \in P$ that $a \wedge b$ is the greatest lower bound of a, b. The partial order of the meet-semilattice $(P,\wedge )$ is the partial order $\le$ we start with. A meet-semilattice $(A, \wedge )$ is (upper) bounded if $\le$ has a greatest element, that we denote by 1. In this case, we extend the signature and consider the algebra $(A, \wedge , 1)$. Throughout this paper, we just write semilattice in place of meet-semilattice.

Implicative semilattices were introduced in Nemitz (1965). They are also known as Brouwerian semilattices. For studies of implicative semilattices, we refer to Köhler (1981), Nemitz and Whaley (1971), Nemitz and Whaley (1973). Implicative semilattices are the algebraic counterpart of the $\{\wedge , \rightarrow , 1\}$-fragment of intuitionistic logic. They are a combination of a Hilbert algebra and a semilattice where $a \rightarrow b$ is the meet-residual of b by a.

Definition 2

An implicative semilattice is an algebra $(H, \wedge , \rightarrow )$ of type (2, 2) such that $(H,\wedge )$ is a semilattice and for every $a,b,c\in H$,

$$\begin{aligned} a\wedge b \le c \quad \Longleftrightarrow \quad a\le b\rightarrow c, \end{aligned}$$

where $\le$ is the semilattice order of $(H, \wedge )$.

Every implicative semilattice has a greatest element, denoted by 1. In this paper, we take the signature for implicative semilattices to be $\{\wedge , \rightarrow , 1\}$, so that $(H, \wedge , \rightarrow , 1)$ is an implicative semilattice if $(H, \wedge , \rightarrow )$ is one and 1 is its greatest element in the natural order. The class of implicative semilattices is a variety, as it was proved by Monteiro (1955). We denote the category of implicative semilattices (i.e., of the implicative semilattices with their algebraic homomorphisms) by ${{\mathsf {I}}}{{\mathsf {S}}}$. Notice that if $(H,\wedge ,\rightarrow ,1) \in {{\mathsf {I}}}{{\mathsf {S}}}$, then $(H,\rightarrow ,1)\in \mathsf {Hil}$. For more details about implicative semilattices, see Curry (1963), Nemitz (1965).

It is known that implicative semilattices are the $\{\wedge , \rightarrow , 1\}$-subreducts of Heyting algebras and Hilbert algebras are the $\{\rightarrow , 1\}$-subreducts of implicative semilattices. Therefore, an arbitrary quasi-equation in the language $\{\rightarrow , 1\}$ holds in every Heyting algebra if and only if it holds in every implicative semilattice, and this happens if and only if it holds in every Hilbert algebra. In particular, the equations

• (1) $(x\wedge y)\rightarrow z \approx x \rightarrow (y\rightarrow z)$

• (2) $x\rightarrow (y\wedge z) \approx (x\rightarrow y)\wedge (x\rightarrow z)$

hold in every implicative semilattice. We highlight here the properties of Hilbert algebras most relevant to the paper.

Lemma 3

Let $H\in \mathsf {Hil}$ and $a,b,c\in H$. The following conditions are satisfied:

• (a) $a\rightarrow a = 1$,

• (b) $1\rightarrow a = a$,

• (c) $a\rightarrow (b\rightarrow c) = b\rightarrow (a \rightarrow c)$,

• (d) $a\rightarrow (b\rightarrow c) = (a\rightarrow b)\rightarrow (a\rightarrow c)$,

• (e) if $a\le b$, then $c\rightarrow a \le c\rightarrow b$ and $b\rightarrow c \le a\rightarrow c$.

Esakia considered in Esakia (2006) the modalized Heyting calculus mHC, which consists of an expansion of the Heyting propositional calculus for intuitionistic logic by a very special modal operator. The algebraic models of this calculus are the Heyting algebras augmented with a frontal operator. Let $(H,\wedge ,\vee ,\rightarrow ,0,1)$ be a Heyting algebra. A map $\tau :H\rightarrow H$ is said to be a frontal operator if the following conditions are satisfied for every $a,b \in H$:

(f1) :

$\tau (a\wedge b) = \tau (a) \wedge \tau (b)$,

(f2) :

$a\le \tau (a)$,

(f3) :

$\tau (a)\le b \vee (b\rightarrow a)$.

One of the main motivations to study frontal operators in Heyting algebras stemmed from some topological semantics where $\tau$ is interpreted as the co-derivative operator. In what follows, we will explain this point.

Let X be a topological space. The derivative operator $\delta$ of X is the map that sends every $A\subseteq X$ to its set of accumulation points. Its dual is the co-derivative operator $\tau$ defined by setting for every $A \subseteq X$, $\tau (A) := \delta (A^{c})^{c}$. In Esakia (2006), the elements of $\tau (A)$ are called the frontal points of A, that is, $x \in X$ is a frontal point of A if and only if there is a neighborhood U of x such that $U\subseteq A \cup \{x\}$. When $\tau$ is applied to an open set, it provides an open set. Esakia (2006) also showed that if X is a topological space, then the co-derivative operator restricted to ${\mathcal {O}}(X)$ is a frontal operator of the Heyting algebra ${\mathcal {O}}(X)$.

We present now an interesting characterization of the co-derivative operator of the Heyting algebra of the open sets of a topological space. Recall that a point x of a topological space X is an isolated point of a set $A \subseteq X$ if there exists a neighborhood $U_x$ of x such that $U_x \cap A = \{x\}$. We denote the set of isolated points of A by $A_a$.

Proposition 4

Let X be a topological space and $\tau$ its co-derivative operator. Then, for every $U\in {\mathcal {O}}(X)$, $\tau (U) = U \cup (U^c)_a$, that is, for every point $x \in X$, x is a frontal point of U if and only if $x \in U$ or x is an isolated point of $U^{c}$.

Proof

Let $x\in \tau (U)$. Suppose that $x\notin U$. We will see that $x \in (U^c)_a$. Since $x\in \tau (U)$, there exists a neighborhood $V_x$ of x such that $V_x\subseteq U\cup \{x\}$. Thus, $V_x \cap U^c =\{x\}$. Hence, $x \in (U^c)_a$. Conversely, let $x\in U\cup (U^c)_a$. If $x \in U$, since U is open, x is a frontal point of U. If $x \in (U^{c})_a$, there exists a neighborhood $V_x$ of x such that $V_{x}\cap U^c=\{x\}$. Hence, $V_{x} = V_{x}\cap (U\cup U^c) =(V_{x}\cap U)\cup \{x\}\subseteq U\cup \{x\}.$ Therefore, x is a frontal point of U. $\square$

We can apply the proposition to the Heyting algebra of the upsets of a poset. Let $(P,\le )$ be a poset and $U\subseteq P$. We write $U_M$ for the set of maximal elements of U (note that this set may be empty).

Corollary 5

Let $(P,\le )$ be a poset and consider the topological space $P^+$ of the upsets of P. Then, $(U^c)_a = (U^c)_M$ for every $U\in P^+$. Hence, the co-derivative frontal operator $\tau$ satisfies that $\tau (U) = U \cup (U^c)_M$ for every $U \in P^{+}$.

Proof

Straightforward computations show that if $x\in P$, then $U_x$ is a neighborhood of x in the topology of the upsets of P if and only if $[x) \subseteq U_x$. Using this fact, we prove that $(U^c)_a = (U^c)_M$ whenever $U\in P^+$. In order to do it, let $U\in P^+$. Suppose that $x\in (U^c)_a$. Thus, there exists a neighborhood $U_x$ of x such that $U_{x} \cap U^c = \{x\}$. Let $x\le y$ with $y\in U^c$. Then, $y\in [x) \cap U^{c} \subseteq U_x \cap U^c = \{x\}$, i.e., $y = x$. Therefore, $x\in (U^c)_M$. Conversely, let $x\in (U^c)_M$. Thus, $[x) \cap U^c = \{x\}$, which implies that $x\in (U^c)_a$. Hence, $(U^c)_a = (U^c)_M$. Finally, it follows from Proposition 4 that $\tau (U) = U \cup (U^{c})_M$ for every $U \in P^{+}$. $\square$

The following definition was introduced in Castiglioni and San Martín (2015) and generalizes to the Hilbert algebras setting the definition of frontal operator given for Heyting algebras.

Definition 6

Let $H\in \mathsf {Hil}$. We say that a map $\tau :H \rightarrow H$ is a frontal operator if it satisfies the following conditions for every $a,b \in H$:

(i1) :

$\tau (a\rightarrow b) \le \tau (a) \rightarrow \tau (b)$,

(i2) :

$a\le \tau (a)$,

(i3) :

$\tau (a) \le ((b\rightarrow a)\rightarrow b)\rightarrow b$.

An algebra $(H,\tau )$ is a frontal Hilbert algebra if H is a Hilbert algebra and $\tau$ a frontal operator on it.

We denote by $\mathsf {FHil}$ the algebraic category of frontal Hilbert algebras (i.e., the morphisms are the algebra homomorphisms). In every Hilbert algebra, there exists at least one frontal operator since the identity map meets the required conditions.

It turns out that a unary map $\tau$ on a Heyting algebra is a frontal operator if and only if it satisfies the conditions $\mathbf{(i1) }$, $\mathbf{(i2) }$, and $\mathbf{(i3) }$. This explains why frontal Hilbert algebras are a generalization of frontal Heyting algebras.²

Let A be an algebra. An n-ary function $f: A^{n} \rightarrow A$ is said to be compatible with a congruence$\theta$ of A if $(a_{i}, b_{i}) \in \theta$ with $i= 1,...,n$ implies $(f(a_{1},...,a_{n}), f(b_{1},...,b_{n}))\in \theta$. And it is said to be a compatible function of A provided it is compatible with all the congruences of A. The simplest examples of compatible functions in an algebra A are the polynomial functions.³ Frontal operators on Heyting algebras and frontal operators on Hilbert algebras are necessarily compatible functions, as it was proved in Castiglioni and San Martín (2015).

Definition 7

An algebra $(H,\tau )$ is a frontal implicative semilattice if H is an implicative semilattice and $\tau$ is a frontal operator of its Hilbert algebra reduct.

We denote by $\mathsf {FIS}$ the algebraic category of frontal implicative semilattices. The following result holds as in the case of Heyting algebras, and its proof is part of the folklore of the subject.

Lemma 8

Let $H\in {{\mathsf {I}}}{{\mathsf {S}}}$ and $\tau$ a unary operator on H. Then, $\tau$ is a frontal operator if and only if $\tau$ satisfies ${\mathbf {(i2)}}$, ${\mathbf {(i3)}}$ and $\tau (a\wedge b) = \tau (a) \wedge \tau (b)$ for every $a, b \in H$.

2.1 An adjunction between $\mathsf {Hil}$ and ${{\mathsf {I}}}{{\mathsf {S}}}$

The forgetful functor from the category of implicative semilattices to the category of Hilbert algebras that forgets the meet operation has a left adjoint. This amounts to the existence of the free implicative semilattice extension of any Hilbert algebra. There are several ways to obtain such a left adjoint. Explicit descriptions of such an adjoint functor and of the free extension of a Hilbert algebra to an implicative semilattice are obtained in Celani and Jansana (2012) and Castiglioni and San Martín (2018).

For completeness of the exposition, we provide now a description of a left adjoint functor to the forgetful functor from ${{\mathsf {I}}}{{\mathsf {S}}}$ to $\mathsf {Hil}$, which will be used later to obtain our results. We give complete proofs using only the minimum tools needed to obtain the results, thus avoiding more general approaches such that those in Celani and Jansana (2012), Castiglioni and San Martín (2018).

We start with some preliminary definitions and results.

It is immediate that if $(P, \le )$ is a poset and $U, V \in P^{+}$, then the following condition is satisfied for every $x \in P$:

$$\begin{aligned} x \in U \Rightarrow V \, \Longleftrightarrow \, (\forall y \in P)(x \le y \text { and } y \in U \Longrightarrow y \in V). \end{aligned}$$

In the general study of Hilbert algebras, the notion of implicative filter plays an important role. Let $H\in \mathsf {Hil}$. A set $F\subseteq H$ is said to be an implicative filter if $1\in F$ and for all $a, b \in H$ we have $b\in F$ whenever $a\in F$ and $a\rightarrow b \in F$. If F is a proper subset of H, then we say that the implicative filter F is proper. It is immediate that every implicative filter of a Hilbert algebra is an upset w.r.t. the natural order. We denote by $\mathsf {Fil}(H)$ the set of all implicative filters of H.

Note that the set of all implicative filters of H is closed under intersections of arbitrary families; therefore, it is a complete lattice under the inclusion order. Thus, we can speak of the implicative filter generated by a set. Let $H\in \mathsf {Hil}$ and $X \subseteq H$. We denote the implicative filter generated by X, i.e., the least filter of H that contains the set X, by F(X). There is a useful explicit description for F(X) (see Buşneag 1985, Lemma 2.3):

$$\begin{aligned} F(X) =&\ \{b \in H: b = 1 \text { or } a_1\rightarrow (a_2\rightarrow \cdots (a_n \rightarrow b) \ldots )=1\\&\ \text {for some}\; a_{1}, \ldots ,a_n\in X\}. \end{aligned}$$

The lattice $\mathsf {Fil}(H)$ is known to be distributive (Diego 1965).

The next fact on implicative filters (Celani 2002, Theorem 3.2) will be used several times along the paper. Let $f:H_1\rightarrow H_2$ be a function between Hilbert algebras. Then, the following two conditions are equivalent:

• (1) $f(1) = 1$ and $f(a\rightarrow b) \le f(a)\rightarrow f(b)$ for every $a,b \in H_1$.

• (2) $f^{-1}[F]$ is an implicative filter of $H_1$ whenever F is an implicative filter of $H_2$.

In particular, (2) holds when f is a homomorphism.

An implicative filter F of a Hilbert algebra H is irreducible if it is an irreducible element of the lattice of the implicative filters of H, i.e., if F is proper and for any implicative filters $F_1, F_2$ of H such that $F = F_1 \cap F_2$ we have $F = F_1$ or $F = F_2$. We denote by ${\mathrm {Irr}}(H)$ the set of irreducible implicative filters of H, as well as the poset we obtain when we order it by the inclusion relation.

For a proof of the following lemma, see Diego (1965).

Lemma 9

Let $H\in \mathsf {Hil}$ and $F\in \mathsf {Fil}(H)$. Then, $F\in {\mathrm {Irr}}(H)$ if and only if F is proper and for every $a,b\notin F$ there exists $c\notin F$ such that $a\le c$ and $b\le c$.

Let $H\in \mathsf {Hil}$. A set $I \subseteq H$ is an order-ideal if I is an order-ideal of $(H, \le )$. We denote by ${{\mathsf {I}}}{{\mathsf {d}}}(H)$ the set of order-ideals of H. The following lemma is Celani (2002, Theorem 2.6).

Lemma 10

Let $H\in \mathsf {Hil}$. Let $F\in \mathsf {Fil}(H)$ and $I \in {{\mathsf {I}}}{{\mathsf {d}}}(H)$ be such that $F\cap I = \emptyset$. Then, there exists $P\in {\mathrm {Irr}}(H)$ such that $F\subseteq P$ and $P\cap I = \emptyset$.

The following known results follow from Lemma 10.

Corollary 11

Let $H\in \mathsf {Hil}$.

• 1. If $F \in \mathsf {Fil}(H)$ and $a \notin F$, then there exists $P\in {\mathrm {Irr}}(H)$ such that $F\subseteq P$ and $a\notin P$.

• 2. If $a,b\in H$ are such that $a\nleq b$, then there exists $P\in {\mathrm {Irr}}(H)$ such that $a\in P$ and $b\notin P$.

• 3. If $F\in \mathsf {Fil}(H)$ and $a,b\in H$, then $a\rightarrow b \notin F$ if and only if there exists $P\in {\mathrm {Irr}}(H)$ such that $F\subseteq P$, $a\in P$ and $b\notin P$.

The next lemma was proved in Castiglioni and San Martín (2015, Section 3, Lemma 16). We give the proof here for the sake of completeness.

Lemma 12

Let $(H,\tau )$ be a frontal Hilbert algebra and $P \in {\mathrm {Irr}}(H)$. For every $a, b \in H$, if $\tau (a) \in P$ and $b \not \in P$, then $b \rightarrow a \in P$.

Proof

Let $P\in {\mathrm {Irr}}(H)$, $\tau (a)\in P$, and $b\notin P$. Suppose that $b \rightarrow a \not \in P$. Then, by Lemma 9 there exists $c\notin P$ such that $b\le c$ and $b\rightarrow a \le c$. Thus, $b \rightarrow c = 1$ and $(b\rightarrow a) \rightarrow c = 1$. Since $(b\rightarrow c)\rightarrow ((b\rightarrow a) \rightarrow c)\rightarrow ((c\rightarrow a)\rightarrow c)) = 1$, we have $(c\rightarrow a)\rightarrow c = 1$. From the fact that $\tau$ is a frontal operator, we have $\tau (a)\le ((c\rightarrow a)\rightarrow c)\rightarrow c$, i.e., $\tau (a)\le c$. Taking into account that $\tau (a)\in P$, we conclude that $c\in P$, which is a contradiction. $\square$

Let $H\in \mathsf {Hil}$. We consider the poset ${\mathrm {Irr}}(H) = ({\mathrm {Irr}}(H), \subseteq )$ and the complete lattice of its upsets ${\mathrm {Irr}}(H)^{+}$. We define the map $\varphi _H: H \rightarrow {\mathrm {Irr}}(H)^{+}$ by setting for every $a\in H$

$$\begin{aligned} \varphi _H(a): = \{P\in {\mathrm {Irr}}(H): a\in P\}. \end{aligned}$$

(2)

This map is well defined since $\varphi _H(a)$ is an upset of ${\mathrm {Irr}}(H)$. When the algebra H is clear from the context, we will use $\varphi$ instead of $\varphi _H$. Corollary 11 implies that $\varphi$ is a one-to-one map. Hence, $\varphi$ is an order embedding from the poset $(H,\le )$, where $\le$ is the natural order of H, into the complete lattice $({\mathrm {Irr}}(H)^{+}, \subseteq )$; therefore, $(({\mathrm {Irr}}(H)^{+}, \subseteq ), \varphi )$ is a completion of $(H,\le )$.

The operation $\Rightarrow$ on ${\mathrm {Irr}}(H)^{+}$, defined by condition (1) in Sect. 2, is such that for every $a, b \in H$

$$\begin{aligned} \varphi (a) \Rightarrow \varphi (b) = \varphi (a \rightarrow b). \end{aligned}$$

Indeed, if $P \in \varphi (a \rightarrow b)$, $P \subseteq Q \in {\mathrm {Irr}}(H)$ and $a \in Q$, then, since Q is an implicative filter, we have $b \in Q$. It follows that $\varphi (a \rightarrow b) \subseteq \varphi (a) \Rightarrow \varphi (b)$. Conversely, if $P \not \in \varphi (a \rightarrow b)$, using Corollary 11 there is $Q \in {\mathrm {Irr}}(H)$ such that $P \subseteq Q$, $a \in Q$, and $b \not \in Q$. It follows then that $P \not \in \varphi (a) \Rightarrow \varphi (b)$. Hence, we obtain the other inclusion. Moreover $\varphi (1) = {\mathrm {Irr}}(H)$ and therefore the map $\varphi$ is an embedding from H into the Hilbert algebra $(\varphi [H], \Rightarrow , {\mathrm {Irr}}(H))$, which is a subalgebra of the $\{\rightarrow , 1\}$-reduct of the Heyting algebra of the upsets of ${\mathrm {Irr}}(H)$.

Remark 13

The completion $(({\mathrm {Irr}}(H)^{+}, \subseteq ), \varphi _H)$ of the poset $(H, \le )$ is a $\Delta _1$-completion in the sense of Gehrke et al. (2013). In González (2019), it is proved that it is indeed the $(\mathsf {Fil}(H), {{\mathsf {I}}}{{\mathsf {d}}}(H))$-completion of $(H, \le )$ and that the operation $\Rightarrow$ is the $\pi$-extension of the operation $\rightarrow$ of H to ${\mathrm {Irr}}(H)^{+}$.

Using that ${\mathrm {Irr}}(H)^{+}$ is a Heyting algebra and the fact that $\varphi$ is an embedding from H to $(\varphi [H], \Rightarrow , {\mathrm {Irr}}(H))$, it is easy to see that for every $a_1, \ldots , a_n, b \in H$,

$$\begin{aligned} \varphi (a_1) \cap \cdots \cap \varphi (a_n) \Rightarrow \varphi (b) = \varphi (a_1 \rightarrow (\ldots (a_n \rightarrow b)\ldots )). \end{aligned}$$

Let $H\in \mathsf {Hil}$. We consider the bounded semilattice $({\mathrm {Irr}}(H)^{+}, \cap , {\mathrm {Irr}}(H))$ and the subalgebra generated by $\varphi [H]$, which is, of course, a bounded semilattice. We denote it, as well as its domain, by $\langle \varphi [H]\rangle$. Since ${\mathrm {Irr}}(H) = \varphi (1) \in \varphi [H]$, the elements of $\langle \varphi [H]\rangle$ are the sets of the form

$$\begin{aligned} U = \varphi (a_1) \cap \cdots \cap \varphi (a_n) \end{aligned}$$

for some $a_1, \ldots , a_n \in H$.

Proposition 14

For every Hilbert algebra H, the set $\langle \varphi [H]\rangle$ is closed under the operation $\Rightarrow$ of ${\mathrm {Irr}}(H)^{+}$.

Proof

Let $U, V \in \langle \varphi [H]\rangle$. Assume that $U = \varphi (a_1) \cap \cdots \cap \varphi (a_n)$ and $V = \varphi (b_1) \cap \cdots \cap \varphi (b_m)$, where $a_1, \ldots , a_n, b_1, \ldots , b_m \in H$. Then,

$$\begin{aligned} U \Rightarrow V = \varphi (a_1) \cap \cdots \cap \varphi (a_n) \Rightarrow \varphi (b_1) \cap \cdots \cap \varphi (b_m). \end{aligned}$$

Using that ${\mathrm {Irr}}(H)^{+}$ is a Heyting algebra, we have

$$\begin{aligned} U \Rightarrow V = \bigcap _{1 \le i \le m} \varphi (a_1) \cap \cdots \cap \varphi (a_n) \Rightarrow \varphi (b_i). \end{aligned}$$

Now, for every $1 \le i \le m$ we have

$$\begin{aligned} \varphi (a_1) \cap \cdots \cap \varphi (a_n) \Rightarrow \varphi (b_i) = \varphi (a_1 \rightarrow (\ldots (a_n \rightarrow b_i)\ldots )). \end{aligned}$$

It follows that $U \Rightarrow V \in \langle \varphi [H]\rangle$. $\square$

The proposition implies that the algebra

$$\begin{aligned} \mathrm {L}(H) := (\langle \varphi [H]\rangle , \cap , \Rightarrow , {\mathrm {Irr}}(H)) \end{aligned}$$

is an implicative semilattice.

Lemma 15

Let $h: H_1 \rightarrow H_2$ be a homomorphism of Hilbert algebras. If $a_1, \ldots , a_n,$$b_1, \ldots , b_m \in H$ are such that

$$\begin{aligned} \varphi _{H_1}(a_1) \cap \cdots \cap \varphi _{H_1}(a_n) \subseteq \varphi _{H_1}(b_1) \cap \cdots \cap \varphi _{H_1}(b_m), \end{aligned}$$

then

$$\begin{aligned} \varphi _{H_2}(h(a_1)) \cap \cdots \cap \varphi _{H_2}(h(a_n)) \subseteq \varphi _{H_2}(h(b_1)) \cap \cdots \cap \varphi _{H_2}(h(b_m)). \end{aligned}$$

Proof

Let $a_1, \ldots , a_n, b_1, \ldots , b_m \in H$ with $\varphi _{H_1}(a_1) \cap \cdots \cap \varphi _{H_1}(a_n) \subseteq \varphi _{H_1}(b_1) \cap \cdots \cap \varphi _{H_1}(b_m)$. Suppose that $P \in \varphi _{H_2}(h(a_1)) \cap \cdots \cap \varphi _{H_2}(h(a_n))$. Then, $a_1, \ldots , a_n \in h^{-1}[P]$. Suppose that there is $b_i$ with $1 \le i \le m$ such that $h(b_i) \not \in P$. Then, $b_i \not \in h^{-1}[P]$. Thus, there exists $Q \in {\mathrm {Irr}}(H)$ such that $b_i \not \in Q$ and $h^{-1}[P] \subseteq Q$. It follows that $Q \in \varphi _{H_1}(a_1) \cap \cdots \cap \varphi _{H_1}(a_n)$, and the assumption implies that $b_i \in Q$, which is a contradiction. Therefore, $P \in \varphi _{H_2}(h(b_1)) \cap \cdots \cap \varphi _{H_2}(h(b_m))$. This concludes the proof. $\square$

Proposition 16

Let $h: H_1 \rightarrow H_2$ be a homomorphism of Hilbert algebras. Then, there exists a unique homomorphism ${\hat{h}}: \mathrm {L}(H_1) \rightarrow \mathrm {L}(H_2)$ such that $\varphi _{H_2} \circ h = {\hat{h}} \circ \varphi _{H_1}$, i.e., that makes the following diagram to commute:

Proof

First we show that if such a homomorphism exists, it is unique. Suppose that $f: \mathrm {L}(H_1) \rightarrow \mathrm {L}(H_2)$ is a homomorphism such that $\varphi _{H_2} \circ h = f \circ \varphi _{H_1}$. Let $U = \varphi _{H_1}(a_1) \cap \cdots \cap \varphi _{H_1}(a_n) \in \langle \varphi _{H_1}[H_1]\rangle$ with $a_1, \ldots , a_n \in H_1$. Then, $f(U) = f(\varphi _{H_1}(a_1)) \cap \cdots \cap f(\varphi _{H_1}(a_n)) = \varphi _{H_2}(h(a_1)) \cap \cdots \cap \varphi _{H_2}(h(a_n))$. This implies that if $f_1, f_2: \mathrm {L}(H_1) \rightarrow \mathrm {L}(H_2)$ are homomorphism such that $\varphi _{H_2} \circ h = f_1 \circ \varphi _{H_1}$ and $\varphi _{H_2} \circ h = f_2 \circ \varphi _{H_1}$, then for every $U \in \langle \varphi _{H_1}[H_1]\rangle$, $f_1(U) = f_2(U)$.

Now we prove the existence. We define ${\hat{h}} : \mathrm {L}(H_1) \rightarrow \mathrm {L}(H_2)$ by setting for every $U \in \langle \varphi _{H_1}[H_1]\rangle$:

$$\begin{aligned} {\hat{h}}(U) = \varphi _{H_2}(h(a_1)) \cap \cdots \cap \varphi _{H_2}(h(a_n)), \end{aligned}$$

where $a_1 \ldots , a_n \in H_1$ are such that $U = \varphi _{H_1}(a_1) \cap \cdots \cap \varphi _{H_1}(a_n)$. Lemma 15 implies that the map ${\hat{h}}$ is well defined. Note that in particular ${\hat{h}}(\varphi _{H_1}(a)) = \varphi _{H_2}(h(a))$. It is immediate to see that $\varphi _{H_2} \circ h = {\hat{h}} \circ \varphi _{H_1}$, that for all $U, V \in {\mathrm {Irr}}(H)$ it holds that ${\hat{h}}(U \cap V) = {\hat{h}}(U) \cap {\hat{h}}(V)$, and that ${\hat{h}}({\mathrm {Irr}}(H_1)) = {\mathrm {Irr}}(H_2)$. It remains to show that ${\hat{h}}(U \Rightarrow V) = {\hat{h}}(U) \Rightarrow {\hat{h}}(V)$ for all $U, V \in {\mathrm {Irr}}(H)$. Suppose that $U = \varphi _{H_1}(a_1) \cap \cdots \cap \varphi _{H_1}(a_n)$ and $V = \varphi _{H_1}(b_1) \cap \cdots \cap \varphi _{H_1}(b_m)$. Reasoning as in the proof of Proposition 14 we have

$$\begin{aligned} U \Rightarrow V = \bigcap _{1 \le i \le m} \varphi _{H_1}(a_1 \rightarrow (\ldots (a_n \rightarrow b_i)\ldots )). \end{aligned}$$

Hence, ${\hat{h}}(U \Rightarrow V) = \bigcap _{1 \le i \le m}\varphi _{H_2}(h(a_1 \rightarrow (\ldots (a_n \rightarrow b_i)\ldots )))$. It easily follows that

$$\begin{aligned} {\hat{h}}(U \Rightarrow V) = \bigcap _{1 \le i \le m} \varphi _{H_2}(h(a_1)) \cap \cdots \cap \varphi _{H_2}(h(a_n)) \Rightarrow \varphi _{H_2}(h(b_i)). \end{aligned}$$

The last expression is equal to ${\hat{h}}(U) \Rightarrow {\hat{h}}(V)$. We conclude that ${\hat{h}}$ is the desired homomorphism. $\square$

Using the results above, the next proposition easily follows.

Proposition 17

The assignments $H\mapsto \mathrm {L}(H)$ and $h\mapsto {\hat{h}}$ define a functor $(\ )^{{{\mathsf {I}}}{{\mathsf {S}}}}:\mathsf {Hil}\rightarrow {{\mathsf {I}}}{{\mathsf {S}}}$.

Recall that if $H\in {{\mathsf {I}}}{{\mathsf {S}}}$, a subset $F\subseteq H$ is said to be a filter if it is an upset, $1 \in F$, and $a\wedge b \in F$ whenever $a,b \in F$. It is part of the folklore that if $H\in {{\mathsf {I}}}{{\mathsf {S}}}$, then the set of implicative filters of H is equal to the set of filters of H.

Let ${\mathrm {U}}$ be the forgetful functor from ${{\mathsf {I}}}{{\mathsf {S}}}$ to $\mathsf {Hil}$; namely, ${\mathrm {U}}$ sends every implicative semilattice to its Hilbert algebra reduct and the homomorphisms accordingly.

Proposition 18

Let H be a Hilbert algebra and let A be an implicative semilattice. Consider the $\{\rightarrow , 1\}$-reduct ${\mathrm {U}}(A)$ of A and a homomorphism $h: H \rightarrow {\mathrm {U}}(A)$. Then, there exists a unique homomorphism ${\overline{h}}:\mathrm {L}(H) \rightarrow A$ such that $h = {\overline{h}} \circ \varphi _H$.

Proof

Straightforward computations show that the map $\varphi _{{\mathrm {U}}(A)}: {\mathrm {U}}(A) \rightarrow \mathrm {L}({\mathrm {U}}(A))$, that we abbreviate in this proof as $\varphi _A$, is in fact an isomorphism between A and $\mathrm {L}({\mathrm {U}}(A))$, because $\varphi _{A}(a) \cap \varphi _{A}(b) = \varphi _{A}(a \wedge b)$ for every $a, b \in A$. By Proposition 16, we have that there exists a unique homomorphism ${\hat{h}}: \mathrm {L}(H) \rightarrow \mathrm {L}(U(A))$ such that ${\hat{h}}\circ \varphi _H = \varphi _{A} \circ h$. Let ${\overline{h}}: \mathrm {L}(H) \rightarrow A$ be the map $\varphi _{A} ^{-1} \circ {\hat{h}}$. Then, it follows that $h = {\overline{h}} \circ \varphi _H$. This proves the existence. To prove uniqueness, suppose that $f_1, f_2: \mathrm {L}(H) \rightarrow A$ are such that $h = f_1 \circ \varphi _H$ and $h = f_2 \circ \varphi _H$. Then, $\varphi _A \circ h = (\varphi _A \circ f_1) \circ \varphi _H$ and $\varphi _A \circ h = (\varphi _A \circ f_2) \circ \varphi _H$. Therefore, Proposition 16 also implies that $\varphi _A \circ f_1 = \varphi _A \circ f_2$. Since $\varphi _A$ is one-to-one, it follows that $f_ 1= f_2$. $\square$

Let ${\mathrm {I}}_{\mathsf {Hil}}$ be the identity functor in $\mathsf {Hil}$. From Proposition 16, it follows that the morphisms $\varphi _H: H \rightarrow \mathrm {L}(H)$ establish a natural transformation from ${\mathrm {I}}_{\mathsf {Hil}}$ to the functor ${\mathrm {U}}\circ (\ )^{{{\mathsf {I}}}{{\mathsf {S}}}}$. Then, using Proposition 18 we obtain the following result.

Theorem 19

The functor $(\ )^{{{\mathsf {I}}}{{\mathsf {S}}}}: \mathsf {Hil}\rightarrow {{\mathsf {I}}}{{\mathsf {S}}}$ is left adjoint to ${\mathrm {U}}$.

An algebra $(H,\rightarrow ,0,1)$ of type (2, 0, 0) is a bounded Hilbert algebra if $(H,\rightarrow ,1)$ is a Hilbert algebra and $0\le a$ for every $a\in A$. We write $\mathsf {Hil}_0$ for the algebraic category of bounded Hilbert algebras. An algebra $(H,\wedge ,\rightarrow ,0,1)$ of type (2, 2, 0, 0) is a bounded implicative semilattice if $(H,\wedge ,\rightarrow ,1)$ is an implicative semilattice and $0\le a$ for every $a\in H$. We write ${{\mathsf {I}}}{{\mathsf {S}}}_0$ for the algebraic category of bounded implicative semilattices. Note that if H is a bounded Hilbert algebra, then $\varphi _{H}(0) = \emptyset$ and therefore the bottom element of the Heyting algebra ${\mathrm {Irr}}(H)^{+}$ belongs to the implicative semilattice $\langle \varphi _{H}[H]\rangle$ and hence it is a bounded implicative semilattice. We define the functors $(\ )^{{{\mathsf {I}}}{{\mathsf {S}}}}: \mathsf {Hil}_0 \rightarrow {{\mathsf {I}}}{{\mathsf {S}}}_0$ and ${\mathrm {U}}$ similarly to those of Theorem 19. Straightforward modifications of propositions 16 and 18 and their proofs show the following result.

Corollary 20

The functor $(\ )^{{{\mathsf {I}}}{{\mathsf {S}}}}: \mathsf {Hil}_0 \rightarrow {{\mathsf {I}}}{{\mathsf {S}}}_0$ is left adjoint to ${\mathrm {U}}$.

3 An adjunction between $\mathsf {FHil}$ and $\mathsf {FIS}$

A frontal operator in a Hilbert algebra resembles a modal operator $\Box$ in a Boolean algebra or in a distributive lattice in many respects. Let $(H,\tau )$ be a frontal Hilbert algebra. We can extend $\tau$ to the algebra ${\mathrm {Irr}}(H)^{+}$ in a similar way as in a normal modal algebra we extend $\Box$ to the powerset algebra of the ultrafilters or in a distributive lattice with a normal $\Box$ we extend it to the distributive lattice of the upsets of the poset of its prime filters. We do it in the next definition.

Definition 21

Let $(H,\tau )\in \mathsf {FHil}$. We define the map ${\tau ^{\pi }}:{\mathrm {Irr}}(H)^+ \rightarrow {\mathrm {Irr}}(H)^+$ in the following way:⁴

$$\begin{aligned} P\in {\tau ^{\pi }}(U) {\Longleftrightarrow }\;(\forall Q\in {\mathrm {Irr}}(H))( \tau ^{-1}[P]\subseteq Q {\Longrightarrow } Q\in U). \end{aligned}$$

Note that the map is well defined since from the definition it follows that ${\tau ^{\pi }}(U)$ is an upset.

The restriction of ${\tau ^{\pi }}$ to $\varphi [H]$ is in fact (modulo isomorphism) $\tau$ as shown in the next lemma.

Lemma 22

Let $(H,\tau )$ be a frontal Hilbert algebra. Then, for every $a \in H$

$$\begin{aligned} \varphi (\tau (a)) = {\tau ^{\pi }}(\varphi (a)). \end{aligned}$$

Proof

Let $P\in \varphi (\tau (a))$, i.e., $\tau (a) \in P$. Let $Q\in {\mathrm {Irr}}(H)$ such that $\tau ^{-1}[P] \subseteq Q$. Then, $a \in Q$. Thus, it follows that $\varphi (\tau (a)) \subseteq {\tau ^{\pi }}(\varphi (a))$. To prove the other inclusion, let $P \in {\tau ^{\pi }}(\varphi (a))$ and assume that $\tau (a) \not \in P$. Thus, $a \not \in \tau ^{-1}[P]$. Since it holds that $\tau (1) = 1$ and $\tau (a\rightarrow b)\le \tau (a) \rightarrow \tau (b)$ for every $a,b\in H$, it follows that $\tau ^{-1}[P]$ is an implicative filter. Therefore, there is $Q \in {\mathrm {Irr}}(H)$ such that $\tau ^{-1}[P] \subseteq Q$ and $a \not \in Q$, which is a contradiction with the fact that $P \in {\tau ^{\pi }}(\varphi (a))$. $\square$

In the sequel, we prove that if $(H,\tau )\in \mathsf {FHil}$, then $({\mathrm {Irr}}(H)^+,{\tau ^{\pi }})$ is a frontal Heyting algebra. (In particular, the appropriate reducts are a frontal implicative semilattice and a frontal Hilbert algebra).

Proposition 23

For every frontal Hilbert algebra $(H,\tau )$, the algebra $({\mathrm {Irr}}(H)^+,{\tau ^{\pi }})$ is a frontal Heyting algebra and $\varphi$ is an embedding of frontal Hilbert algebras from $(H,\tau )$ to $({\mathrm {Irr}}(H)^+,{\tau ^{\pi }})$.

Proof

First of all note that for every $P \in {\mathrm {Irr}}(H)^+$, $P\subseteq \tau ^{-1}[P]$. This holds because $a\le \tau (a)$ for every $a\in H$.

Let $U\in {\mathrm {Irr}}(H)^+$. We show that $U\subseteq {\tau ^{\pi }}(U)$. To this end, let $P\notin {\tau ^{\pi }}(U)$. Thus, there exists $Q\in {\mathrm {Irr}}(H)$ such that $\tau ^{-1}[P]\subseteq Q$ and $Q\notin U$. Since $P\subseteq \tau ^{-1}[P]$, $P\subseteq Q$. But $Q\notin U$, therefore $P\notin U$.

Straightforward computations based on the definition of ${\tau ^{\pi }}$ show that for all $U,V\in {\mathrm {Irr}}(H)^+$, ${\tau ^{\pi }}(U\cap V) = {\tau ^{\pi }}(U) \cap {\tau ^{\pi }}(V)$.

Finally, we see that ${\tau ^{\pi }}(U) \subseteq V \cup (V\Rightarrow U)$, for every $U,V\in {\mathrm {Irr}}(H)^+$. Suppose that there exists $P\in {\tau ^{\pi }}(U)$ such that $P\notin V \cup (V\Rightarrow U)$. Hence, $P\notin V$ and there exists $Q\in {\mathrm {Irr}}(H)$ such that $P\subseteq Q$, $Q\in V$ and $Q\notin U$. Since $P\in {\tau ^{\pi }}(U)$ and $Q\notin U$, we have $\tau ^{-1}[P]\nsubseteq Q$, which implies that there exists $a\in H$ such that $\tau (a)\in P$ and $a\notin Q$. Also notice that $Q\nsubseteq P$ because $P\notin V$, $Q\in V$ and $P\subseteq Q$. Hence, there exists $b\in H$ such that $b\in Q$ and $b\notin P$. Since $\tau (a)\in P$ and $b\notin P$, it follows from Lemma 12 that $b\rightarrow a \in P$, so $b\rightarrow a \in Q$. As $b\in Q$, it follows that $a \in Q$, which is a contradiction. We conclude that ${\tau ^{\pi }}(U) \subseteq V \cup (V\Rightarrow U)$.

Therefore, we have shown that $({\mathrm {Irr}}(H)^+,{\tau ^{\pi }})$ is a frontal Heyting algebra. $\square$

Corollary 24

The variety $\mathsf {FHil}$ of the frontal Hilbert algebras is the class of the frontal Hilbert subreducts of frontal Heyting algebras.

Proof

Let ${\mathcal {V}}$ the class of the frontal Hilbert subreducts of frontal Heyting algebras. It is immediate that ${\mathcal {V}} \subseteq \mathsf {FHil}$. Conversely, let $(H,\tau )\in \mathsf {FHil}$. It follows from Proposition 23 that $\varphi$ is an embedding of frontal Hilbert algebras from $(H,\tau )$ to $({\mathrm {Irr}}(H)^+,{\tau ^{\pi }})$. Since $({\mathrm {Irr}}(H)^+,{\tau ^{\pi }})$ is also a frontal Heyting algebra, it follows that $(H,\tau ) \in {\mathcal {V}}$. Thus, $\mathsf {FHil}\subseteq {\mathcal {V}}$. $\square$

Let $(H,\tau )\in \mathsf {FHil}$ and $U\in \mathrm {L}(H)$. Then, there exist $a_1,\ldots ,a_n\in H$ such that $U = \varphi (a_1)\cap \cdots \cap \varphi (a_n)$. Since ${\tau ^{\pi }}$ is a frontal operator on the Heyting algebra ${\mathrm {Irr}}(H)^+$, ${\tau ^{\pi }}(U) = \varphi (\tau (a_1))\cap \cdots \cap \varphi (\tau (a_n)) \in \mathrm {L}(H)$. It follows from Proposition 23 that the restriction of ${\tau ^{\pi }}$ to $\mathrm {L}(H)$ is a function ${\tau ^{\pi }}:\mathrm {L}(H) \rightarrow \mathrm {L}(H)$ which is a frontal operator on $\mathrm {L}(H)$. Taking into account Proposition 17, we obtain the following result.

Corollary 25

Let $(H,\tau )\in \mathsf {FHil}$. Then, $(\mathrm {L}(H),{\tau ^{\pi }})\in \mathsf {FIS}$.

If $h:(H_1,\tau _1)\rightarrow (H_2,\tau _2)$ is a morphism in $\mathsf {FHil}$, then $h:H_1\rightarrow H_2$ is a morphism in $\mathsf {Hil}$. Therefore, it follows from Proposition 17 that $h^{{{\mathsf {I}}}{{\mathsf {S}}}}:\mathrm {L}(H_1)\rightarrow \mathrm {L}(H_2)$ is a morphism in ${{\mathsf {I}}}{{\mathsf {S}}}$. In the sequel, we prove that $h^{{{\mathsf {I}}}{{\mathsf {S}}}}:(\mathrm {L}(H_1),{\tau _{1}^{\pi }})\rightarrow (\mathrm {L}(H_2),{\tau _{2}^{\pi }})$ is also a morphism in $\mathsf {FIS}$.

Lemma 26

Let $h:(H_1,\tau _1)\rightarrow (H_2,\tau _2)$ be a morphism in $\mathsf {FHil}$. Then, the function $h^{{{\mathsf {I}}}{{\mathsf {S}}}}:(\mathrm {L}(H_1),{\tau _{1}^{\pi }})\rightarrow (\mathrm {L}(H_2),{\tau _{2}^{\pi }})$ is a morphism in $\mathsf {FIS}$.

Proof

We only need to prove that $h^{{{\mathsf {I}}}{{\mathsf {S}}}}({\tau _{1}^{\pi }}(U)) = {\tau _{2}^{\pi }}(h^{{{\mathsf {I}}}{{\mathsf {S}}}}(U))$ for every $U\in \mathrm {L}(H_1)$. Let $U\in \mathrm {L}(H_1)$, so there exist $a_1,\ldots ,a_n\in H_1$ such that $U = \bigcap _{i=1}^{n} \varphi _{H_1}(a_i)$. Taking into account that $h^{{{\mathsf {I}}}{{\mathsf {S}}}}$ is a morphism in ${{\mathsf {I}}}{{\mathsf {S}}}$ and that $h^{{{\mathsf {I}}}{{\mathsf {S}}}}(\varphi _{H_1}(a)) = \varphi _{H_2}(h(a))$, we have

$$\begin{aligned} \begin{array} [c]{lllll} h^{{{\mathsf {I}}}{{\mathsf {S}}}}({\tau _{1}^{\pi }}(U))&{} = &{} h^{{{\mathsf {I}}}{{\mathsf {S}}}}\left( \bigcap _{i=1}^{n} \varphi _{H_1}(\tau _{1}(a_i))\right) &{} &{} \\ &{} = &{} \bigcap _{i=1}^{n} h^{{{\mathsf {I}}}{{\mathsf {S}}}}(\varphi _{H_1}(\tau _{1}(a_i))) &{} &{} \\ &{} = &{} \bigcap _{i=1}^{n} \varphi _{H_2}(h(\tau _{1}(a_i))) &{} &{} \\ &{} = &{} \bigcap _{i=1}^{n} \varphi _{H_2}(\tau _{2}(h(a_i))) &{} &{} \\ &{} = &{} {\tau _{2}^{\pi }}\left( \bigcap _{i=1}^{n} \varphi _{H_2}(h(a_i))\right) &{} &{} \\ &{} = &{} {\tau _{2}^{\pi }}\left( \bigcap _{i=1}^{n} h^{{{\mathsf {I}}}{{\mathsf {S}}}}(\varphi _{H_1}(a_i))\right) &{} &{} \\ &{} = &{} {\tau _{2}^{\pi }}\left( h^{{{\mathsf {I}}}{{\mathsf {S}}}}\left( \bigcap _{i=1}^{n} \varphi _{H_1}(a_i)\right) \right) &{} &{} \\ &{} = &{} {\tau _{2}^{\pi }}(h^{{{\mathsf {I}}}{{\mathsf {S}}}}(U)).&{} &{} \end{array} \end{aligned}$$

Therefore, $h^{{{\mathsf {I}}}{{\mathsf {S}}}}({\tau _{1}^{\pi }}(U)) = {\tau _{2}^{\pi }}(h^{{{\mathsf {I}}}{{\mathsf {S}}}}(U))$, which was our aim. $\square$

Then, we obtain the next proposition.

Proposition 27

The functor $(\ )^{{{\mathsf {I}}}{{\mathsf {S}}}}:\mathsf {Hil}\rightarrow {{\mathsf {I}}}{{\mathsf {S}}}$ can be extended to a functor $(\ )^{\mathsf {FIS}}: \mathsf {FHil}\rightarrow \mathsf {FIS}$.

The next theorem follows from Propositions 19, 27, and the fact that if $(H,\tau )\in \mathsf {FIS}$, then $\varphi :(H,\tau ) \rightarrow (\mathrm {L}(H),{\tau ^{\pi }})$ is an embedding.

Theorem 28

The functor $(\ )^{\mathsf {FIS}}: \mathsf {FHil}\rightarrow \mathsf {FIS}$ is left adjoint to the forgetful functor ${\mathrm {U}}: \mathsf {FIS}\rightarrow \mathsf {FHil}$.

Let $\mathsf {FHil}_0$ be the algebraic category of frontal bounded Hilbert algebras and $\mathsf {FIS}_0$ the algebraic category of frontal bounded implicative semilattices.

The following corollary is a consequence of Corollary 20 together with similar ideas to those used to obtain Proposition 27 and Theorem 28.

Corollary 29

The functor $(\ )^{\mathsf {FIS}}: \mathsf {FHil}\rightarrow \mathsf {FIS}$ can be extended to a functor $(\ )^{\mathsf {FIS}}: \mathsf {FHil}_0 \rightarrow \mathsf {FIS}_0$ that is left adjoint to the forgetful functor ${\mathrm {U}}: \mathsf {FIS}_0 \rightarrow \mathsf {FHil}_0$.

4 An adjunction between $\mathsf {Hil}_{\gamma }$ and $\mathsf {IS}_{\gamma }$

A set E(f) of equations in the signature of Heyting algebras augmented with the unary function symbol f is said to define an implicit operation of Heyting algebras if for any Heyting algebra H there is at most one function $f_{H}:H\rightarrow H$ that satisfies the equations. When all these $f_H$ are compatible, it is said that E(f) defines an implicit compatible operation. Implicit and compatible operations were introduced and studied by Caicedo and Cignoli (2001). In particular, one of them was called a $\gamma$-operator (Caicedo and Cignoli 2001, Example 3.1). This operator can be alternatively defined as a frontal operator that satisfies some extra conditions. More precisely, a frontal operator $\tau$ on a Heyting algebra H is a $\gamma$-operator if it satisfies :

• (1) $\lnot \tau (0) = 0$

• (2) $\tau (a) \le a \vee \tau (0)$, for every $a\in H$.

In Castiglioni et al. (2010, Proposition 2.4), it is shown that a unary map $\gamma$ on a Heyting algebra H is a $\gamma$-operator if and only if it satisfies the following conditions we find in Caicedo and Cignoli (2001, Example 3.1):

• (1) $\lnot \gamma (0) = 0$

• (2) $\gamma (0)\le a \vee \lnot a$,

• (3) $\gamma (a) = a \vee \gamma (0)$.

for every $a\in H$.

Note that the condition $\gamma (a) = a \vee \gamma (0)$ can be replaced by $\gamma (a) \le a \vee \gamma (0)$. If a $\gamma$-operator $\tau$ on H exists, it is unique since it is characterized by the condition

$$\begin{aligned} \tau (a) =\; \text {min}\;\{b: \lnot b \vee a\le b\}, \end{aligned}$$

for every $a \in H$, as it is proved in Castiglioni et al. (2010). For this reason, when a $\gamma$-operator on H exists, it is denoted by $\gamma$. The operator $\gamma$ exists in every finite Heyting algebra (see Caicedo and Cignoli 2001); however, there are Heyting algebras (necessarily infinite) where there is no $\gamma$-operator. For example, if we consider the real interval [0, 1] with the usual order, then there is no $\gamma$-operator in its associated Heyting algebra.

In Castiglioni and San Martín (2015), the notion of a $\gamma$-operator was generalized to the framework of bounded Hilbert algebras. As in Heyting algebras, if $H\in \mathsf {Hil}_0$ and $a\in H$, we define $\lnot a: = a\rightarrow 0$. Let us say that a frontal operator $\tau$ on a bounded Hilbert algebra H is a $\gamma$-operator if it satisfies for every $a,b \in H$ the following conditions:

(g4) :

$\lnot \tau (a)\le \tau (a)$.

(g5) :

$\tau (a) \le (a\rightarrow b) \rightarrow ((\lnot b \rightarrow b) \rightarrow b))$.

Let $\tau$ be a unary map on a bounded Hilbert algebra H. In Castiglioni and San Martín (2015, Section 3, Proposition 7), we find proved the following fact: the map $\tau$ is a $\gamma$-operator if and only if for every $a \in H$ the condition

$$\begin{aligned} \tau (a) =\;\text {min}\;\{b\in H: \lnot b\le b\;\text {and}\;a\le b\} \end{aligned}$$

is satisfied. Thus, there is at most one $\gamma$-operator on a bounded Hilbert algebra. But $\gamma$-operators may not exist. In Castiglioni and San Martín (2015, Section 3, Example 14), in contrast with the case of Heyting algebras, we find examples of finite bounded Hilbert algebras that lack a $\gamma$-operator. When a $\gamma$-operator on H exists, it will be denoted by $\gamma$, as we did already for Heyting algebras.

Note that if $H\in \mathsf {Hil}_0$ and $b\in H$, then $\lnot b\le b$ if and only if $\lnot b = 0$. Then, condition $\mathbf{(g4) }$ can be replaced by $\lnot \gamma (a) = 0$.

Lemma 30

Let $H\in \mathsf {Hil}_0$ and $f:H\rightarrow H$ a function which is monotone w.r.t. the natural order. Then, $\lnot f(a) = 0$ for every $a\in H$ if and only if $\lnot f(0) = 0$.

Proof

Suppose that $\lnot f(0) = 0$ and let $a\in H$. Since $0\le a$, then $f(0)\le f(a)$, so $\lnot f(a) \le \lnot f(0) = 0$. Hence, $\lnot f(a) = 0$. $\square$

The next corollary easily follows.

Corollary 31

Let $H\in \mathsf {Hil}_0$. A frontal operator $\tau$ on H is a $\gamma$-operator if and only if $\lnot \tau (0) = 0$ and condition ${\mathbf {(g5)}}$ holds.

We write $\mathsf {Hil}_{\gamma }$ for the algebraic category whose objects are the algebras $(H,\gamma )$ where $H\in \mathsf {Hil}_0$ and $\gamma$ is a $\gamma$-operator. In a similar way, we define the category $\mathsf {IS}_{\gamma }$.

Let $H\in \mathsf {Hil}_0$. For every $a\in H$, we define the set

$$\begin{aligned} \gamma _{a} := \{b\in H:\lnot b \le b\;\text {and}\;a\le b\}. \end{aligned}$$

Proposition 32

Let $H \in {{\mathsf {I}}}{{\mathsf {S}}}_0$. For every $a\in H$, the set $\gamma _{a}$ is a filter. Moreover, if H is finite, then there exists the minimum of $\gamma _a$ for every $a\in H$, i.e., H has a $\gamma$-operator.

Proof

Let $a\in H$. It is immediate that $1\in \gamma _a$ and that $\gamma _a$ is an upset. In what follows, we will show that if $b,c\in \gamma _a$, then $b\wedge c\in \gamma _a$. Let $b,c\in \gamma _a$, i.e., $\lnot b\le b$, $\lnot c \le c$, $a\le b$ and $a\le c$. Thus, $\lnot b = \lnot c = 0$ and $a\le b\wedge c$. Then, $(b\wedge c)\rightarrow 0 = b\rightarrow (c\rightarrow 0) = b\rightarrow 0 = 0$. Hence, $b\wedge c\in \gamma _a$. $\square$

The following is Castiglioni and San Martín (2015, Section 4, Lemma 15).

Lemma 33

Let $(H,\gamma ) \in \mathsf {Hil}_{\gamma }$. Then, $\varphi (\gamma (a)) = \varphi (a) \cup ({\mathrm {Irr}}(H))_M$ for every $a\in H$.

Let $(P,\le )$ be a poset. Note that if $U\in P^+$, then $U \cup X_M\in P^+$.

Lemma 34

Let $(H,\gamma ) \in \mathsf {Hil}_{\gamma }$. Then, $({\mathrm {Irr}}(H)^+, {\gamma ^{\pi }}) \in \mathsf {IS}_{\gamma }$. Moreover, ${\gamma ^{\pi }}$ takes the form $\gamma ^{\pi }(U) = U \cup ({\mathrm {Irr}}(H))_M$.

Proof

We already know that ${\gamma ^{\pi }}$ is a frontal operator. To prove that it is a $\gamma$-operator, we first show that ${\gamma ^{\pi }}(\emptyset ) = ({\mathrm {Irr}}(H))_M$. Let $P\in ({\mathrm {Irr}}(H))_M$. From Corollary 31, we know that $\lnot \gamma (0)\notin P$, so there exists $Q\in {\mathrm {Irr}}(H)$ such that $P\subseteq Q$ and $\gamma (0)\in Q$. Thus, $P = Q$. Since $\gamma (0)\in Q$, then $\gamma (0)\in P$. Therefore, since $\gamma$ is monotone, for every $a \in H$, $\gamma (a) \in P$, i.e., $\gamma ^{-1}[P] = H$. Then, $P\in {\gamma ^{\pi }}(\emptyset )$. Thus, $({\mathrm {Irr}}(H))_M \subseteq {\gamma ^{\pi }}(\emptyset )$. Conversely, assume that $P\in {\gamma ^{\pi }}(\emptyset )$ and that $P\notin ({\mathrm {Irr}}(H))_M$. It follows from Lemma 33 that $\varphi (\gamma (0)) = ({\mathrm {Irr}}(H))_M$, so $\gamma (0)\notin P$, i.e., $0\notin \gamma ^{-1}[P]$. Hence, there exists $Q\in {\mathrm {Irr}}(H)$ such that $\gamma ^{-1}[P]\subseteq Q$, which contradicts the fact that $P\in {\gamma ^{\pi }}(\emptyset )$. We conclude that ${\gamma ^{\pi }}(\emptyset ) \subseteq ({\mathrm {Irr}}(H))_M$. Hence, ${\gamma ^{\pi }}(\emptyset ) = ({\mathrm {Irr}}(H))_M$.

Next we see that $\lnot {\gamma ^{\pi }}(\emptyset ) = \emptyset$. Since $({\mathrm {Irr}}(H))_M = {\gamma ^{\pi }}(\emptyset )$, $\lnot {\gamma ^{\pi }}(\emptyset ) = \lnot ({\mathrm {Irr}}(H))_M$. But $\lnot ({\mathrm {Irr}}(H)_M) = (({\mathrm {Irr}}(H))_M]^c$. Since $\varphi (0) = \emptyset$, it follows from Lemma 33 that $(({\mathrm {Irr}}(H))_M] = {\mathrm {Irr}}(H)$. Then, $\lnot {\gamma ^{\pi }}(\emptyset ) = \emptyset$.

Now we show that ${\gamma ^{\pi }}(U) \subseteq U \cup {\gamma ^{\pi }}(\emptyset )$ for every $U\in {\mathrm {Irr}}(H)^+$. Let $U\in {\mathrm {Irr}}(H)^+$ and $P\in {\gamma ^{\pi }}(U)$. Suppose that $P\notin U$ and $P\notin {\gamma ^{\pi }}(\emptyset )$. The fact that $P\in {\gamma ^{\pi }}(U)$ together with $P\notin U$ implies that $\gamma ^{-1}[P]\nsubseteq P$. Thus, there exists $a\in H$ such that $\gamma (a)\in P$ and $a\notin P$. It follows from Lemma 33 that $\varphi (\gamma (a)) = \varphi (a) \cup ({\mathrm {Irr}}(H))_M$. Since $\gamma (a)\in P$ and $a\notin P$, we have $P\in ({\mathrm {Irr}}(H))_M$. At the beginning of the proof, it was established that ${\gamma ^{\pi }}(\emptyset ) = ({\mathrm {Irr}}(H))_M$, so $P\in {\gamma ^{\pi }}(\emptyset )$, which is a contradiction. Hence, ${\gamma ^{\pi }}(U) \subseteq U \cup {\gamma ^{\pi }}(\emptyset )$. Then, ${\gamma ^{\pi }}$ is the $\gamma$-operator on ${\mathrm {Irr}}(H)^+$, and therefore $({\mathrm {Irr}}(H)^+, {\gamma ^{\pi }}) \in \mathsf {IS}_{\gamma }$.

Finally, we see that ${\gamma ^{\pi }}(U) = U\cup ({\mathrm {Irr}}(H))_M$ for every $U\in {\mathrm {Irr}}(H)^+$. Let $U\in {\mathrm {Irr}}(H)^+$. Since ${\gamma ^{\pi }}(U) \subseteq U \cup {\gamma ^{\pi }}(\emptyset )$ and ${\gamma ^{\pi }}(\emptyset ) = ({\mathrm {Irr}}(H))_M$, it follows that ${\gamma ^{\pi }}(U) \subseteq U \cup ({\mathrm {Irr}}(H))_M$. On the other hand, $U\subseteq {\gamma ^{\pi }}(U)$ and $({\mathrm {Irr}}(H))_M = {\gamma ^{\pi }}(\emptyset ) \subseteq {\gamma ^{\pi }}(U)$, because $\emptyset \subseteq U$. Hence, $U \cup ({\mathrm {Irr}}(H))_M \subseteq {\gamma ^{\pi }}(U)$. Therefore, we obtain that ${\gamma ^{\pi }}(U) = U\cup ({\mathrm {Irr}}(H))_M$. $\square$

In particular, we have that if $(H,\gamma ) \in \mathsf {Hil}_{\gamma }$, then $(\mathrm {L}(H),{\gamma ^{\pi }})\in \mathsf {IS}_{\gamma }$. This follows from the facts that, being ${\gamma ^{\pi }}$ a frontal operator, $\mathrm {L}(H)$ is closed under ${\gamma ^{\pi }}$ and that in a Heyting algebra the existence of $\gamma$ is equivalent to the existence of a frontal operator $\tau$ that satisfies $\lnot \tau (0) = 0$ and $\tau (a) \le a \vee \tau (0)$ for every a.

The following proposition follows from Corollary 29 and Lemma 34.

Proposition 35

The functor $(\ )^{\mathsf {FIS}}:\mathsf {FHil}_0 \rightarrow \mathsf {FIS}_0$ can be restricted to a functor $(\ )^{\mathsf {FIS}}: \mathsf {Hil}_{\gamma }\rightarrow \mathsf {IS}_{\gamma }$ that is left adjoint to the forgetful functor ${\mathrm {U}}: \mathsf {IS}_{\gamma }\rightarrow \mathsf {Hil}_{\gamma }$.

5 An adjunction between $\mathsf {Hil_{S}}$ and $\mathsf {IS_{S}}$

In Kuznetsov (1985), Kuznetsov introduced a new unary operation on Heyting algebras as an attempt to build an intuitionistic version of the provability logic of Gödel-Löb, which formalizes the concept of provability in Peano Arithmetic. This unary operation, which we shall call successor, was also studied by Caicedo and Cignoli (2001) and by Esakia (2006). A unary operation S on a Heyting algebra is a successor operation if it satisfies for very $a \in H$ the following conditions:

• (1) $a\le S(a)$,

• (2) $S(a)\le b\vee (b\rightarrow a)$,

• (3) $S(a)\rightarrow a = a$.

The conditions $a\le S(a)$ and $S(a)\rightarrow a = a$ can be replaced by the single condition $S(a)\rightarrow a \le S(a)$, as it was shown in Castiglioni et al. (2010). In Castiglioni et al. (2010, Proposition 2.3), it was proved that in fact a unary map S on a Heyting algebra H is a successor operation if and only if it is a frontal operator that satisfies $S(a)\rightarrow a = a$ for every $a \in H$.

Moreover, in Castiglioni et al. (2010) it was also proved that a unary operation S on a Heyting algebra H is a successor operation if and only if for every $a \in H$ it holds that

$$\begin{aligned} S(a) =\;\text {min}\{b:b\rightarrow a\le b\}. \end{aligned}$$

Therefore, if a successor operation exists on a Heyting algebra, then it is unique. The successor operation exists in all finite Heyting algebras (see Caicedo and Cignoli 2001), but there are examples of Heyting algebras where there is no successor operation.

Let $(P,\le )$ be a poset. We know that $P^+$ is a complete Heyting algebra. In what follows, we will see that the existence of a successor operation in $P^+$ can be easily described in terms of a certain condition on $(P,\le )$. This result provides examples of complete Heyting algebras without a successor operation.

Recall that a poset $(P,\le )$ satisfies the ascending chain condition (ACC) if every strictly ascending sequence of elements eventually terminates. Equivalently, given any sequence $x_{1} \le x_{2} \le x_{3}\le \cdots$ there exists a natural number n such that $x_n = x_m$ for every $m\ge n$. It is known that the (ACC) is equivalent to the following condition: every nonempty subset of P has a maximal element. Notice that straightforward computations show that the (ACC) is also equivalent to the following condition, that will be called (P): for every downset V of $(P,\le )$, if $x\in V$, then there exists $y\in V_M$ such that $x\le y$. Moreover, the condition (P) is equivalent to the following one: for every downset V of $(P,\le )$, $V = (V_M]$.

Let $(P,\le )$ be a poset. Consider the co-derivative frontal operator $\tau :P^+ \rightarrow P^+$, that, as we saw in Corollary 5, satisfies that $\tau (U) = U \cup (U^c)_M$ for every $U \in P^{+}$. It follows that for every $U \in P^{+}$, $\tau (U) \Rightarrow U = ((U^c)_M]^c$. Therefore, $\tau$ is a successor operation on $P^+$ if and only if $(P,\le )$ satisfies the (ACC). This property can also be obtained from results in Kuznetsov (1979).

The following question arises then naturally: Is the (ACC) satisfied when $P^+$ has successor operation? The next theorem answers it in the positive.

Theorem 36

Let $(P, \le )$ be a poset. Then, $P^{+}$ has a successor operation if and only if $(P, \le )$ satisfies ${\mathrm {(ACC)}}$.

Proof

It follows from the discussion above that if $(P,\le )$ satisfies the (ACC), then $P^+$ has a successor operation S that takes the form $S(U) = U\cup (U^c)_M$ for every $U \in P^{+}$.

Conversely, suppose that $P^+$ has a successor operation S. Let us consider the co-derivative frontal operator $\tau :P^+ \rightarrow P^+$. To see that $(P,\le )$ has the (ACC), it is enough to see that $\tau = S$. To this end, we prove first the following claims.

Claim 1. If f is a frontal operator on $P^+$, then $f(U) \subseteq S(U)$ for every $U\in P^+$. In order to prove it, let $U\in P^+$. Then, since f is a frontal operator we have $f(U) \subseteq S(U) \cup (S(U) \Rightarrow U) = S(U) \cup U = S(U)$.

Claim 2. If $\{U_{i}\}_{i\in I}\subseteq P^+$, then $S(\bigcap _{i\in I} U_i) \subseteq \bigcap _{i\in I} S(U_{i})$. This holds because S is a monotone map.

Claim 3. In $P^+$, the operator $\tau$ preserves arbitrary meets. In order to show it, let $\{U_{i}\}_{i\in I} \subseteq P^+$. The monotonicity of $\tau$ implies that $\tau (\bigcap _{i\in I} U_{i}) \subseteq \bigcap _{i\in I} \tau (U_{i})$. Conversely, let $x\in \bigcap _{i\in I} \tau (U_{i})$. If $x\in \bigcap _{i\in I} U_{i}$, then $x \in \tau (\bigcap _{i\in I} U_{i})$. On the contrary, if $x\notin \bigcap _{i\in I} U_{i}$, let us see that $x \in ((\bigcap _{i\in I} U_{i})^{c})_M$. To this end, suppose that $x \le y$ with $y \not \in \bigcap _{i\in I} U_{i}$. Thus, there exists $j \in I$ such that $y\notin U_{j}$, and being $U_j$ an upset we have $x \not \in U_j$. Hence, since $x \in \tau (U_j)$, $x \in (U_{j}^{c})_M$. Therefore, $x = y$. We conclude that $\tau (\bigcap _{i\in I} U_{i}) = \bigcap _{i\in I} \tau (U_{i})$.

Claim 4: For every $x\in P$, $S((x]^{c}) = \tau ((x]^{c}) = (x]^{c} \cup \{x\}$. In order to prove it, first note that $\tau ((x]^{c}) \Rightarrow (x]^c = (x]^c$. On the other hand, by Claim 1 we know that $\tau ((x]^{c}) \subseteq S((x]^{c})$. Using that $\tau$ is a frontal operator on the Heyting algebra $P^+$ and the fact that $\tau ((x]^{c}) \Rightarrow (x]^c = (x]^c$, we will prove that $S((x]^{c}) \subseteq \tau ((x]^{c})$ as follows:

$$\begin{aligned} \begin{array} [c]{lllll} S((x]^{c})&{} \subseteq &{} \tau ((x]^{c}) \cup (\tau ((x]^{c}) \Rightarrow (x]^{c})&{} &{} \\ &{} = &{} \tau ((x]^{c}) \cup (x]^c &{} &{} \\ &{} = &{} \tau ((x]^{c}).&{} &{} \end{array} \end{aligned}$$

Thus, $S((x]^{c}) = \tau ((x]^{c})$.

Now we use the previous claims to show that for every $U\in P^+$ we have $\tau (U) = S(U)$. To this end, we first note that for every downset V it clearly holds that $V= \bigcup _{x\in V} (x]$. Thus, for very upset U we have $U = \bigcap _{x \in U^{c}}(x]^{c}$. Let $U\in P^+$. Then,

$$\begin{aligned} \begin{array} [c]{lllll} \tau (U)&{} \subseteq &{} S(U)&{} &{} \\ &{} = &{} S\left( \bigcap _{x\in U^c}(x]^c\right) &{} &{} \\ &{} \subseteq &{} \bigcap _{x\in U^c}S((x]^c) &{} &{} \\ &{} = &{} \bigcap _{x\in U^c}\tau ((x]^c) &{} &{} \\ &{} = &{} \tau \left( \bigcap _{x\in U^c}(x]^c\right) &{} &{} \\ &{} = &{} \tau (U).&{} &{} \end{array} \end{aligned}$$

Therefore, $\tau (U) = S(U)$, which was our aim. $\square$

Theorem 36 implies that not every Heyting algebra has a successor operation. Indeed, if $(P,\le )$ is a poset that does not satisfy the (ACC), then the Heyting algebra $P^{+}$ has no successor. This can be used to give an example of a Heyting algebra with successor (H, S) such that the Heyting algebra ${\mathrm {Irr}}(H)^+$ of the upsets of the partial order of the irreducible implicative filters of H (which are the prime filters of H) does not have a successor operation. For instance, if ${\mathbb {N}}^{0}$ is the set of natural numbers with its inverse order, and $\oplus$ is the ordinal sum of posets (see Balbes and Dwinger 1974, p. 39), then ${\mathbb {N}}\oplus {\mathbb {N}}^{0}$ is a Heyting algebra with successor operation. However, $({\mathrm {Irr}}({\mathbb {N}}\oplus {\mathbb {N}}^{0}))^{+}$ is not a Heyting algebra with successor operation because the (ACC) is not satisfied in the poset ${\mathrm {Irr}}({\mathbb {N}}\oplus {\mathbb {N}}^{0})$. The fact that $({\mathrm {Irr}}({\mathbb {N}}\oplus {\mathbb {N}}^{0}))^{+}$ is not a Heyting algebra with successor operation was also mentioned in Castiglioni and San Martín (2012).

In Castiglioni and San Martín (2015), the successor operation defined on Heyting algebras was generalized to the setting of Hilbert algebras.

Let $H\in \mathsf {Hil}$. A unary function $S:H\rightarrow H$ is a successor operation if for every $a, b \in H$ the following conditions are satisfied:

(S1) :

$S(a) \le ((b\rightarrow a)\rightarrow b)\rightarrow b$,

(S2) :

$S(a)\rightarrow a \le S(a)$.

for every $a, b \in H$.

It follows from Castiglioni and San Martín (2015, Section 3, Corollary 4) and Castiglioni and San Martín (2015, Section 3, Proposition 5) that a unary function S on a Hilbert algebra H is a successor operation if and only if it is a frontal operator that satisfies the equality

$$\begin{aligned} S(a)\rightarrow a = a \end{aligned}$$

for every $a\in H$. Moreover, it was also proved in Castiglioni and San Martín (2015) that a unary map S on a Hilbert algebra is a successor operation if and only if for every $a \in H$,

$$\begin{aligned} S(a) =\;\text {min}\; \{b\in H:b\rightarrow a \le b\}. \end{aligned}$$

Thus, if there exists a successor operation on a Hilbert algebra, then it is unique. There are examples of finite Hilbert algebras where no successor operation exists, see for instance Castiglioni and San Martín (2015, Section 3, Example 14).

Definition 37

We say that an algebra (H, S) is a Hilbert algebra with successor if H is a Hilbert algebra and S is a successor operation.

In a similar way, we define implicative semilattices with successor. We write $\mathsf {Hil_{S}}$ for the algebraic category of Hilbert algebras with successor and $\mathsf {IS_{S}}$ for the algebraic category of implicative semilattices with successor.

Let $H\in {{\mathsf {I}}}{{\mathsf {S}}}$. For every $a\in H$, we define the set

$$\begin{aligned} S_{a} = \{b\in H:b\rightarrow a\le b\}. \end{aligned}$$

Proposition 38

Let $H\in {{\mathsf {I}}}{{\mathsf {S}}}$. For every $a\in H$, the set $S_{a}$ is a filter. Moreover, if H is finite, then there exists the minimum of $S_a$ for every $a\in H$, i.e., there exists a successor operation.

Proof

Suppose that $a\in H$. It is immediate that $1\in S_a$. We will prove that $S_a$ is an upset. Let $b\le c$ and $b\in S_a$. Thus, $b\rightarrow a \le b$ and $c \rightarrow a \le b\rightarrow a$. Since $b\le c$, then $c\rightarrow a \le c$, i.e., $c\in S_a$. Thus, $S_a$ is an upset.

We proceed to show that if $b,c\in S_a$, then $b\wedge c\in S_a$. Let $b,c\in S_a$, i.e., $b\rightarrow a \le b$ and $c\rightarrow a\le c$. Note that $b\wedge ((b\wedge c) \rightarrow a) \le c\rightarrow a \le c$, so $b \wedge ((b\wedge c)\rightarrow a)\le b\wedge c$. Besides, we have that $b\wedge ((b\wedge c)\rightarrow a) \le (b\wedge c)\rightarrow a$. Thus, $b\wedge ((b\wedge c)\rightarrow a) \le a$ and hence $(b\wedge c)\rightarrow a \le b\rightarrow a$. Since $b\rightarrow a\le b$, we obtain that $(b\wedge c)\rightarrow a \le b$. Using an analogous argument, we also obtain that $(b\wedge c)\rightarrow a \le c$. Hence, $(b\wedge c)\rightarrow a \le b \wedge c$ and therefore $b\wedge c \in S_a$. $\square$

The following lemma is Castiglioni and San Martín (2015, Section 4, Lemma 8).

Lemma 39

If $(H,S)\in \mathsf {Hil_{S}}$, then $\varphi (S(a)) = \varphi (a) \cup (\varphi (a)^{c})_M$ for every $a\in H$.

The next lemma will be used later.

Lemma 40

Let $(P,\le )$ be a poset and $U_1,\ldots ,U_n\in P^+$. Then,

$$\begin{aligned} \bigcap _{i=1}^{n}(U_i \cup (U_{i}^{c})_M) = \left( \bigcap _{i=1}^{n} U_i\right) \cup \left( \bigcup _{i=1}^{n} U_{i}^{c}\right) _M. \end{aligned}$$

Proof

Consider a poset $(P,\le )$. It follows from Corollary 5 that the co-derivative frontal operator $\tau$ of the Heyting algebra $P^{+}$ is such that $\tau (U) = U \cup (U^{c})_M$, for every $U \in P^{+}$. Since $\tau$ is a frontal operator on the Heyting algebra $P^+$, then $\tau$ preserves finite meets. Therefore, we obtain the desired result. $\square$

The following lemma is a generalization of Diego (1965, Lemma 7). To prove it, we introduce the following definition. Let $H\in \mathsf {Hil}$ and $a\in H$. We define the set

$$\begin{aligned} \sigma (a) := \{F\in \mathsf {Fil}(H):a\in F\}. \end{aligned}$$

Lemma 41

Let H be a Hilbert algebra and $a_1,\ldots ,a_n\in H$. Then,

$$\begin{aligned} \bigcup _{i=1}^{n} \varphi (a_i)^c = \left[ \left( \bigcup _{i=1}^{n} \varphi (a_i)^c\right) _M \right] . \end{aligned}$$

Proof

Assume that $P \in \bigcup _{i=1}^{n} \varphi (a_i)^c$. Consider the set

$$\begin{aligned} \Sigma =\left\{ Q\in \mathsf {Fil}(H):P\subseteq Q\;\text {and}\;Q\in \bigcup _{i=1}^{n} \sigma (a_i)^c\right\} . \end{aligned}$$

Since $P\in \Sigma$, $\Sigma \ne \emptyset$. Straightforward computations show that if $\{Q_i\}_{i\in I}$ is a chain of elements in $\Sigma$, then $\bigcup _{i \in I}Q_i \in \Sigma$, so by Zorn’s lemma there exists a maximal element in $\Sigma$, which will be denoted by Q. In what follows, we see that $Q\in {\mathrm {Irr}}(H)$ by using Lemma 9. Let $a,b\notin Q$. We prove that there exists $c\notin Q$ such that $a\le c$ and $b\le c$. Assume the contrary, i.e., that for every $c\in H$ if $a\le c$ and $b\le c$, then $c\in Q$. Thus, $[a)\cap [b) \subseteq Q$, and hence $Q = Q \vee ([a)\cap [b))$. Since the lattice of implicative filters of H is distributive (Diego 1965, Theorem 6), we have $Q = (Q\vee [a))\cap (Q\vee [b))$ (note that $Q\vee [a) = F(Q \cup \{a\})$ and $Q\vee [b) = F(Q \cup \{b\})$). Since $P\subseteq Q\subset Q\vee [a)$ and $P\subseteq Q\subset Q\vee [b)$, it follows from the maximality of Q that $Q\vee [a), Q\vee [b) \notin \Sigma$. In particular, we obtain that $a_1,\ldots ,a_n \in (Q\vee [a))\cap (Q\vee [b)) = Q$, which is a contradiction. Hence, $Q\in {\mathrm {Irr}}(H)$ and, moreover, $Q\in \bigcup _{i=1}^{n} \varphi (a_i)^c$. We prove that Q is maximal in this set. To this end, assume that $Q'\in {\mathrm {Irr}}(H)$ is such that $Q\subseteq Q'$ and $Q'\in \bigcup _{i=1}^{n} \varphi (a_i)^c$. In particular, $Q'\in \bigcup _{i=1}^{n} \sigma (a_i)^c$, so $Q'\in \Sigma$. Thus, $Q = Q'$. Therefore, $P\subseteq Q$ with $Q\in (\bigcup _{i=1}^{n} \varphi (a_i)^c)_M$, and hence $P \in ((\bigcup _{i=1}^{n} \varphi (a_i)^c)_M]$. We conclude that $\bigcup _{i=1}^{n} \varphi (a_i)^c \subseteq ((\bigcup _{i=1}^{n} \varphi (a_i)^c)_M]$. The converse inclusion is immediate. $\square$

It is straightforward to see that for every poset $(P,\le )$ and $U\in P^+$, $U \cup (U^{c})_M \in P^+$.

Lemma 42

Let $(H,S) \in \mathsf {Hil_{S}}$. Then, $(\mathrm {L}(H), \mathrm {S^{\pi }}) \in \mathsf {IS_{S}}$. Moreover, $\mathrm {S^{\pi }}$ takes the form $\mathrm {S^{\pi }}(U) = U \cup (U^c)_M$.

Proof

Suppose that $U\in \mathrm {L}(H)$; so there exist $a_1,\ldots ,a_n\in H$ such that $U = \bigcap _{i=1}^{n} \varphi (a_i)$. The frontal operator $\mathrm {S^{\pi }}$ on ${\mathrm {Irr}}(H)^{+}$ applied to U gives that

$$\begin{aligned} \mathrm {S^{\pi }}(U) = \bigcap _{i = 1}^{n} \varphi (S(a_i)). \end{aligned}$$

Then, Lemma 39 implies

$$\begin{aligned} \mathrm {S^{\pi }}(U) = \bigcap _{i = 1}^{n} (\varphi (a_i) \cup (\varphi (a_i)^{c})_M). \end{aligned}$$

Now using Lemma 40 we obtain that

$$\begin{aligned} \mathrm {S^{\pi }}(U) = \bigcap _{i = 1}^{n} \varphi (a_i) \cup \left( \left( \bigcap _{i = 1}^{n} \varphi (a_i)\right) ^{c}\right) _M. \end{aligned}$$

Therefore, $\mathrm {S^{\pi }}(U) = U \cup (U^{c})_M$. Since $\mathrm {S^{\pi }}$ is a frontal operator, to show that it is a successor we only need to prove that $\mathrm {S^{\pi }}(U)\Rightarrow U = U$. This holds if and only if $(U^{c}_M]^c = U$. But it follows from Lemma 41 that $(U^{c}_M]^c = U$. Therefore, the implicative semilattice $\mathrm {L}(H)$ has successor $\mathrm {S^{\pi }}$ and $\mathrm {S^{\pi }}(U) = U \cup (U^{c})_M$. $\square$

The following proposition follows from Proposition 27, Lemma 42 and Theorem 28.

Proposition 43

The functor $(\ )^{{{\mathsf {I}}}{{\mathsf {S}}}}:\mathsf {Hil}\rightarrow {{\mathsf {I}}}{{\mathsf {S}}}$ can be extended to a functor $(\ )^{\mathsf {FIS}}: \mathsf {Hil_{S}}\rightarrow \mathsf {IS_{S}}$ that is left adjoint to the forgetful functor ${\mathrm {U}}: \mathsf {IS_{S}}\rightarrow \mathsf {Hil_{S}}$.

6 An adjunction between $\mathsf {Hil_{G}}$ and $\mathsf {IS_{G}}$

In Caicedo and Cignoli (2001, Example 5.3), Caicedo and Cignoli studied an example of implicit compatible operation of Heyting algebras that was considered by Gabbay (1977). When it exists, it is also a case of a frontal operator.

Let H be a Heyting algebra. A unary map G on H is a Gabbay function (G-function for short) if the following conditions are satisfied for every $a, b \in H$:

• (1) $G(a)\le b \vee (b\rightarrow a)$,

• (2) $a\rightarrow b\le G(a)\rightarrow G(b)$,

• (3) $a\le G(a)$,

• (4) $G(a)\le \lnot \lnot a$,

• (5) $G(a)\rightarrow a \le \lnot \lnot a \rightarrow a$.

In Castiglioni et al. (2010), it was proved that a unary map G on a Heyting algebra is a G-function if and only if for every $a \in H$,

$$\begin{aligned} G(a) = \;\text {min}\;\{b\in H:(b\rightarrow a) \wedge \lnot \lnot a \le b\}. \end{aligned}$$

Thus, if there is a G-function on a Heyting algebra, then it is unique. In every finite Heyting algebra, the function G exists (see Caicedo and Cignoli 2001). However, there are examples of Heyting algebras where no Gabbay function exists. In Castiglioni et al. (2010, Proposition 2.7), it was also proved that a G-function of a Heyting algebra is a frontal operator.

In Castiglioni and San Martín (2015), the notion of Gabbay function was generalized to the framework of bounded Hilbert algebras. Let $H\in \mathsf {Hil}_0$. We say that function $G:H\rightarrow H$ is a G-function if the inequalities ${\mathbf {(i2)}}$, ${\mathbf {(i3)}}$ hold as well as the following additional ones:

(G4) :

$G(a)\le \lnot \lnot a$,

(G5) :

$G(a) \rightarrow a \le \lnot \lnot a\rightarrow a$.

Let $H\in \mathsf {Hil}_0$. It follows from Castiglioni and San Martín (2015, Section 3, Corollary 19) that a unary map G is a G-function if and only if it is a frontal operator that satisfies the additional conditions $\mathbf{(G4) }$ and $\mathbf{(G5) }$. It is interesting to note that in Castiglioni and San Martín (2015, Section 3, Proposition 10) it was proved that a G-function is also characterized by the fact that for every $a \in H$

$$\begin{aligned} G(a) = \;\text {min}\; \{b\in H: b\rightarrow a\le \lnot \lnot a \rightarrow b\}. \end{aligned}$$

There are examples of finite bounded Hilbert algebras where no G-function exists, see for instance Castiglioni and San Martín (2015, Section 3, Example 15).

We write $\mathsf {Hil_{G}}$ for the algebraic category whose objects are the algebras (H, G) where $H\in \mathsf {Hil}_0$ and G is a G-function. In a similar way, we define $\mathsf {IS_{G}}$.

Let $H\in \mathsf {Hil}_0$. For every $a\in H$, we define $G_{a} := \{b\in H:b\rightarrow a\le \lnot \lnot a \rightarrow b\}$. If $H\in {{\mathsf {I}}}{{\mathsf {S}}}_0$, then $G_a = \{b\in H:\lnot \lnot a \wedge (b\rightarrow a)\le b\}$.

Proposition 44

Let $H\in {{\mathsf {I}}}{{\mathsf {S}}}_0$. For every $a\in H$, the set $G_{a}$ is a filter. Moreover, if H is finite, then there exists the minimum of $G_a$ for every $a\in H$, i.e., there exists a G-function.

Proof

Let $a\in H$. It is immediate that $1\in G_a$. We prove that $G_a$ is an upset. Let $b\le c$ and $b\in G_a$. Then, $\lnot \lnot a \wedge (b\rightarrow a) \le b$ and $c \rightarrow a \le b\rightarrow a$. Taking into account that $b\le c$, we deduce that $\lnot \lnot a \wedge (c\rightarrow a) \le c$, i.e., $c\in G_a$. Thus, $G_a$ is an upset.

We proceed to show that if $b,c\in G_a$, then $b\wedge c\in G_a$. Let $b,c\in G_a$, i.e., $\lnot \lnot a \wedge (b\rightarrow a) \le b$ and $\lnot \lnot a \wedge (c\rightarrow a)\le c$. Note that

$$\begin{aligned} \lnot \lnot a \wedge (b\wedge ((b\wedge c) \rightarrow a)) \le \lnot \lnot a \wedge (c\rightarrow a) \le c, \end{aligned}$$

so we get

$$\begin{aligned} \lnot \lnot a \wedge b \wedge ((b\wedge c)\rightarrow a)\le b\wedge c. \end{aligned}$$

Moreover, $\lnot \lnot a \wedge b\wedge ((b\wedge c)\rightarrow a) \le (b\wedge c)\rightarrow a$. Thus, $\lnot \lnot a \wedge b\wedge ((b\wedge c)\rightarrow a) \le a$. It follows that $\lnot \lnot a \wedge ((b\wedge c)\rightarrow a) \le b\rightarrow a$. Hence, using that $b \in G_a$,

$$\begin{aligned} \lnot \lnot a \wedge ((b\wedge c)\rightarrow a) \le \lnot \lnot a \wedge (b\rightarrow a) \le b, \end{aligned}$$

Using an analogous argument, we obtain $\lnot \lnot a \wedge ((b\wedge c)\rightarrow a) \le c$. Therefore, $\lnot \lnot a \wedge ((b\wedge c)\rightarrow a) \le b \wedge c$, i.e., $b\wedge c \in G_a$. $\square$

The following is Castiglioni and San Martín (2015, Section 3, Lemma 17).

Lemma 45

Let $(H,G) \in \mathsf {Hil_{G}}$. Then, $\varphi (G(a)) = \varphi (a) \cup (\varphi (\lnot \lnot a)\cap (\varphi (a)^{c})_M)$ for every $a\in H$.

Let H be a bounded Hilbert algebra and $a\in H$. We have that $\varphi (\lnot a) = \varphi (a) \Rightarrow \varphi (0) = \varphi (a) \Rightarrow \emptyset$. In what follows, we write $\lnot \varphi (a)$ in place of $\varphi (a) \Rightarrow \emptyset$.

Let $(P,\le )$ be a poset and let $U\in P^+$. Note that $U \cup ((\lnot \lnot U) \cap (U^c)_M) \in P^+$, because $U \cup ((\lnot \lnot U) \cap (U^c)_M) = (U \cup (U^c)_M)\cap \lnot \lnot U$ and $U \cup (U^c)_M \in P^+$.

Lemma 46

If $(H,G) \in \mathsf {Hil_{G}}$, then $(\mathrm {L}(H), \mathrm {G^{\pi }}) \in \mathsf {IS_{G}}$. Moreover, $\mathrm {G^{\pi }}$ takes the form $\mathrm {G^{\pi }}(U) = U \cup ((\lnot \lnot U) \cap (U^c)_M)$.

Proof

Assume that $U\in \mathrm {L}(H)$, so there exist $a_1,\ldots ,a_n\in H$ such that $U = \varphi (a_1)\cap \cdots \cap \varphi (a_n)$. In what follows, we see that $\mathrm {G^{\pi }}(U) =U \cup ((\lnot \lnot U) \cap (U^c)_M)$.

It follows from Lemma 45 that $\varphi (G(a_i)) = \varphi (a_i)\cup [\varphi (\lnot \lnot a_i) \cap (\varphi (a_i)^{c})_M]$ for every $i=1,\ldots ,n$. Hence, using Lemma 40 we have

$$\begin{aligned} \begin{array} [c]{lllll} \mathrm {G^{\pi }}(U)&{} = &{} \bigcap _{i=1}^{n} \varphi (G(a_i))&{} &{} \\ &{} = &{} \bigcap _{i=1}^{n} \varphi (a_i)\cup [\varphi (\lnot \lnot a_i) \cap (\varphi (a_i)^{c})_M] &{} &{} \\ &{} = &{} \bigcap _{i=1}^{n}(\varphi (a_i)\cup (\varphi (a_i)^{c})_M) \cap \varphi (\lnot \lnot a_i) &{} &{} \\ &{} = &{} \left( \bigcap _{i=1}^{n} \varphi (a_i)\cup (\varphi (a_i)^{c})_M\right) \cap \left( \bigcap _{i=1}^{n} \lnot \lnot \varphi (a_i)\right) &{} &{} \\ &{} = &{} (U \cup (U^c)_M) \cap \lnot \lnot \left( \bigcap _{i=1}^{n} \varphi (a_i)\right) &{} &{} \\ &{} = &{} (U \cup (U^c)_M) \cap \lnot \lnot U.&{} &{} \end{array} \end{aligned}$$

Therefore, $\mathrm {G^{\pi }}(U) = U \cup ((U^c)_M \cap \lnot \lnot U)$.

Now we prove that $\mathrm {G^{\pi }}$ is a G-function. Let $U\in \mathrm {L}(H)$. Then, $\mathrm {G^{\pi }}(U) = U \cup ((\lnot \lnot U) \cap (U^c)_M) \subseteq U \cup \lnot \lnot U = \lnot \lnot U$, so $\mathrm {G^{\pi }}(U) \subseteq \lnot \lnot U$. Finally, we will need to prove that $\mathrm {G^{\pi }}(U) \Rightarrow U \subseteq \lnot \lnot U \Rightarrow U$, i.e., $(\lnot \lnot U \cap U^c] \subseteq (\lnot \lnot U \cap (U^c)_M]$. This inclusion follows from Lemma 41. $\square$

The following proposition follows from Corollary 29 and Lemma 46.

Proposition 47

The functor $(\ )^{\mathsf {FIS}}:\mathsf {FHil}_0 \rightarrow \mathsf {FIS}_0$ can be restricted to a functor $(\ )^{\mathsf {FIS}}: \mathsf {Hil_{G}}\rightarrow \mathsf {IS_{G}}$ that is left adjoint to the forgetful functor ${\mathrm {U}}:\mathsf {IS_{G}}\rightarrow \mathsf {Hil_{G}}$.

As in the case of Heyting algebras with successor, we have that ${\mathbb {N}}\oplus {\mathbb {N}}^{0}$ is a Heyting algebra with a G-function. It can also be proved that $({\mathrm {Irr}}({\mathbb {N}}\oplus {\mathbb {N}}^{0}))^{+}$ is not a Heyting algebra with a G-function.