1 Introduction

In what follows, we assume the reader is familiar with the theory of Heyting algebras (Balbes and Dwinger 1974), which are the algebraic counterpart of Intuitionistic Propositional Logic. Hilbert algebras were introduced in the early 1950s by Henkin for some investigations of implication in intuitionistic and other non-classical logics (Rasiowa 1974, pp. 16). In the 1960s, they were studied especially by Horn (1962) and Diego (1965).

Let K be any variety in the language \(\mathscr {L}_K\) and \(\mathscr {L}\) a sublanguage of \(\mathscr {L}_K\). Assume that the class of \({\mathscr {L}}\)-subreducts of the elements of K form a variety M. Let us also write K and M, for the algebraic categories whose class of objects are the members of the varieties K and M, respectively. The correspondence assigning each member of K to its \(\mathscr {L}\)-reduct induces a functor \(U{:}\,K \rightarrow M\), which is usually referred to as the forgetful functor from K to M, since part of the structure of each member in K is forgotten. It can be seen that this functor has a left adjoint \(F{:}\,M \rightarrow K\) (see for instance, Moraschini 2018, Theorem 3.5). For any \(a \in M\), the element \(F(a) \in K\) is usually referred to as the free K-extension of a. However, the usual general arguments guaranteeing its existence do not provide an easy description of it.

Celani and Jansana (2012) gave a concrete description of the free implicative semilattice extension of a Hilbert algebra, from where an explicit description for the left adjoint of the forgetful functor from the category of implicative semilattices to the category of Hilbert algebras follows.

The main goal of this paper is to arrive at the explicit description of the adjunction presented in Celani and Jansana (2012) following an alternative path. We also apply these ideas in order to provide similar constructions for the category of generalized Heyting algebras.

The paper is organized as follows. In Sect. 2, we give some basic results about Hilbert algebras. In particular, we recall the categorical equivalence for Hilbert algebras developed by Cabrer et al. (2009) (see also Celani and Montangie 2012). In Sect. 3, we use the equivalence for the category of Hilbert algebras in order to build up a functor from the category of Hilbert algebras to the category of implicative semilattices. We also present an explicit description for the left adjoint to the forgetful functor from the category of implicative semilattices to the category of Hilbert algebras. Finally, we establish the connections between our results and those of Celani and Jansana (2012). In Sect. 4, we give an explicit description for the left adjoint to the forgetful functor from the category of generalized Heyting algebras (Heyting algebras) to the category of Hilbert algebras with supremum (Hilbert algebras with supremum and a minimum). Finally, in Sect. 5, we build up a functor from the category of Hilbert algebras to the category of generalized Heyting algebras and we comment some open problems.

2 Basic results

Recall that a Hilbert algebra (see Diego 1965) is an algebra \((H,\rightarrow ,1)\) of type (2, 0) which satisfies the following conditions for every \(a,b,c\in H\):

  1. (a)

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

  2. (b)

    \((a\rightarrow (b\rightarrow c)) \rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c)) = 1\),

  3. (c)

    if \(a\rightarrow b = b\rightarrow a = 1\) then \(a = b\).

Diego (1965) proves that the class of Hilbert algebras is a variety. Moreover, this is the variety generated by the \(\{1,\rightarrow \}\)-reduct of Heyting algebras. In every Hilbert algebra H, we have a partial order given by \(a\le b\) if and only if \(a\rightarrow b = 1\), which is called natural order. Relative to the natural order on H, 1 is the greatest element.

We write \(\mathsf {Hil}\) for the variety of Hilbert algebras. Observe that \(\mathsf {Hil}\), when equipped with homomorphisms, has the structure of a category.

Lemma 1

Let \(H\in \mathsf {Hil}\) and \(a,b,c\in H\). Then the following conditions are satisfied:

  1. (a)

    \(a\rightarrow a = 1\),

  2. (b)

    \(1\rightarrow a = a\),

  3. (c)

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

  4. (d)

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

  5. (e)

    if \(a\le b\) then \(c\rightarrow a \le c\rightarrow b\) and \(b\rightarrow c \le a\rightarrow c\).

Some additional elemental properties of Hilbert algebras can be found in Buşneag and Ghiţǎ (2010) and Diego (1965).

For the general development of Hilbert algebras, the notion of implicative filter plays an important role. Let H be a Hilbert algebra. A subset \(F\subseteq H\) is said to be a implicative filter if the following two conditions are satisfied: (1) \(1\in F\); (2) if \(a\in F\) and \(a\rightarrow b \in F\) then \(b\in F\). If in addition \(F\ne H\), then we say that the implicative filter F is proper. Let \(f{:}\,H\rightarrow G\) be a function between Hilbert algebras. Celani (2002, Theorem 3.2) it was proved that 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\); (2) \(f^{-1}(F)\) is an implicative filter of H whenever F is an implicative filter of G.

Definition 1

Let \(H\in \mathsf {Hil}\) and F an implicative filter. We say that F is irreducible if F is proper and for any implicative filters \(F_1, F_2\) such that \(F = F_1 \cap F_2\) we have that \(F = F_1\) or \(F = F_2\). We write X(H) for the set of irreducible implicative filters of H.

Let us consider a poset \(\left\langle X,\le \right\rangle \). A subset \(U\subseteq X\) is said to be an upset if for all \(x, y \in X\) such that \(x\in U\) and \(x\le y\) we have \(y\in U\). The notion of downset is dually defined.

Remark 1

Every implicative filter of a Hilbert algebra is an upset.

Let \(H\in \mathsf {Hil}\) and \(I \subseteq H\) with \(I\ne \emptyset \). We say that I is an order-ideal if I is a downset and for every \(a,b\in I\) there is \(c\in I\) such that \(a\le c\) and \(b\le c\). Let \(\mathsf {Id}(H)\) be the set of order-ideals of H and \(\mathsf {Fil}(H)\) the set of implicative filters of H. The following lemma is Celani (2002, Theorem 2.6). (It is also an immediate consequence of the work of polarities and optimality as carried on for instance in Gehrke et al. 2010, Proposition 6.7.)

Lemma 2

Let \(H\in \mathsf {Hil}\). Let \(F\in \mathsf {Fil}(H)\) and \(I \in \mathsf {Id}(H)\) such that \(F\cap I = \emptyset \). Then there exists \(P\in X(H)\) such that \(F\subseteq P\) and \(P\cap I = \emptyset \).

Recall that if H is a Hilbert algebra and \(X \subseteq H\), we define the implicative filter generated by X as the least filter of H that contains the set X, which will be denoted by F(X). There is an explicit description for F(X) (see Buşneag 1985, Lemma 2.3):

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

The following known results are consequence of Lemma 2.

Corollary 3

Let \(H\in \mathsf {Hil}\), \(F \in \mathsf {Fil}(H)\) and \(a \notin F\). Then there exists \(P\in X(H)\) such that \(F\subseteq P\) and \(a\notin P\).

Corollary 4

Let \(H\in \mathsf {Hil}\) and \(a,b\in H\) such that \(a\nleq b\). Then there exists \(P\in X(H)\) such that \(a\in P\) and \(b\notin P\).

Corollary 5

Let \(H\in \mathsf {Hil}\), \(F\in \mathsf {Fil}(H)\) and \(a,b\in H\). Then \(a\rightarrow b \notin F\) if and only if there exists \(P\in X(H)\) such that \(F\subseteq P\), \(a\in P\) and \(b\notin P\).

If \(f{:}\,H\rightarrow G\) is a function between Hilbert algebras, we define the relation \(R_f \subseteq X(G)\times X(H)\) by

$$\begin{aligned} (P,Q)\in R_f\;\text {if and only if}\; f^{-1}(P) \subseteq Q. \end{aligned}$$

Normally duals of homomorphisms are functions (e.g., in Priestley and Stone dualities). However, these functions can be seen as binary relations and, accordingly, in not so well-behaved dualities, the dual of a homomorphism tends to be a binary relation. The definition of \(R_f\) should be understood in this spirit.

The following lemma was proved in Celani (2002, Theorem 3.3).

Lemma 6

Let H and G be Hilbert algebras and \(f{:}\,H\rightarrow G\) a function such that \(f(1) = 1\) and \(f(a\rightarrow b)\le f(a)\rightarrow f(b)\) for every \(a,b\in H\). Then the following statements are equivalent:

  1. (1)

    f is a homomorphism.

  2. (2)

    If \((P,Q)\in R_f\), then there is \(F\in X(H)\) such that \(P\subseteq F\) and \(f^{-1}(F) = Q\).

If H is a Hilbert algebra and \(a\in H\), we define

$$\begin{aligned} \varphi (a): = \left\{ P\in X(H){:}\,a\in P\right\} . \end{aligned}$$
(1)

Let X and Y be sets and let \(R\subseteq X\times Y\) be a binary relation. For every \(x\in X\), we define \(R(x): =\{y\in Y{:}\,(x,y)\in R\}\).

Let \(f{:}\,H\rightarrow G\) an homomorphism in \(\mathsf {Hil}\), \(P\in X(G)\) and \(a\in H\). Cabrer et al. (2009, Lemma 3.3) it was proved that \(f(a)\in P\) if and only if for all \(Q\in X(G)\), if \((P,Q) \in R_f\) then \(a\in Q\). The previous property can be written in the following way:

$$\begin{aligned} f(a) \in P\;\text {if and only if}\; R_f(P) \subseteq \varphi (a). \end{aligned}$$
(2)

We now recall some definitions and results from Cabrer et al. (2009) and Celani and Montangie (2012) and fix some notation.

Let us consider a poset \(\left\langle X,\le \right\rangle \). For each \(Y \subseteq X\), the upset generated by Y is defined by \([Y) = \{x\in X{:}\,\;\text {there is}\;y\in Y\,\text {such that}\;y\le x\}\). The downset generated by Y is dually defined. If \(Y = \{y\}\), then we will write [y) and (y] instead of \([\{y\})\) and \((\{y\}]\), respectively. We also define \(Y^{c}:= \{x\in X{:}\,x\notin Y\}\).

Remark 2

Let \(\left\langle X,\le \right\rangle \) be a poset. Write \(X^{+}\) for the set of upsets of \(\left\langle X,\le \right\rangle \). Define on \(X^{+}\) the binary operation \(\Rightarrow \) by

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

Then \(X^{+}\) is a complete Heyting algebra.

Let \((X,\tau )\) be a topological space. An arbitrary non-empty subset Y of X is said to be irreducible if for any closed subsets Z and W such that \(Y\subseteq Z \cup W\) we have that \(Y \subseteq Z\) or \(Y \subseteq W\). We say that \((X,\tau )\) is sober if for every irreducible closed set Y there exists a unique \(x\in X\) such that \(Y = \overline{\{x\}}\), where \(\overline{\{x\}}\) denotes the closure of \(\{x\}\). A subset of X is saturated if it is an intersection of open sets. The saturation of a subset Y of X is defined as \(\mathrm {sat}(Y):= \bigcap \{U\in \tau {:}\,Y\subseteq U\}\). Recall that the specialization order of \((X,\tau )\) is defined by \(x\preceq y\) if and only if \(x \in \overline{\{y\}}\). The relation \(\preceq \) is reflexive and transitive, i.e., a quasi-order. The relation \(\preceq \) is a partial order if \((X,\tau )\) is \(T_0\). The dual quasi-order order of \(\preceq \) will be denoted by \(\preceq _{d}\). Hence,

$$\begin{aligned} x\preceq _{d}y\;\text {if and only if}\; y\in \overline{\{x\}}. \end{aligned}$$

Remark 3

Let \((X,\tau )\) be a topological space which is \(T_0\), and consider the order \(\preceq _{d}\). Let \(x\in X\) and \(Y\subseteq X\). Then \(\overline{\{x\}}= [x)\) and \(\mathrm {sat}(Y) = (Y]\), where [x) is the upset generated by \(\{x\}\) with respect to the partial order \(\preceq _{d}\) and (Y] is the downset generated by Y with respect to the partial order \(\preceq _{d}\).

For the following definition see Celani and Montangie (2012).

Definition 2

A Hilbert space, or H-space for short, is a structure \((X,\tau ,{\kappa })\) where \((X,\tau )\) is a topological space, \({\kappa }\) is a family of subsets of X and the following conditions are satisfied:

  1. (H1)

    \({\kappa }\) is a base of open and compact subsets for the topology \(\tau \) on X.

  2. (H2)

    For every \(U, V \in {\kappa }\), \(\mathrm {sat}(U \cap V^{c}) \in {\kappa }\).

  3. (H3)

    \((X, \tau )\) is sober.

In what follows, if \((X,\tau ,{\kappa })\) is an H-space, we simply write \((X,{\kappa })\).

Remark 4

  1. 1.

    A sober topological space is \(T_0\).

  2. 2.

    Viewing any topological space as a poset, with the order \(\preceq _{d}\), condition \(\mathrm {(H2)}\) of Definition 2 can be rewritten as: for every \(U,V\in {\kappa }\), \((U\cap V^{c}] \in {\kappa }\).

Let X and Y be sets and let \(R\subseteq X\times Y\) be a binary relation. If \(U\subseteq Y\), then we define \(R^{-1}(U): =\{x\in X{:}\,R(x)\cap U \ne \emptyset \}\). Let XY and Z be sets, \(R\subseteq X\times Y\) and \(S\subseteq Y\times Z\). Then the relational product (or composition) of R and S is defined as follows:

$$\begin{aligned}&R\circ S: = \left\{ (x,z){:}\,\text {there is}\; y\in Y\;\text {such that}\right. \nonumber \\&\left. \quad (x,y) \in R\;\text {and}\;(y,z)\in S\right\} . \end{aligned}$$
(4)

Definition 3

Let \(\mathbf {X}_1 = (X_1,{\kappa }_1)\) and \(\mathbf {X}_2 = (X_2,{\kappa }_2)\) be two H-spaces. Let us consider a relation \(R\subseteq X_1 \times X_2\). We say that R is an H-relation from \(\mathbf {X}_1\) into \(\mathbf {X}_2\) if it satisfies the following properties:

  1. (HR1)

    \(R^{-1}(U) \in {\kappa }_1\), for every \(U \in {\kappa }_2\).

  2. (HR2)

    R(x) is a closed subset of \(\mathbf {X}_2\), for all \(x\in X_1\).

We say that R is an H-functional relation if it satisfies the following additional condition:

\(\mathrm {(HF)}\) :

If \((x, y)\in R\), then there is \(z\in X_1\) such that \(z\in \overline{\{x\}}\) and \(R(z) = \overline{\{y\}}\).

Remark 5

Condition \(\mathrm {(HF)}\) from Definition 3 can also be given as follows: if \((x, y)\in R\) then there exists \(z\in X_1\) such that \(x\preceq _{d}z\) and \(R(z) = [y)\).

If H is a Hilbert algebra, then \(\mathbf {X}(H) = (X(H), {\kappa }_H)\) is an H-space, where \({\kappa }_H =\{\varphi (a)^{c}{:}\,a\in H\}\). If f is a homomorphism of Hilbert algebras then \(R_f\) is an H-functional relation. Write \(\mathsf {HS}\) for the category whose objects are Hilbert spaces and whose morphisms are H-functional relations, where the composition of two H-relations is defined as in (4). Then the assignment \(H\mapsto \mathbf {X}(H)\) can be extended to a functor \(\mathbf {X}{:}\,\mathsf {Hil}\rightarrow \mathsf {HS}\).

Let \((X,{\kappa })\) be an H-space. Define \(D(X) =\{U\subseteq X{:}\,U^{c}\in {\kappa }\}\). Then \(D(X) \subseteq X^{+}\). It follows from Definition 2 and Remark 4 that D(X) is closed under the operation \(\Rightarrow \) given in (3) of Remark 2. Since \(X^{+}\) is a Heyting algebra then \(\mathbf {D}(X) = (D(X), \Rightarrow , X)\) is a Hilbert algebra. If R is an H-functional relation from \((X_1, {\kappa }_1)\) into \((X_2, {\kappa }_2)\), then the map \(h_R\) from \(\mathbf {D}(X_2)\) into \(\mathbf {D}(X_1)\) given by \(h_R(U) = \{x\in X_1{:}\,R(x)\subseteq U\}\) is a homomorphism of Hilbert algebras. Then the assignment \(X\mapsto \mathbf {D}(X)\) can be extended to a functor \(\mathbf {D}{:}\,\mathsf {HS}\rightarrow \mathsf {Hil}\).

If \(H\in \mathsf {Hil}\), the map \(\varphi {:}\,H \rightarrow \mathbf {D}(\mathbf {X}(H))\) defined as in (1) is an isomorphism in \(\mathsf {Hil}\). If \((X,{\kappa })\) is an H-space, then the map \(\epsilon _{X}{:}\,X\rightarrow \mathbf {X}(\mathbf {D}(X))\) given by \(\epsilon _{X}(x) =\{U\in D(X){:}\,x\in U\}\) is an order-isomorphism and a homeomorphism between the topological spaces X and \(\mathbf {X}(\mathbf {D}(X))\) (Cabrer et al. 2009, Theorem 2.2). If there is no ambiguity, we will write \(\epsilon \) in place of \(\epsilon _{X}\). Moreover, the relation \(\epsilon ^{*}\subseteq X\times X(D(X))\) given by \((x,P)\in \epsilon ^{*}\) if and only if \(\epsilon (x)\subseteq P\) is an H-functional relation which is an isomorphism in \(\mathsf {HS}\).

The following theorem can be found in Celani and Montangie (2012) (see also Cabrer et al. 2009).

Theorem 7

The contravariant functors \(\mathbf {X}\) and \(\mathbf {D}\) define a dual equivalence between \(\mathsf {Hil}\) and \(\mathsf {HS}\) with natural equivalences \(\epsilon ^{*}\) and \(\varphi \).

3 An adjunction between \(\mathsf {Hil}\) and \(\mathsf {IS}\)

In this section, we build up a functor from the algebraic category of Hilbert algebras to the algebraic category of implicative semilattices. This provides an explicit construction for the left adjoint for the forgetful functor from the category of implicative semilattices to that of Hilbert algebras. Finally, we establish the link between our result and the results studied in Celani and Jansana (2012) (in particular, with item (1) of Celani and Jansana 2012, Proposition 7.9).

We start with some preliminary definitions and results.

Let \(\langle H,\le \rangle \) be a poset. If any two elements \(a,b \in H \) have a greatest lower bound \(a\wedge b\), then the algebra \((H,\wedge )\) is called meet semilattice. The algebra \((H,\wedge )\) is said to be bounded if it has a greatest element, which will be denoted by 1; in this case we write \((H,\wedge ,1)\). Throughout this paper, we just write semilattice in place of meet semilattice.

Definition 4

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

In the literature, implicative semilattices are known also as Brouwerian semilattices. Every implicative semilattice has a greatest element, denoted by 1. In this paper, we take this element in the language of the algebras. It is part of the folklore the fact that the variety of implicative semilattices is the variety generated by the \(\{1,\wedge ,\rightarrow \}\)-reduct of Heyting algebras. For more details about implicative semilattices see Curry (1963) and Nemitz (1965).

We write \(\mathsf {IS}\) for the category whose objects are implicative semilattices and whose morphisms are functions \(f{:}\,H\rightarrow G\) such that \(f(1) = 1\) and \(f(a\wedge b) = f(a) \wedge f(b)\) for every \(a,b \in H\).

3.1 From \(\mathsf {IS}\) to \(\mathsf {Hil}\)

Let \(f{:}\,H\rightarrow G\) be a morphism in \(\mathsf {Hil}\). It follows from Theorem 7 that the following diagram commutes:

Let \(g = \mathbf {D}(\mathbf {X}(f))\). The elements of \(\mathbf {D}(\mathbf {X}(H))\) take the form \(\varphi (a)\) for \(a\in H\). Thus, the commutativity of the previous diagram is equivalent to the following equality, for every \(a\in H\):

$$\begin{aligned} \varphi (f(a)) = g(\varphi (a)). \end{aligned}$$
(5)

Also note that it follows from (2) of Sect. 2 that

$$\begin{aligned} g(\varphi (a)) = \left\{ P\in \mathbf {X}(G){:}\,R_{f}(P)\subseteq \varphi (a)\right\} . \end{aligned}$$

For every \(H \in \mathsf {Hil}\), we have that \(\varphi [H] = \mathbf {D}(\mathbf {X}(H)) \subseteq \mathbf {X}(H)^{+}\).

Lemma 8

The homomorphism of Hilbert algebras g can be extended to a homomorphism of implicative semilattices \({\hat{g}}{:}\,\mathbf {X}(H)^{+} \rightarrow \mathbf {X}(G)^{+}\).

Proof

Let \({\hat{g}}{:}\,\mathbf {X}(H)^{+} \rightarrow \mathbf {X}(G)^{+}\) be given by

$$\begin{aligned} {\hat{g}}(U) = \{P\in \mathbf {X}(G){:}\,R_{f}(P)\subseteq U\}. \end{aligned}$$

In order to show the good definition of \({\hat{g}}\), let \(U \in \mathbf {X}(H)^{+}\) and \(P, Q \in \mathbf {X}(G)\) such that \(P\subseteq Q\) and \(P \in {\hat{g}}(U)\), i.e., \(R_{f}(P)\subseteq U\). Let \(Z\in R_{f}(Q)\), so \(f^{-1}(Q)\subseteq Z\). Since \(f^{-1}(P) \subseteq f^{-1}(Q)\) then \(f^{-1}(P)\subseteq Z\), so \(Z\in R_{f}(P)\subseteq U\). Thus, \(Z\in U\). Hence, \(R_{f}(Q)\subseteq U\), i.e., \(Q\in {\hat{g}}(U)\). In consequence, \({\hat{g}}\) is a well defined map. It is immediate that \({\hat{g}}(\mathbf {X}(H)) = \mathbf {X}(G)\) and \({\hat{g}}(U\cap V) = {\hat{g}}(U) \cap {\hat{g}}(V)\) for every \(U,V\in \mathbf {X}(H)^{+}\). In particular, \({\hat{g}}(U\Rightarrow V) \subseteq {\hat{g}}(U) \Rightarrow {\hat{g}}(V)\) for every \(U,V\in \mathbf {X}(H)^{+}\).

Let \(U,V\in \mathbf {X}(H)^{+}\). In order to prove that \({\hat{g}}(U) \Rightarrow {\hat{g}}(V) \subseteq {\hat{g}}(U\Rightarrow V)\), suppose that \(P\notin {\hat{g}}(U \Rightarrow V)\), i.e., \(R_{f}(P)\nsubseteq U\Rightarrow V\). Then there exists \(Q\in \mathbf {X}(H)\) such that \(f^{-1}(P)\subseteq Q\) and \(Q\notin U\Rightarrow V\). Hence, there exists \(Z\in \mathbf {X}(H)\) such that \(Q\subseteq Z\) and \(Z\in U\cap V^c\). Since \(f^{-1}(P) \subseteq Q\), then it follows from Lemma 6 that there exists \(W\in \mathbf {X}(G)\) such that \(P\subseteq W\) and \(f^{-1}(W) = Z\). Thus, \(R_{f}(W)\subseteq U\). In order to show it, let \(T\in R_{f}(W)\). Hence, \(Z\subseteq T\). Since \(Z\in U\) and \(U\in \mathbf {X}(H)^{+}\), then \(T\in U\). So, we have proved that \(R_{f}(W)\subseteq U\). Besides \(R_{f}(W)\nsubseteq V\) because \(Z\in R_{f}(W)\) and \(Z\notin V\). Summarizing, \(P\subseteq W\), \(R_{f}(W)\subseteq U\) and \(R_{f}(W)\nsubseteq V\), so \(P\notin {\hat{g}}(U) \Rightarrow {\hat{g}}(V)\). Therefore, \({\hat{g}}(U \Rightarrow V) = {\hat{g}}(U) \Rightarrow {\hat{g}}(V)\). \(\square \)

Remark 6

In general, the map \({\hat{g}}\) of Lemma 8 is not necessarily a Heyting homomorphism. In order to prove it, consider the following two posets:

Endow these posets with the Hilbert algebra structures induced by the order; i.e., the implication is given by \(x \rightarrow y = 1\) if \(x \le y\) and \(x \rightarrow y = y\) if \(x \nleq y\). Define \(f{:}\,H \rightarrow G\) by \(f(x) = a\), \(f(y) = b\) and \(f(1) = 1\). Straightforward computations show that \(f \in \mathsf {Hil}\) and that \({\hat{f}}\) does not preserve joins.

It is worth mentioning that \(\varphi [H] = \mathbf {D}(\mathbf {X}(H)) \subseteq \mathbf {X}(H)^{+}\), as defined before Lemma 8, is the logic-based canonical extension of the Hilbert algebra H, as defined in Gehrke et al. (2010). This fact follows from González (2018, Corollary 6.26).

If S is a subset of an implicative semilattice, we write \(\langle S \rangle _{\mathsf {IS}}\) for the implicative semilattice generated by S. Let \(H\in \mathsf {Hil}\). Since \(\varphi [H]\) is a subset of the implicative semilattice \(\mathbf {X}(H)^+\), then we define the following implicative semilattice of \(X(H)^+\):

$$\begin{aligned} H^{\mathsf {IS}}: = \langle \varphi [H] \rangle _{\mathsf {IS}}. \end{aligned}$$

Let \(H\in \mathsf {Hil}\). It is interesting to note that the immersion of H into \(\mathbf {X}(H)^+\) induced by \(\varphi \) does not necessarily preserve existing infima; however, it does preserve existing suprema. See for instance Chajda (2002, Theorem 3.2). Since \(\mathbf {X}(H)^+\) is the logic-based canonical extension of H as defined in Gehrke et al. (2010), then the fact that \(\varphi (a\vee b) = \varphi (a) \cup \varphi (b)\) whenever \(a \vee b\) exists can be also deduced from Gehrke et al. (2013, Proposition 6.10).

The following remark is a well-known fact from universal algebra (Burris and Sankappanavar 1981).

Remark 7

Let A and B be algebras of the same type and \(X\subseteq A\) with \(X\ne \emptyset \). Let \(f{:}\,A\rightarrow B\) be a homomorphism. Write \(\mathrm {Sg}^{A}(X)\) for the subalgebra of A generated by X and \(\mathrm {Sg}^{B}(f(X))\) for the subalgebra of B generated by f(X). We have that \(f(\mathrm {Sg}^{A}(X))= \mathrm {Sg}^{B}(f(X))\).

Lemma 9

The homomorphism of implicative semilattices \({\hat{g}}\) defined in Lemma 8 satisfies \({\hat{g}}(H^{\mathsf {IS}}) \subseteq G^{\mathsf {IS}}\).

Proof

It follows from Lemma 8, Remark 7 and the equality \(g(\varphi (a)) = \varphi (f(a))\) given in (5). \(\square \)

Let \(f{:}\,H \rightarrow G\) be a morphism in \(\mathsf {Hil}\). It follows from Lemmas 8 and 9 that the map \(f^{\mathsf {IS}}{:}\,H^{\mathsf {IS}}\rightarrow G^{\mathsf {IS}}\) given by

$$\begin{aligned} f^{\mathsf {IS}}(U) = \left\{ P\in \mathbf {X}(G){:}\,R_{f}(P)\subseteq U\right\} \end{aligned}$$

is a morphism in \(\mathsf {IS}\). Let \(\mathsf {Id}\) be an identity morphism in \(\mathsf {Hil}\). It is immediate that \(\mathsf {Id}^{\mathsf {IS}}\) is an identity in \(\mathsf {IS}\). Let \(f{:}\,H\rightarrow G\) and \(g{:}\,G \rightarrow K\) be morphisms in \(\mathsf {Hil}\). It follows from Cabrer et al. (2009, Theorem 3.3) that \(R_{g\circ f} = R_{g} \circ R_{f}\). Hence, straightforward computations based in the above-mentioned equality shows that

$$\begin{aligned} (g \circ f)^{\mathsf {IS}} = g^{\mathsf {IS}}\circ f^{\mathsf {IS}}. \end{aligned}$$

Therefore, we obtain the following proposition.

Proposition 1

The assignments \(H\mapsto H^{\mathsf {IS}}\) and \(f\mapsto f^{\mathsf {IS}}\) define a functor \((\ )^{\mathsf {IS}}{:}\,\mathsf {Hil}\rightarrow \mathsf {IS}\).

In what follows, we write \(\mathrm {U}\) for the forgetful functor from \(\mathsf {IS}\) to \(\mathsf {Hil}\).

3.2 Adjunction

Now we prove that the functor \((\ )^{\mathsf {IS}}{:}\,\mathsf {Hil}\rightarrow \mathsf {IS}\) is left adjoint of \(\mathrm {U}\).

Recall that if \(H\in \mathsf {IS}\), a subset \(F\subseteq H\) is said to be a filter if it satisfies the following conditions:

  1. (1)

    \(1 \in F\),

  2. (2)

    \(a\wedge b \in F\) whenever \(a,b \in F\),

  3. (3)

    F is an upset.

We can also define the concept of implicative (and irreducible) filter for the case of implicative semilattices. It is part of the folklore that if \(H\in \mathsf {IS}\) then the set of implicative filters of H is equal to the set of filters of H. If \(H\in \mathsf {IS}\), we also write X(H) for the set of irreducible filters of H.

Remark 8

Let \(H\in \mathsf {IS}\). We write \(H^{\mathsf {IS}}\) in place of \((\mathrm {U}(H))^{\mathsf {IS}}\). For every \(a\in H\), we also write \(\varphi (a)\) for the set \(\{P\in X(H){:}\,a\in P\}\).

Let \(H\in \mathsf {Hil}\). Consider the injective morphism of Hilbert algebras \(\psi {:}\,H\rightarrow \mathrm {U}(H^{\mathsf {IS}})\) given by \(\psi (a) = \varphi (a)\).

Proposition 2

Let \(G\in \mathsf {IS}\) and \(f{:}\,H\rightarrow \mathrm {U}(G)\in \mathsf {Hil}\). Then, there exists a unique morphism \(h{:}\,H^{\mathsf {IS}}\rightarrow G\) such that \(f = \mathrm {U}(h) \circ \psi \).

Proof

The map \(f^{\mathsf {IS}}{:}\,\ H^{\mathsf {IS}}\rightarrow G^{\mathsf {IS}}\) is a morphism in \(\mathsf {IS}\). Since \(G\in \mathsf {IS}\) then for every \(a,b\in G\), we have that \(\varphi (a\wedge b) = \varphi (a) \cap \varphi (b)\), so a reflection’s moment shows that the map \(\varphi {:}\,G\rightarrow G^{\mathsf {IS}}\) is an isomorphism in \(\mathsf {IS}\). Hence, the map \(h{:}\,H^{\mathsf {IS}}\rightarrow G\) given by \(h = \varphi ^{-1} \circ f^{\mathsf {IS}}\) is also a morphism in \(\mathsf {IS}\). Finally, it follows from (5) that \(f = \mathrm {U}(h) \circ \psi \).

\(\square \)

Let \(\mathrm {I_{Hil}}\) be the identity functor in \(\mathsf {Hil}\). It follows from (5) that \(\Psi {:}\,\mathrm {I_{Hil}}\rightarrow \mathrm {U}\circ (\ )^{\mathsf {IS}}\) is a natural transformation. Here, the family of morphism associated to the natural transformation is given by the morphisms \(\psi \).

In other words, to say that \(\Psi {:}\,\mathrm {I_{Hil}}\rightarrow \mathrm {U}\circ (\ )^{\mathsf {IS}}\) is a natural transformation is equivalent to say that if \(f{:}\,H\rightarrow G\) is a morphism in \(\mathsf {Hil}\) then the following diagram commutes:

Therefore, we get the following result.

Theorem 10

The functor \((\ )^{\mathsf {IS}}{:}\,\mathsf {Hil}\rightarrow \mathsf {IS}\) is left adjoint to \(\mathrm {U}\).

3.3 Connections with the literature

In what follows, we connect our results with those of Celani and Jansana (2012). We also make a brief remark about \(\varphi _H{:}\,H \rightarrow \mathbf {X}(H)^{+}\), viewed as the logic-based canonical extension of the Hilbert algebra H, as presented in Gehrke et al. (2010).

Fix \(H\in \mathsf {Hil}\). A pair (Ge) where G is an implicative semilattice and e is an injective morphism from H to \(\mathrm {U}(G)\) is said to be an implicative semilattice envelope of H if for every \(y\in G\) there exists a finite subset \(X\subseteq H\) such that \(y = \bigwedge e(X)\). Define the following set:

$$\begin{aligned}&\mathrm {S}(H) = \left\{ U {:}\,U = \varphi (a_1)\cap \cdots \cap \varphi (a_n)\right. \\&\left. \quad \text {for some}\; a_1,\ldots ,a_n \in H\right\} . \end{aligned}$$

Then, \(\varphi [H] \subseteq \mathrm {S}(H) \subseteq \mathbf {X}(H)^{+}\). Moreover, \(\mathrm {S}(H) \in \mathsf {IS}\) by considering the implication \(\Rightarrow \) given by (3). The pair \((\mathrm {S}(H),\eta )\) is an implicative semilattice envelope of H, where \(\eta {:}\,H \rightarrow \mathrm {U}(\mathrm {S}(H))\) is given by \(\eta (a) = \varphi (a)\) (Celani and Jansana 2012, Lemma 6.4). It follows from results of Celani and Jansana (2012) that \((\mathrm {S}(H),\eta )\) is a solution (Ge) of the following universal problem: For every \(G' \in \mathsf {IS}\) and every \(e' {:}\,H \rightarrow \mathrm {U}(G') \in \mathsf {Hil}\), there is a unique \(g{:}\,G \rightarrow G' \in \mathsf {IS}\) such that \(e' = \mathrm {U}(g) \circ e\).

It follows from Celani and Jansana (2012, Proposition 6.9) that if \(h {:}\,H \rightarrow K \in \mathsf {Hil}\) then there is a unique \({\overline{h}}{:}\,\mathrm {S}(H) \rightarrow \mathrm {S}(K)\) such that \(\eta \circ h = {\overline{h}} \circ \eta \).

The following theorem summarize some properties from Celani and Jansana (2012), which it was proved in an alternative way in the present paper (Theorem 10).

Theorem 11

There exists a functor \(\mathrm {S}{:}\,\mathsf {Hil}\rightarrow \mathsf {IS}\) that maps every \(H \in \mathsf {Hil}\) to \(\mathrm {S}(H) \in \mathsf {IS}\), and every \(h {:}\,H\rightarrow G \in \mathsf {Hil}\) to \({\overline{h}}{:}\,\mathrm {S}(H) \rightarrow \mathrm {S}(G)\in \mathsf {IS}\). The functor \(\mathrm {S}\) is left adjoint to \(\mathrm {U}\).

Let \(H\in \mathsf {Hil}\). Since \(\mathrm {S}(H) \in \mathsf {IS}\), it follows from the definition of \(H^{\mathsf {IS}}\) that \(H^{\mathsf {IS}}\) is in fact equal to \(\mathrm {S}(H)\), i.e.,

$$\begin{aligned} H^{\mathsf {IS}}= \mathrm {S}(H). \end{aligned}$$
(6)

Gehrke et al. (2010) the logic-based canonical extension of an algebra in certain classes of algebras of interest for abstract algebraic logic is presented. In particular, it is proved there that when this notion of canonicity is considered, the variety of Hilbert algebras is canonical. It can be seen that the logic-based canonical extension of a Hilbert algebra, as performed in Gehrke et al. (2010, Section 5.1) is indeed given by the embedding \(\varphi _H {:}\,H \rightarrow \mathbf {X}(H)^{+}\).

4 Relation between \(\mathsf {Hil}^{\vee }\) \((\mathsf {Hil}_{\mathsf {0}}^{\vee }\)) and \(\mathsf {gH}\) (\(\mathsf {Hey}\))

In this section, we provided a construction for the left adjoint of the forgetful functor from the algebraic category of generalized Heyting algebras (Heyting algebras) to the algebraic category of Hilbert algebras with supremum (Hilbert algebras with supremum and a minimum).

Definition 5

An algebra \((H,\vee ,\rightarrow ,1)\) of type (2, 2, 0) is a Hilbert algebra with supremum if the following conditions are satisfied:

1.:

\((H,\rightarrow ,1)\) is a Hilbert algebra.

2.:

\((H,\vee ,1)\) is a join semilattice with greatest element 1.

3.:

For every \(a,b\in H\), \(a\rightarrow b = 1\) if and only if \(a \vee b = b\).

We denote by \(\mathsf {Hil}^{\vee }\) to the category whose objects are Hilbert algebras with supremum and whose morphisms are the homomorphisms \(f{:}\,H\rightarrow G\) in \(\mathsf {Hil}\) such that \(f(a\vee b) = f(a)\vee f(b)\) for every \(a,b\in H\). For more details about Hilbert algebras with supremum, see Celani and Montangie (2012).

Definition 6

A generalized Heyting algebra (gH-algebra for short) is a lattice such that for every \(a,b\in H\) there exists the maximum of the set \(\{c\in H{:}\,a\wedge c\le b\}\), denoted by \(a\rightarrow b\).

It is known that gH-algebras have a largest element, which will be denoted by 1. We consider gH-algebras as algebras \((H,\wedge ,\vee ,\rightarrow ,1)\) of type (2, 2, 2, 0), and Heyting algebras as algebras \((H,\wedge ,\vee ,\rightarrow ,0,1)\) of type (2, 2, 2, 0, 0). We write \(\mathsf {gH}\) for the category of gH-algebras and \(\mathsf {Hey}\) for the category of Heyting algebras. For more about these classes of algebras, see Balbes and Dwinger (1974) and Monteiro (1980).

Let \(H\in \mathsf {Hil}^{\vee }\) and F an implicative filter of H. We say that F is prime if it is proper and for any \(a,b \in H\) such that \(a\vee b \in F\) we have that \(a\in F\) or \(b\in F\). It is part of the folklore that the set of prime filters of H is equal to the set of irreducible implicative filters of H.

Lemma 12

Let \(f{:}\,H\rightarrow G\) be a morphism in \(\mathsf {Hil}^{\vee }\). Then for every \(P\in \mathbf {X}(G)\) it holds that \(f^{-1}(P)\in \mathbf {X}(H)\) or \(f^{-1}(P) = H\).

Proof

It follows from Celani and Montangie (2012, Lemma 5.10). \(\square \)

Celani and Montangie (2012, Lemma 5.10) it was also proved that if \(f{:}\,H\rightarrow G\) be a morphism in \(\mathsf {Hil}^{\vee }\) then for every \(P\in \mathbf {X}(G)\) such that \(R_{f}(P) \ne \emptyset \) it holds that if UV are closed sets of \(\mathbf {X}(H)\) such that \(R_{f}(P) \subseteq U \cup V\) then \(R_{f}(P) \subseteq U\) or \(R_{f}(P)\subseteq V\). In the following lemma, we generalize the above-mentioned property.

Lemma 13

Let \(f{:}\,H\rightarrow G\) be a morphism in \(\mathsf {Hil}^{\vee }\), \(P\in \mathbf {X}(G)\) and \(U,V \in \mathbf {X}(H)^{+}\). If \(R_{f}(P)\subseteq U\cup V\) then \(R_{f}(P) \subseteq U\) or \(R_{f}(P) \subseteq V\).

Proof

Assume that \(R_{f}(P)\subseteq U\cup V\). It follows from Lemma 12 that \(f^{-1}(P) \in \mathbf {X}(H)\) or \(f^{-1}(P) = H\). Suppose that \(f^{-1}(P) = H\), i.e., \(R_{f}(P) = \emptyset \). Then \(R_{f}(P)\subseteq U\) or \(R_{f}(P)\subseteq V\). Hence, we can assume that \(f^{-1}(P) \in \mathbf {X}(H)\), i.e., \(f^{-1}(P) \in R_{f}(P)\). Since \(R_{f}(P)\subseteq U\cup V\) then \(f^{-1}(P)\in U\) or \(f^{-1}(P) \in V\). Consider that \(f^{-1}(P) \in U\) and let \(Q\in R_{f}(P)\). Thus, \(f^{-1}(P) \subseteq Q\). Since \(f^{-1}(P) \in U\) and \(U\in \mathbf {X}(H)^{+}\) then \(Q\in U\). Hence, \(R_{f}(P) \subseteq U\). The same argument proves that if \(f^{-1}(P) \in V\) then \(R_{f}(P) \subseteq V\). \(\square \)

If S is a subset of a gH-algebra, we write \(\langle S \rangle _{\mathsf {gH}}\) for the gH-algebra generated by S. Let \(H\in \mathsf {Hil}\). Since \(\varphi [H]\) is a subset of the gH-algebra \(\mathbf {X}(H)^+\) then we define the following gH-algebra of \(X(H)^+\):

$$\begin{aligned} H^{\mathsf {gH}}: = \langle \varphi [H] \rangle _{\mathsf {gH}}. \end{aligned}$$

Let \(f{:}\,H\rightarrow G\) be a morphism in \(\mathsf {Hil}^{\vee }\) and \({\hat{g}}{:}\,\mathbf {X}(H)^{+} \rightarrow \mathbf {X}(G)^{+}\) the function considered in Lemma 8. It follows from Lemma 13 that if \(U,V \in \mathbf {X}(H)^{+}\) then

$$\begin{aligned} {\hat{g}}(U\cup V) = {\hat{g}}(U) \cup {\hat{g}}(V). \end{aligned}$$

Hence, by Lemma 8, we have that \({\hat{g}}{:}\,\mathbf {X}(H)^{+} \rightarrow \mathbf {X}(G)^{+}\) is a morphism in \(\mathsf {gH}\). By the same argument of Lemma 9, we have that \({\hat{g}}(H^{\mathsf {gH}})\subseteq G^{\mathsf {gH}}\), so \({\hat{g}}\) can be restricted to a morphism \(f^{\mathsf {gH}}{:}\,H^{\mathsf {gH}} \rightarrow G^{\mathsf {gH}}\) in \(\mathsf {gH}\).

The following result is similar to that given in Proposition 1.

Proposition 3

The assignments \(H\mapsto H^{\mathsf {gH}}\) and \(f\mapsto f^{\mathsf {gH}}\) define a functor \((\ )^{\mathsf {gH}}{:}\,\mathsf {Hil}^{\vee }\rightarrow \mathsf {gH}\).

Write also \(\mathrm {U}\) for the forgetful functor from \(\mathsf {gH}\) to \(\mathsf {Hil}^{\vee }\). As in the case of Theorem 10, we can show the following result.

Theorem 14

The functor \((\ )^{\mathsf {gH}}{:}\,\mathsf {Hil}^{\vee }\rightarrow \mathsf {gH}\) is left adjoint to \(\mathrm {U}\).

In the following proposition, we give an easy description for \(H^{\mathsf {gH}}\) when H is a finite algebra.

Proposition 4

Let \(H\in \mathsf {Hil}^{\vee }\) be a finite algebra. Then \(H^{\mathsf {gH}} = \mathbf {X}(H)^{+}\).

Proof

By definition, we have that \(H^{\mathsf {gH}}\subseteq \mathbf {X}(H)^{+}\). In order to prove the converse inclusion, let \(U\in \mathbf {X}(H)^+\). Since H is finite then \(\emptyset \in H^{\mathsf {gH}}\), so we can assume that \(U\ne \emptyset \). Since U is finite there exist \(P_1,\ldots ,P_n\in \mathbf {X}(H)\) such that \(U = \{P_1,\ldots ,P_n\}\). Hence, \(U = \bigcup _{i=1}^{n} [P_i)\). Note that if \(P\in \mathbf {X}(H)\) then \([P) = \bigcap _{a\in P} \varphi (a)\) (it is a finite union) and \(\varphi (1) = \mathbf {X}(H)\). Thus, \(U = \bigcap _{i=1}^{m} U_i\), where for every \(i=1,\ldots ,m\) the set \(U_i\) takes the form \(\varphi (a_{1i})\cap \cdots \cap \varphi (a_{mi})\). Then \(U\in H^{\mathsf {gH}}\). Therefore, \(H^{\mathsf {gH}} = \mathbf {X}(H)^{+}\). \(\square \)

For \(H\in \mathsf {Hil}^{\vee }\), we can give the following description of \(H^{\mathsf {gH}}\), where we see \(H^{\mathsf {gH}}\) as an implicative semilattice.

Proposition 5

Let \(H\in \mathsf {Hil}^{\vee }\). Then \(\mathrm {S}(H) = H^{\mathsf {gH}}\).

Proof

By (6) of the end of Sect. 3, we only need to prove that if \(U, V \in \mathrm {S}(H)\) then \(U\cup V \in \mathrm {S}(H)\). Let \(U, V \in \mathrm {S}(H)\). Then there exist \(a_1,\ldots ,a_n \in H\) and \(b_1,\ldots ,b_m\in H\) such that \(U = \varphi (a_1) \cap \cdots \cap \varphi (a_n)\) and \(V = \varphi (b_1) \cap \cdots \cap \varphi (b_m)\). Since \(\varphi (1) = \mathbf {X}(H)\), we can assume that \(n = m\). Hence, \(U \cup V = \bigcap _{i,j=1}^{n} (\varphi (a_i)\cup \varphi (b_j)) = \bigcap _{i,j=1}^{n} \varphi (a_i \vee b_j)\). Therefore, \(U\cup V \in \mathrm {S}(H)\). \(\square \)

Let \(\mathsf {Hil}_{\mathsf {0}}^{\vee }\) be the category whose objects are algebras \((H,\vee ,\rightarrow ,0,1)\) of type (2, 2, 0, 0) such that \((H,\vee ,\rightarrow ,1) \in \mathsf {Hil}^{\vee }\) and 0 satisfies that \(0\le x\) for every \(x\in H\). The morphisms are the homomorphisms f of \(\mathsf {Hil}^{\vee }\) such that \(f(0) = 0\). Also write \(\mathrm {U}\) for the forgetful functor from \(\mathsf {Hey}\) to \(\mathsf {Hil}^{\vee }\). If \(H\in \mathsf {Hey}\), we define \(H^{\mathsf {Hey}}\) as the Heyting subalgebra of \(\mathbf {X}(H)^+\) generated by \(\varphi [H]\), and if \(f{:}\,H\rightarrow G\) is a morphism in \(\mathsf {Hey}\) we can define a morphism \(f^{\mathsf {Hey}}{:}\,H^{\mathsf {Hey}} \rightarrow G^{\mathsf {Hey}}\) in \(\mathsf {Hey}\) similarly to the case of gH-algebras. We also write \(\mathrm {U}\) for the forgetful functor from \(\mathsf {Hey}\) to \(\mathsf {Hil}_{\mathsf {0}}^{\vee }\)

Corollary 15

The functor \((\ )^{\mathsf {Hey}}{:}\,\mathsf {Hil}_{\mathsf {0}}^{\vee }\rightarrow \mathsf {Hey}\) is left adjoint to \(\mathrm {U}\).

5 Final remarks

In this final section, we define a functor from \(\mathsf {Hil}\) to \(\mathsf {gH}\). As usual, we start with some definitions and preliminary results.

The proof of the following lemma is similar to the proof of Celani (2002, Theorem 3.3).

Lemma 16

Let \(f{:}\,H\rightarrow G\in \mathsf {Hil}\), \(I\in \mathsf {Fil}(G)\) and \(J\in \mathbf {X}(H)\) be such that \(f^{-1}(I)\subseteq J\). Then there exists \(K\in \mathbf {X}(H)\) such that \(I\subseteq K\) and \(f^{-1}(K) = J\).

Proof

Since \(J\in \mathbf {X}(H)\), we have that

$$\begin{aligned} (f(J^{c})] = \left\{ b\in G{:}\,b\le f(a)\;\text {for some}\;a\in J^c\right\} \end{aligned}$$

is an order-ideal of G (see Celani 2002, Theorem 2.3). Let us see that

$$\begin{aligned} (f(J^{c})] \cap F(I\cup f(J)) = \emptyset . \end{aligned}$$

Suppose that \((f(J^{c})] \cap F(I\cup f(J)) \ne \emptyset \). Then, there are \(x \in H\), \(j \notin J\), \(j_1, \ldots , j_m \in J\) and \(i_1, \ldots , i_n \in I\) such that \(x \le f(j)\) and

$$\begin{aligned}&i_1 \rightarrow (i_2 \rightarrow \cdots (i_n \rightarrow ( f(j_1) \rightarrow (f(j_2) \rightarrow \cdots \\&\quad (f(j_m) \rightarrow x) \ldots ) = 1. \end{aligned}$$

Note that elements can be always ordered in this way, since in any Hilbert algebra the identity \(a \rightarrow (b \rightarrow c) = b \rightarrow (a \rightarrow c)\) holds. Since \(1, i_1, \ldots , i_n\) are in I, \(f(j_1) \rightarrow (f(j_2) \rightarrow \cdots (f(j_m) \rightarrow x) \ldots ) \in I\). Since \(x \le f(j)\) then

$$\begin{aligned}&f(j_1) \rightarrow (f(j_2) \rightarrow \cdots (f(j_m) \rightarrow x) \ldots ) \le \\&f(j_1) \rightarrow (f(j_2) \rightarrow \cdots (f(j_m) \rightarrow f(j)) \ldots ) \\&\quad = f\left( j_1 \rightarrow (j_2 \rightarrow \cdots (j_m \rightarrow j) \ldots )\right) . \end{aligned}$$

Since I is an upset then \(f(j_1 \rightarrow (j_2 \rightarrow \cdots (j_m \rightarrow j) \ldots )) \in I\), what implies that \(j_1 \rightarrow (j_2 \rightarrow \cdots (j_m \rightarrow j) \ldots ) \in f^{-1}(I) \subseteq J\). Hence, \(j \in J\), which is a contradiction. In consequence, \((f(J^{c})] \cap F(I\cup f(J)) = \emptyset \).

By Lemma 2, there exists \(K \in \mathbf {X}(G)\) such that \(F(I\cup f(J))\subseteq K\) and \((f(J^{c})] \cap K = \emptyset \). Thus, \(I\subseteq K\) and \(f^{-1}(K) = J\). \(\square \)

Let \(H\in \mathsf {Hil}\). We define the following set:

$$\begin{aligned}&X^{\vee }(H) = \left\{ F\in \mathsf {Fil}(H){:}\,F = \bigcap \textit{X}_0,\;\text {for some finite} \right. \nonumber \\&\left. \quad \textit{X}_0\subseteq \mathbf {X}(H)\right\} . \end{aligned}$$
(7)

It is known that if F is a proper implicative filter of H then F is the intersection of all irreducible filters of H such that contain F (it is an immediate consequence of Corollary 3). In particular, note that if H is finite then \(F \in X^{\vee }(H)\) if and only if F is a proper implicative filter of H.

Corollary 17

Let \(f{:}\,H\rightarrow G\in \mathsf {Hil}\), \(I \in X^{\vee }(H)\) and \(J\in X^{\vee }(G)\) be such that \(f^{-1}(I) \subseteq J\). Then there exists \(K\in X^{\vee }(H)\) such that \(I \subseteq K\) and \(f^{-1}(K) = J\).

Proof

Let \(I \in X^{\vee }(H)\) and \(J\in X^{\vee }(G)\) be such that \(f^{-1}(I) \subseteq J\). Then there exist \(Q_1,\ldots ,Q_n \in \mathbf {X}(G)\) such that \(J = Q_1\cap \cdots \cap Q_n\), so \(f^{-1}(I)\subseteq Q_i\) for every \(i=1,\ldots ,n\). By Lemma 16, we have that there exist \(K_1,\ldots ,K_n\in \mathbf {X}(H)\) such that \(I\subseteq K_i\) and \(f^{-1}(K_i) = Q_i\) for every \(i=1,\ldots ,n\). Let \(K = \mathrm {K}_{1} \cap \cdots \cap K_n\). Thus, \(K\in X^{\vee }(H)\), \(I\subseteq K\) and \(f^{-1}(K) = J\). \(\square \)

Let \(H\in \mathsf {Hil}\). We define the function \(\Phi {:}\,H \rightarrow (X^{\vee }(H))^{+}\) by

$$\begin{aligned} \Phi (a) = \left\{ F\in X^{\vee }(H){:}\,a\in F\right\} . \end{aligned}$$

Lemma 18

Let \(H\in \mathsf {Hil}\). The function \(\Phi \) defined above is an injective morphism in \(\mathsf {Hil}\). Moreover, if \(H^{\dag }\) is the gH-algebra of \((X^{\vee }(H))^{+}\) generated by \(\Phi (H)\), then \(\Phi \) can be also considered as a map from H to \(H^{\dag }\).

Proof

It is immediate that if \(a\in H\) then \(\Phi (a)\) is an upset of \(X^{\vee }(H)\) and that \(\Phi (1) = X^{\vee }(H)\). The equality \(\Phi (a\rightarrow b) = \Phi (a) \Rightarrow \Phi (b)\) follows from Corollary 3. Finally, Corollary 4 implies the injectivity of \(\Phi \). \(\square \)

Let \(f{:}\,H\rightarrow G\in \mathsf {Hil}\). We define \(R_{f}^{\vee }\subseteq X^{\vee }(G) \times X^{\vee }(H)\) by

$$\begin{aligned} (I,J) \in R_{f}^{\vee }\; \text {if and only if}\; f^{-1}(I)\subseteq J. \end{aligned}$$

Lemma 19

Let \(f{:}\,H\rightarrow G\in \mathsf {Hil}\). Then the following holds:

  1. (a)

    For every \(a\in H\), \(\Phi (f(a)) = \{F\in X^{\vee }(G){:}\,R_{f}^{\vee }(F)\subseteq \Phi (a)\}\).

  2. (b)

    The function \(g{:}\,(X^{\vee }(H))^{+} \rightarrow (X^{\vee }(G))^{+}\) given by

    $$\begin{aligned} g(U) = \left\{ F\in X^{\vee }(G){:}\,R_{f}^{\vee }(F) \subseteq U\right\} \end{aligned}$$

    is a morphism in \(\mathsf {gH}\).

  3. (c)

    For every \(a\in H\), \(g(\Phi (a)) = \Phi (f(a))\). In particular, \(f(H^{\dag })\subseteq G^{\dag }\) and the function \(f^{\dag }{:}\,H^{\dag } \rightarrow G^{\dag }\) given by \(f^{\dag }(U) = g(U)\) is a morphism in \(\mathsf {gH}\).

Proof

First we will prove a). Let \(a\in H\). It is immediate that \(\Phi (f(a)) \subseteq \{F\in X^{\vee }(G){:}\,R_{f}^{\vee }(F)\subseteq \Phi (a)\}\). Conversely, let \(F\in X^{\vee }(G)\) such that \(R_{f}^{\vee }(F) \subseteq \Phi (a)\). Suppose that \(F\notin \Phi (f(a))\), i.e., \(a \notin f^{-1}(F)\). Since \(f^{-1}(F)\) is an implicative filter of H then it follows from Corollary 5 that there exists \(P\in \mathbf {X}(H)\) such that \(f^{-1}(F)\subseteq P\) and \(a\notin P\). Then, \(P\in R_{f}^{\vee }(F) \subseteq \Phi (a)\). Hence, we deduce that \(a\in P\), which is a contradiction. Thus, we have proved that \(\{F\in X^{\vee }(G){:}\,R_{f}^{\vee }(F)\subseteq \Phi (a)\} \subseteq \Phi (f(a))\).

Now we will prove b). Let \(U,V\in (X^{\vee }(H))^{+}\). It is immediate that \(g(U\cap V) = g(U)\cap g(V)\) and \(g(X^{\vee }(H)) = X^{\vee }(G)\). The equality \(g(U\Rightarrow V) = g(U) \Rightarrow g(V)\) can be proved as Lemma 8 but using Corollary 17.

Finally, we will prove that \(g(U\cup V) = g(U) \cup g(V)\) for every \(U,V\in (X^{\vee }(H))^{+}\). It is enough to prove that if \(F\in X^{\vee }(G)\) and \(R_{f}^{\vee }(F)\subseteq U\cup V\) then \(R_{f}^{\vee }(F) \subseteq U\) or \(R_{f}^{\vee }(F) \subseteq V\). Let \(R_{f}^{\vee }(F)\subseteq U\cup V\). Suppose that \(R_{f}^{\vee }(F)\nsubseteq U\) and \(R_{f}^{\vee }(F)\nsubseteq V\). Then there exist \(J,K \in X^{\vee }(H)\) such that \(f^{-1}(F) \subseteq J\), \(f^{-1}(F)\subseteq K\), \(J\notin U\) and \(K\notin V\). In particular, \(f^{-1}(F) \subseteq J \cap K\). Since \(J\cap K\in X^{\vee }(H)\) then \(J\cap K \in R_{f}^{\vee }(F) \subseteq U\cup V\), so \(J\cap K \in U\) or \(J\cap K \in V\). Since \(J\cap K \subseteq J\), \(J\cap K \subseteq K\) and \(U,V \in (X^{\vee }(H))^{+}\) then \(J\in U\) or \(K\in V\), which is a contradiction.

The item (c) follow from items (a) and (b). \(\square \)

The following result follows from Lemma 18.

Proposition 6

The assignments \(H\mapsto H^{\dag }\) and \(f\mapsto f^{\dag }\) define a functor \((\ )^{\dag }{:}\,\mathsf {Hil}\rightarrow \mathsf {gH}\).

A straightforward computation shows that if H is a finite Hilbert algebra then

$$\begin{aligned} H^{\dag } = (X^{\vee }(H))^{+}. \end{aligned}$$

We conclude this paper stating the following open problem. Is it possible to adapt the constructions of this paper in order to get an explicit description of the (generalized) Heyting algebra freely generated by a Hilbert algebra?