INTUITIONISTIC SAHLQVIST THEORY FOR DEDUCTIVE SYSTEMS

Abstract

Sahlqvist theory is extended to the fragments of the intuitionistic propositional calculus that include the conjunction connective. This allows us to introduce a Sahlqvist theory of intuitionistic character amenable to arbitrary protoalgebraic deductive systems. As an application, we obtain a Sahlqvist theorem for the fragments of the intuitionistic propositional calculus that include the implication connective and for the extensions of the intuitionistic linear logic.

1 Introduction

Sahlqvist theorem is one of modal logic’s crown jewels [71]. The theorem revolves around a family of syntactically defined modal formulas, known as Sahlqvist formulas, and consists of two halves, related to the phenomena of canonicity and correspondence, respectively. The canonicity part of the theorem states that the validity of Sahlqvist formulas is preserved by canonical extensions of modal algebras [55, 56], while the correspondence part states that the class of Kripke frames validating a Sahlqvist formula is strictly elementary. Taken together, the two imply that every normal modal logic axiomatized by Sahlqvist formulas is complete with respect to an elementary class of Kripke frames.

Whilst Sahlqvist theory has been at the center of many investigations in modal logic (see, e.g., [59, 72]), it received less attention in the setting of the intuitionistic propositional calculus $\mathsf {IPC}$ , with the notable exception of [46] (see also [22, 70]). This should not come as a surprise, as a version of Sahlqvist theory for $\mathsf {IPC}$ can easily be derived from the modal one, utilizing the Gödel–McKinsey–Tarski translation of $\mathsf {IPC}$ into the modal system $\mathsf {S4}$ [49, 63] and its semantic interpretation [62], as explained in [22]. However, this method breaks down for fragments of $\mathsf {IPC}$ , mostly because their duality theory is more opaque than that of $\mathsf {IPC}$ .

In this paper, we will fill this gap by extending Sahlqvist theory to fragments ¹ of $\mathsf {IPC}$ including the conjunction connective (Theorem 5.1). This will serve as the basis for our main contribution, which consists of a Sahlqvist theory of intuitionistic character amenable to arbitrary deductive systems (Theorem 7.15).

More precisely, we say that a formula of $\mathsf {IPC}$ is a Sahlqvist antecedent if it is constructed from negative formulas and the constants $0$ and $1$ using only $\land $ and $\lor $ . It is a Sahlqvist implication if it is either positive, or the negation of a Sahlqvist antecedent, or of the form $\varphi \to \psi $ , where $\varphi $ is a Sahlqvist antecedent and $\psi $ a positive formula. Lastly, formulas obtained from Sahlqvist implications using only $\land $ and $\lor $ will be called Sahlqvist formulas.

Instead of working with Sahlqvist formulas, we prefer to focus on Sahlqvist quasiequations, i.e., expressions of the form

$$\begin{align*}\varphi_1 \land y \leqslant z \, \& \cdots \& \, \varphi_n \land y \leqslant z \Longrightarrow y \leqslant z, \end{align*}$$

where $\varphi _1, \dots , \varphi _n$ are Sahlqvist formulas and y and z are distinct variables that do not occur in them. This is because, while in Heyting algebras (i.e., the algebraic models of $\mathsf {IPC}$ ) Sahlqvist quasiequations and formulas are equally expressive, in the case of fragments the expressive power of Sahlqvist quasiequations is often greater. For instance, the so-called bounded top width n axiom [74]

can be rendered as the Sahlqvist quasiequation

(1)

which, contrarily to the formula $\mathsf {btw}_n$ , does not contain the disjunction connective and, therefore, makes the concept of “bounded top width n” amenable also to the algebraic models of the $\langle \land , \lnot \rangle $ -fragment of $\mathsf {IPC}$ , i.e., pseudocomplemented semilattices. Furthermore, the role of the quasiequation $\Phi _n$ cannot be taken over by any formula or equation in $\land $ and $\lnot $ only, because the expressive power of the latter is extremely limited [54].

Recall that the lattice $\mathsf {Up}(\mathbb {X})$ of upsets of a poset $\mathbb {X}$ can be endowed with the structure of a Heyting algebra (see, e.g., [17, 34]). Furthermore, a formula of $\mathsf {IPC}$ is valid in a poset $\mathbb {X}$ viewed as a Kripke frame iff it is valid in the Heyting algebra $\mathsf {Up}(\mathbb {X})$ . Lastly, given a semilattice ${\boldsymbol {A}} = \langle A; \land \rangle $ , we denote by ${\boldsymbol {A}}_\ast $ the poset of its meet irreducible filters. The Sahlqvist theorem for fragments of $\mathsf {IPC}$ with $\land $ takes the following form (Theorems 4.12 and 5.1):

Theorem 1. The following conditions hold for a Sahlqvist quasiequation $\Phi $ in a language $\mathcal {L} \subseteq \{ \land , \lor , \to , \lnot , 0, 1 \}$ containing $\land :$

1. (i) Canonicity $:$ If an $\mathcal {L}$ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra validates $\Phi $ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\Phi $ .

2. (ii) Correspondence $:$ There exists an effective computable first-order sentence $\mathsf {tr}(\varphi )$ in the language of posets such that $\mathsf {Up}(\mathbb {X}) \vDash \Phi $ iff $\mathbb {X} \vDash \mathsf {tr}(\Phi )$ , for every poset  $\mathbb {X}$ .

The main obstacles in proving Theorem 1 can be summarized as follows. On the one hand, the method of [22] is based on the observation that a Heyting algebra ${\boldsymbol {A}}$ validates a formula $\varphi $ iff the free Boolean extension of ${\boldsymbol {A}}$ , viewed as a modal algebra, validates the Gödel–McKinsey–Tarski translation of $\varphi $ . This property, however, need not hold in subreducts of Heyting algebras, preventing the applicability of a similar method. On the other hand, the algebraic models of fragments of $\mathsf {IPC}$ with $\land $ admit the presence of operations that fail to be order preserving in every coordinate (such as the negation or the implication), contrarily to the case of [57]. Similarly, they need not have a lattice structure and, therefore, do not fall under the scope of [15, 20, 44].

Lastly, even when these models have a lattice structure (as in the case of finite pseudocomplemented semilattices), they need not be distributive lattices. Because of this reason, their traditional canonical canonical extensions [32, 42, 43] may fail to be Heyting algebras. For instance, the smallest nonmodular lattice $\boldsymbol {N}_{\hspace{-1pt}5}$ can be viewed as a pseudocomplemented semilattice, whose canonical extension is order isomorphic to $\boldsymbol {N}_{\hspace{-1pt}5}$ itself and, therefore, is not a Heyting algebra. To overcome this problem, in the canonicity part of the theorem we work with completions of the form $\mathsf {Up}({\boldsymbol {A}}_\ast )$ which, in turn, are always Heyting algebras. ² As a consequence, the order theoretic properties typical of canonical extensions which serve as the basis of the approach of [46] and [20, 21, 28] need not hold in our setting: for instance, the completions of the form $\mathsf {Up}({\boldsymbol {A}}_\ast )$ need not be dense in the sense of [32] and are not induced by a polarity of filters and ideals in the sense of [45].

Our main tools are a model theoretic observation on universal classes (Theorem 2.7) and the correspondence in Section 3 between algebraic homomorphisms on the one hand and partial order preserving maps that generalize the notion of a p-morphism typical of Esakia duality [33, 34] on the other hand (see, e.g., [4, 58, 78–80]).

As we mentioned, part of the interest of Theorem 1 is that it contains the germ of a Sahlqvist theory amenable to arbitrary logics (a.k.a. deductive systems), i.e., finitary and substitution invariant consequence relations on the set of formulas of some algebraic language. The price to pay in exchange for the great generality, however, is that the resulting Sahlqvist theory is of intuitionistic character and, therefore, does not apply to logics whose meet irreducible theories are maximally consistent (such as normal modal logics).

This generalization is made possible by the methods of abstract algebraic logic [35], which allow to recognize that the pillars sustaining the intuitionistic Sahlqvist theory are certain metalogical properties that govern the behavior of the intuitionistic connectives $\lnot , \to $ , and $\lor $ . More precisely, a logic $\vdash $ is said to have:

1. (i) The inconsistency lemma [67] when for every $n \in \mathbb {Z}^+$ there exists a finite set of formulas ${\thicksim _{n}\!\!(x_1, \dots , x_n)}$ such that for every finite set of formulas $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \}$ ,

   $$\begin{align*}\Gamma \cup \{\varphi_1, \dots, \varphi_n \} \text{ is inconsistent}\, \, \text{ iff } \, \, \Gamma \vdash\, \sim_n\!\!(\varphi_1, \dots, \varphi_n). \end{align*}$$

2. (ii) The deduction theorem [11] when there exists a finite set of formulas $x \Rightarrow y$ such that for every finite set of formulas $\Gamma \cup \{ \psi , \varphi \}$ ,

   $$\begin{align*}\Gamma, \psi \vdash \varphi \, \, \text{ iff } \, \, \Gamma \vdash \psi \Rightarrow \varphi. \end{align*}$$

3. (iii) The proof by cases [23, 27] when there exists a finite set $x \curlyvee y$ of formulas such that for every finite set of formulas $\Gamma \cup \{ \psi , \varphi , \gamma \}$ ,

   $$\begin{align*}\Gamma, \psi \vdash \gamma \text{ and }\Gamma, \varphi \vdash \gamma \, \, \text{ iff } \, \, \Gamma, \psi\curlyvee \varphi \vdash \gamma. \end{align*}$$

It is well known that $\mathsf {IPC}$ has the inconsistent lemma, the deduction theorem, and the proof by cases, as witnessed, respectively, by the sets

Accordingly, when a logic $\vdash $ possesses the metalogical properties governing the behavior of the connectives among $ \lnot , \to $ , and $\lor $ appearing in a formula $\varphi (x_1, \dots , x_n)$ of $\mathsf {IPC}$ , we say that $\varphi $ is compatible with $\vdash $ . In this case, with every $k \in \mathbb {Z}^+$ we can associate a finite set of formulas

$$\begin{align*}\boldsymbol{\varphi}^k(x_1^1, \dots, x_1^k, \dots, x_n^1, \dots, x_n^k) \end{align*}$$

of $\vdash $ which globally behaves as $\varphi $ . For instance, suppose that $\varphi = \lnot \psi $ and that we already defined $\boldsymbol {\psi }^k$ to be $\{ \chi _1, \dots , \chi _n \}$ . Since the connective $\lnot $ appears in $\varphi $ , the assumption that $\varphi $ is compatible with $\vdash $ guarantees that the latter has the inconsistency lemma. Accordingly, we set

thus ensuring that $\boldsymbol {\varphi }^k$ behaves as the negation of $\boldsymbol {\psi }^k = \{ \chi _1, \dots , \chi _n \}$ in $\vdash $ .

Our main result applies to logics $\vdash $ that are protoalgebraic, i.e., that possess a nonempty set of formulas $\Delta (x, y)$ which globally behaves as a weak implication, in the sense that $\emptyset \vdash \Delta (x, x)$ and modus ponens $x, \Delta (x, y) \vdash y$ hold [26]. It takes the form of a correspondence theorem connecting the validity of certain metarules in a logic $\vdash $ with the structure of the posets $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ of meet irreducible deductive filters of $\vdash $ on arbitrary algebras ${\boldsymbol {A}}$ (Theorem 7.15).

Theorem 2. Let $\varphi _1 \land y \leqslant z \, \& \cdots \& \, \varphi _n \land y \leqslant z \Longrightarrow y \leqslant z $ be a Sahlqvist quasiequation such that $\varphi _1, \dots , \varphi _n$ are compatible with a protoalgebraic logic $\vdash $ . Then $\vdash $ validates all the metarules of the form

iff the poset $\mathsf {Spec}_{\vdash }({\boldsymbol {A}})$ validates $\mathsf {tr}(\Phi )$ , for every algebra ${\boldsymbol {A}}$ .

For instance, a protoalgebraic logic with the inconsistency lemma validates the metarules corresponding to the bounded top width n Sahlqvist quasiequation in Condition (1) iff the principal upsets in $\mathsf {Spec}_{\vdash }({\boldsymbol {A}})$ have at most n maximal elements, for every algebra ${\boldsymbol {A}}$ (Theorem 8.6). In the case where $n=1$ , this was first proved in [60] (see also [66]).

The connection between Theorems 1 and 2 is made possible by a series of bridge theorems that connect the validity of the inconsistency lemma, the deduction theorem, and the proof by cases in a protoalgebraic logic $\vdash $ with the demand that the semilattices $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ of compact deductive filters of $\vdash $ on algebras ${\boldsymbol {A}}$ are subreducts of Heyting algebras in a suitable language containing $\land $ . For instance, a protoalgebraic logic $\vdash $ has the inconsistency lemma iff $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is a pseudocomplemented semilattice, for every algebra ${\boldsymbol {A}}$ [67]. A similar result, where implicative semilattices and distributive lattices take over the role of pseudocomplemented semilattices, holds for the deduction theorem and the proof by cases [10–12, 18, 23, 27]. This allows us to apply Theorem 1 to the semilattices of the form $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ . Together with the observation that the poset $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})_\ast $ of meet irreducible filters of $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is isomorphic to $\mathsf {Spec}_{\vdash }({\boldsymbol {A}})$ , these are the keys for extending Theorem 1 to arbitrary protoalgebraic logics.

Lastly, we come full circle and derive a version of Sahlqvist theory for fragments of $\mathsf {IPC}$ including the implication connective $\to $ from Theorem 2. As the correspondence part of the theory is already supplied by Theorem 1, our result takes the form of a canonicity theorem. More precisely, given a language $\mathcal {L} \subseteq \{ \land , \lor , \to , \lnot , 0, 1 \}$ containing $\to $ and an $\mathcal {L}$ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra, we denote by ${\boldsymbol {A}}_\ast $ the poset of meet irreducible implicative filters of ${\boldsymbol {A}}$ . Since every Sahlqvist quasiequation $\Phi $ in $\mathcal {L}$ can be rendered (up to equivalence in Heyting algebras) as a set $\mathsf {A}(\Phi )$ of formulas of $\mathcal {L}$ , our canonicity theorem can be phrased as follows (Theorem 9.6):

Theorem 3. Let $\Phi $ be a Sahlqvist quasiequation in a language $\mathcal {L} \subseteq \{ \land , \lor , \to , \lnot , 0, 1 \}$ containing $\to $ . If an $\mathcal {L}$ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra validates $\mathsf {A}(\Phi )$ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\mathsf {A}(\Phi )$ .

We close the paper with another application of Theorem 2, namely a correspondence result for intuitionistic linear logic (Theorem 10.8) which differs from the one in [75, 76] in that, while our theorem captures only the intuitionistic aspects of this logic, it extends naturally to its axiomatic extensions.

2 Pseudocomplemented and implicative semilattices

Definition 2.1. An algebra $\langle A; \land \rangle $ is said to be a semilattice when $\land $ is an associative, commutative, and idempotent binary operation.

With each semilattice $\langle A; \land \rangle $ we can associate a partial order $\leqslant $ on A defined, for every $a, b \in A$ , as follows:

(2) $$ \begin{align} a \leqslant b \, \, \Longleftrightarrow\, \, a \land b = a. \end{align} $$

In this case, $\langle A; \leqslant \rangle $ is a poset in which the binary meet of every pair of elements $a, b$ exists and coincides with the element $a \land b$ . Furthermore, given a poset $\langle A; \leqslant \rangle $ in which binary meets exist, the pair $\langle A; \land \rangle $ , where $\land $ is the operation of taking binary meets, is a semilattice. These transformations are one inverse to the other.

For the present purpose, two kinds of semilattices are of special interest (see, e.g., [38, 65]):

Definition 2.2. A semilattice $\langle A; \land \rangle $ is said to be:

1. (i) Pseudocomplemented if it has a minimum element $0$ and for each $a \in A$ there exists an element $\lnot a \in A$ such that for every $c \in A$ ,

   (3) $$ \begin{align} c \land a = 0 \, \, \Longleftrightarrow \, \, c \leqslant \lnot a. \end{align} $$

2. (ii) Implicative if for each $a, b \in A$ there exists an element $a \to b \in A$ such that for every $c \in A$ ,

   (4) $$ \begin{align} c \land a \leqslant b \, \, \Longleftrightarrow \, \, c \leqslant a \to b. \end{align} $$

It follows that a semilattice $\langle A; \land \rangle $ is pseudocomplemented if it has a minimum element $0$ and for each $a \in A$ there exists the largest $c \in A$ such that $a \land c = 0$ (in which case, we take it to be $\lnot a$ ). As a consequence, every pseudocomplemented semilattice has a maximum element, namely .

Similarly, a semilattice $\langle A; \land \rangle $ is implicative if for each $a, b \in A$ there exists the largest $c \in A$ such that $c \land a \leqslant b$ (in which case, we take it to be $a \to b$ ). As a consequence, implicative semilattices $\langle A; \land \rangle $ have always a maximum, namely $a \to a$ for an arbitrary $a \in A$ . Because of this, an implicative semilattice is said to be bounded when it has a minimum element $0$ . Notably, every bounded implicative semilattice $\langle A; \land \rangle $ is pseudocomplemented, since Condition (3) holds setting , for every $a \in A$ .

Since for every lattice $\langle A; \land , \lor \rangle $ the pair $\langle A; \land \rangle $ is a semilattice, the above terminology extends naturally to lattices [1, 34, 69]:

Definition 2.3. A lattice $\langle A; \land , \lor \rangle $ is said to be pseudocomplemented (resp. implicative) if so is $\langle A; \land \rangle $ . Bounded implicative lattices will be called Heyting algebras.

It is well known that the lattice reduct of an implicative lattice is always distributive.

Remark 2.4. Sometimes it will be convenient to treat pseudocomplemented and implicative semilattices as algebras whose basic operations include $\lnot $ , $\to $ , $0$ , and $1$ (as opposed to $\land $ only). When this is the case, we will assume that pseudocomplemented semilattices are algebras $\langle A; \land , \lnot , 0, 1 \rangle $ , where $\langle A; \land \rangle $ is a semilattice with minimum $0$ and maximum $1$ and $\lnot $ a unary operation on A satisfying Condition (3). Similarly, we will treat implicative semilattices as algebras $\langle A; \land , \to , 1 \rangle $ , where $\langle A; \land \rangle $ is a semilattice with maximum $1$ and $\to $ a binary operation on A satisfying Condition (4). Lastly, bounded implicative semilattices will be algebras $\langle A; \land , \to , 0, 1 \rangle $ , where $\langle A; \land , \to , 1 \rangle $ is an implicative semilattice with minimum $0$ . The analogous conventions apply to pseudocomplemented lattices, implicative lattices, and Heyting algebras with the only difference that the language of these structures will be assumed to contain the join operation $\lor $ .

When $\langle A; \land \rangle $ is a finite semilattice with a maximum element, the partial order $\langle A; \leqslant \rangle $ is a lattice in which

$$\begin{align*}a \lor b = \bigwedge \{ c \in A : a, b \leqslant c \}, \text{ for every }a, b \in A. \end{align*}$$

Because of this, Condition (ii) in the following result makes sense.

Proposition 2.5. The following conditions hold $:$

1. (i) If ${\boldsymbol {A}} = \langle A; \land , \lor , \lnot , 0, 1 \rangle $ is a finite pseudocomplemented distributive lattice, the structure $\langle A; \land , \lor , \to , 0, 1 \rangle $ , where $\to $ is defined as $a \to b = \max \{ c \in A : c \land a \leqslant b \}$ , is a Heyting algebra in which the term function $x \to 0$ coincides with the operation $\lnot $ of ${\boldsymbol {A}}$ .

2. (ii) If ${\boldsymbol {A}} = \langle A; \land , \to , 1 \rangle $ is a finite implicative semilattice, the structure $\langle A; \land , \lor , \to , 0, 1 \rangle $ , where $\lor $ and $0$ are, respectively, the join operation and the minimum element of $\langle A; \leqslant \rangle $ , is a Heyting algebra.

Proof Condition (i) holds because every finite distributive lattice is a Heyting algebra and the structure of a Heyting algebra is uniquely determined by its order reduct. For Condition (ii), see, e.g., [58].

Remark 2.6. In contrast to this, finite pseudocomplemented semilattices cannot be given in general the structure of a Heyting algebra, because they need not be distributive, e.g., the nonmodular pentagon lattice $\boldsymbol {N}_5$ is a pseudocomplemented semilattice.

We denote the class operators of closure under isomorphic copies, homomorphic images, subalgebras, direct products, and ultraproducts, respectively, by $\mathbb {I}, \mathbb {H}, \mathbb {S}$ , $\mathbb {P}$ , and . A class of similar algebras is said to be a quasivariety when it is closed under $\mathbb {I}, \mathbb {S}, \mathbb {P}$ , and or, equivalently, when it can be axiomatized by a set of quasiequations (see, e.g., [13, Theorem V.2.25]), i.e., universal sentences of the form

$$\begin{align*}\forall \vec{x}((\varphi_1 \thickapprox \psi_1 \, \& \, \cdots \, \& \, \varphi_n \thickapprox \psi_n)\Longrightarrow \epsilon \thickapprox \delta). \end{align*}$$

We often drop the the universal quantifier at the beginning of a quasiequation and write simply

$$\begin{align*}\varphi_1 \thickapprox \psi_1 \, \& \, \cdots \, \& \, \varphi_n \thickapprox \psi_n \Longrightarrow \epsilon \thickapprox \delta. \end{align*}$$

Lastly, a class of similar algebras is said to be a variety when it is closed under $\mathbb {H}$ , $\mathbb {S}$ , and $\mathbb {P}$ or, equivalently, when it can be axiomatized by a set of equations (see, e.g., [13, Theorem II.11.9]). When understood as in Remark 2.4, the following classes are examples of varieties:

From a logical standpoint, the interest of these varieties can be explained as follows. Let $\mathscr {L}$ be a sublanguage of the language of an algebra ${\boldsymbol {A}}$ . The $\mathscr {L}$ -reduct of ${\boldsymbol {A}}$ is the $\mathscr {L}$ -algebra . Accordingly, the subalgebras of the $\mathscr {L}$ -reduct of ${\boldsymbol {A}}$ are called $\mathscr {L}$ -subreducts of ${\boldsymbol {A}}$ . The varieties in the above display consist of the subreducts of Heyting algebras in the appropriate signature. For instance, $\mathsf {PSL}$ is the class of $\langle \land , \lnot , 0, 1 \rangle $ -subreducts of Heyting algebras, and similarly for the other cases.

A class of similar algebras $\mathsf {K}$ is said to be a universal class if it can be axiomatized by a set of universal sentences or, equivalently, if it is closed under $\mathbb {I}, \mathbb {S}$ , and (see, e.g., [13, Theorem V.2.10]). The least universal class containing a class of similar algebras $\mathsf {K}$ coincides with and will be denoted by $\mathbb {U}(\mathsf {K})$ . The rest of the section is devoted to proving the following:

Theorem 2.7. Let ${\boldsymbol {A}}$ be a semilattice in a variety between $\mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ . Then ${\boldsymbol {A}}$ embeds into the appropriate reduct ${\boldsymbol {B}}^-$ of a Heyting algebra ${\boldsymbol {B}}$ such that ${\boldsymbol {B}}^- \in \mathbb {U}({\boldsymbol {A}})$ .

To prove this, recall that a variety $\mathsf {K}$ is locally finite if its finitely generated members are finite. We rely on the following observation:

Proposition 2.8. The varieties $\mathsf {PSL}, \mathsf {(b)ISL}$ , and $\mathsf {PDL}$ are locally finite.

Proof For $\mathsf {(b)ISL}$ and $\mathsf {PSL}$ the result is essentially [29, Corollary III.4.1] (see also [30, 54]), while for $\mathsf {PDL}$ , see, e.g., [3, Corollary 4.55] and [61].

Furthermore, we will make use of the following general embedding theorem.

Proposition 2.9 [13, Theorem V.2.14].

Let $\mathsf {K} \cup \{ {\boldsymbol {A}} \}$ be a class of similar algebras. If every finitely generated subalgebra of ${\boldsymbol {A}}$ belongs to $\mathbb {I}\mathbb {S}(\mathsf {K})$ , then .

We are now ready to prove Theorem 2.7.

Proof We begin by the case where ${\boldsymbol {A}} \in \mathsf {ISL}$ . Since every finitely generated subalgebra of ${\boldsymbol {A}}$ embeds into itself, in view of Proposition 2.9 there exist a family $\{ {\boldsymbol {A}}_i : i \in I \}$ of finitely generated subalgebras of ${\boldsymbol {A}}$ and an ultrafilter U on I with an embedding

$$\begin{align*}f \colon {\boldsymbol{A}} \to \prod_{i \in I}{\boldsymbol{A}}_i /U. \end{align*}$$

Since universal classes are closed under $\mathbb {S}$ and

, we have

In view of Proposition 2.8, each ${\boldsymbol {A}}_i$ is finite and, therefore, can be expanded to a Heyting algebra ${\boldsymbol {A}}_i^+$ by Proposition 2.5(ii). Clearly,

is a Heyting algebra, whose $\langle \land , \to \rangle $ -reduct ${\boldsymbol {B}}^-$ coincides with $\prod _{i \in I}{\boldsymbol {A}}_i / U$ . Since ${\boldsymbol {A}}$ embeds into ${\boldsymbol {B}}^-$ and ${\boldsymbol {B}}^- \in \mathbb {U}({\boldsymbol {A}})$ , we are done.

The same proof works for the case where ${\boldsymbol {A}}$ belongs to $\mathsf {bISL}$ or to $\mathsf {PDL}$ with the only difference that, when ${\boldsymbol {A}} \in \mathsf {PDL}$ , we apply Condition (i) of Proposition 2.5 instead of Condition (ii). Lastly, the case where ${\boldsymbol {A}}$ belongs to $\mathsf {HA}$ is straightforward, since can simply take .

It only remains to consider the case where ${\boldsymbol {A}} \in \mathsf {IL}$ . Let ${\boldsymbol {A}}^+$ be the expansion of ${\boldsymbol {A}}$ with a new constant $c_a$ for each of its elements a. Let also $0$ be another new constant. Then, consider the set of sentences

where $\mathsf {Th}({\boldsymbol {A}}^+)$ is the elementary theory of ${\boldsymbol {A}}^+$ and $0 \leqslant c_a$ is a shorthand for ${0 \land c_a \thickapprox 0}$ . Clearly, every finite part $\Gamma $ of $\Sigma $ is realizable in ${\boldsymbol {A}}^+$ , for if $c_{a_1}, \dots , c_{a_n}, 0$ are the new constants appearing in $\Gamma $ , we can interpret $0$ as $c_{a_1} \land \dots \land c_{a_n}$ in ${\boldsymbol {A}}^+$ . Therefore, we can apply the Compactness Theorem of first-order logic, obtaining that $\Sigma $ has a model $\boldsymbol {C}$ .

Let ${\boldsymbol {B}}^+$ be the subalgebra of $\boldsymbol {C}$ generated by $\{ 0 \} \cup \{ c_a : a \in A \}$ . As $\boldsymbol {C}$ is a model of $\mathsf {Th}({\boldsymbol {A}}^+)$ , the map $f \colon A \to C$ defined by the assignment is an elementary embedding of ${\boldsymbol {A}}$ into the $\langle \land , \lor , \to , 1 \rangle $ -reduct ${\boldsymbol {C}}^-$ of $\boldsymbol {C}$ . Consequently, ${\boldsymbol {A}}$ embeds also into the $\langle \land , \lor , \to , 1 \rangle $ -reduct ${\boldsymbol {B}}^-$ of ${\boldsymbol {B}}^+$ . Furthermore, as ${\boldsymbol {B}}^-$ embeds into the elementary extension ${\boldsymbol {C}}^-$ of ${\boldsymbol {A}}$ and the validity of universal sentences persists in elementary extensions and subalgebras, ${\boldsymbol {B}}^-$ satisfies all the universal sentences valid in ${\boldsymbol {A}}$ and, therefore, belongs to $\mathbb {U}({\boldsymbol {A}})$ .

To conclude the proof, it only remains to show that ${\boldsymbol {B}}^-$ is the $\langle \land , \lor , \to , 1 \rangle $ -reduct of a Heyting algebra ${\boldsymbol {B}}$ . Since ${\boldsymbol {A}} \in \mathsf {IL}$ and $\mathsf {IL}$ is a universal class, from ${\boldsymbol {B}}^-\in \mathbb {U}({\boldsymbol {A}})$ it follows that ${\boldsymbol {B}}^- \in \mathsf {IL}$ . Therefore, it suffices to prove that $0$ is the minimum element of ${\boldsymbol {B}}^-$ , as in this case we can let ${\boldsymbol {B}}$ be the expansion of ${\boldsymbol {B}}^-$ with $0$ .

To prove this, recall that ${\boldsymbol {B}}^+$ is the subalgebra of $\boldsymbol {C}$ generated by of $\{ 0 \} \cup \{ c_a : a \in A \}$ . Therefore, every element of ${\boldsymbol {B}}^-$ (equiv. of ${\boldsymbol {B}}^+$ ) has the form $\varphi ^{{\boldsymbol {C}}}(0, c_{a_1}, \dots , c_{a_n})$ for some $a_1, \dots , a_n \in A$ and $\langle \land , \lor , \to , 1 \rangle $ -term $\varphi (y, x_1, \dots , x_n)$ . We will prove by induction on the construction of $\varphi $ that

$$\begin{align*}0 \leqslant \varphi^{{\boldsymbol{C}}}(0, c_{a_1}, \dots, c_{a_n}) \end{align*}$$

for every $a_1, \dots , a_n \in A$ .

In the base case, $\varphi $ is either the constant $1$ or a variable. If it is the constant $1$ , then $\varphi ^{\boldsymbol {C}}(0, c_{a_1}, \dots , c_{a_n})$ is the maximum of ${\boldsymbol {C}}$ , whence the above display holds. Then we consider the case where $\varphi $ is a variable. Since $\varphi \in \{ y, x_1, \dots , x_n \}$ , we have $\varphi ^{\boldsymbol {C}}(0, c_{a_1}, \dots , c_{a_n}) \in \{ 0, c_{a_1}, \dots , c_{a_n}\}$ . If $\varphi ^{\boldsymbol {C}}(0, c_{a_1}, \dots , c_{a_n}) = 0$ , it is clear that the above display holds. Consider the case where $\varphi ^{\boldsymbol {C}}(0, c_{a_1}, \dots , c_{a_n}) = c_{a_i}$ for some $i \leqslant n$ . Since ${\boldsymbol {C}}$ is a model of the formula $0 \leqslant c_{a_i}$ (which belongs to $\Sigma $ ), we obtain $0 \leqslant c_{a_i} = \varphi ^{\boldsymbol {C}}(0, c_{a_1}, \dots , c_{a_n})$ as desired.

In the induction step, $\varphi $ is a complex formula. The case where $\varphi $ is of the form $\psi _1 \land \psi _2$ or $\psi _1 \lor \psi _2$ is straightforward. Accordingly, we detail only the case where $\varphi $ is of the form $\psi _1 \to \psi _2$ . By the inductive hypothesis, we have

$$\begin{align*}0 \leqslant \psi_2^{{\boldsymbol{C}}}(0, c_{a_1}, \dots, c_{a_n}) \end{align*}$$

and, therefore,

$$\begin{align*}0 \land \psi_1^{{\boldsymbol{C}}}(0, c_{a_1}, \dots, c_{a_n}) \leqslant \psi_2^{{\boldsymbol{C}}}(0, c_{a_1}, \dots, c_{a_n}). \end{align*}$$

Since ${\boldsymbol {C}}$ is an elementary extension of ${\boldsymbol {A}}$ , it satisfies Condition (4). Consequently, from the above display it follows

$$\begin{align*}0 \leqslant \psi_1^{{\boldsymbol{C}}}(0, c_{a_1}, \dots, c_{a_n}) \to^{{\boldsymbol{C}}} \psi_2^{{\boldsymbol{C}}}(0, c_{a_1}, \dots, c_{a_n}) = \varphi^{{\boldsymbol{C}}}(0, c_{a_1}, \dots, c_{a_n}). \end{align*}$$

Hence, we conclude that $0$ is the minimum of ${\boldsymbol {B}}^-$ as desired.

3 Posets and partial functions

In this section, we will individuate a correspondence between homomorphisms in the varieties $\mathsf {PSL}$ , $\mathsf {(b)ISL}$ , $\mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ and appropriate partial functions between (possibly empty) posets that generalize the notion of a p-morphism typical of Esakia duality for Heyting algebras [33, 34].

The idea of using partial functions to dualize varieties of subreducts of Heyting algebras can be traced back at least to [58, 77] and [78–80] and was developed systematically in [4, 5, 14, 16]. Our presentation is largely inspired by the approach of [4], which deals with categories of Heyting algebras with maps preserving the operations in some smaller signature. Since we work with semilattices (as opposed to Heyting algebras), some additional care will be needed, however.

For a poset $\mathbb {X}$ and $Y \subseteq X$ , let

We call the set Y an upset if $Y={\uparrow }Y$ and a downset if $Y={\downarrow }Y$ . If $Y = \{ y \}$ , we simply write ${\uparrow } y$ and ${\downarrow } y$ instead of ${\uparrow } \{ y \}$ and ${\downarrow } \{ y\}$ . When the poset $\mathbb {X}$ is not clear from the context, we will write ${\uparrow }^{\mathbb {X}} Y$ and ${\downarrow }^{\mathbb {X}} Y$ , respectively, instead of ${\uparrow } Y$ and ${\downarrow } Y$ .

A partial function p from a set X to a set Y is a function from a subset Z of X to Y. In this case, Z is said to be the domain of p and will be denoted by $\mathsf {dom}(p)$ . We will write $p \colon X \rightharpoonup Y$ to indicate that p is a partial function from X to Y. A partial function $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ between posets is order preserving when, for every $x, z \in \mathsf {dom}(p)$ ,

$$\begin{align*}\text{if }x \leqslant^{\mathbb{X}} z, \text{ then }p(x) \leqslant^{\mathbb{Y}} p(z). \end{align*}$$

Definition 3.1. An order preserving partial function $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ between posets is:

1. (i) A partial negative p-morphism if

   $$\begin{align*}X = {\downarrow}^{\mathbb{X}} \{ x \in X : {\uparrow}^{\mathbb{X}}x \subseteq \mathsf{dom}(p) \} \end{align*}$$

   and for every $x \in \mathsf {dom}(p)$ and $y \in Y$ ,

   $$\begin{align*}\text{if }p(x) \leqslant^{\mathbb{Y}} y, \text{ there exists }z \in \mathsf{dom}(p)\text{ s.t. }x \leqslant^{\mathbb{X}}z \text{ and }y \leqslant^{\mathbb{Y}} p(z). \end{align*}$$

2. (ii) A partial positive p-morphism if for every $x \in \mathsf {dom}(p)$ and $y \in Y$ ,

   $$\begin{align*}\text{if }p(x) \leqslant^{\mathbb{Y}} y, \text{ there exists }z \in \mathsf{dom}(p)\text{ s.t. }x \leqslant^{\mathbb{X}}z \text{ and }y = p(z). \end{align*}$$

3. (iii) A partial p-morphism if it is both a partial negative p-morphism and a partial positive p-morphism.

When p is a total function, we drop the adjective partial in the above definitions.

Remark 3.2. Partial p-morphisms $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ coincide with partial positive p-morphism such that $X = {\downarrow }\mathsf {dom}(p)$ .

We say that a partial function $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ between posets is almost total when $\mathsf {dom}(p)$ is a downset of $\mathbb {X}$ . Notice that almost total partial functions $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ such that $X = {\downarrow }\mathsf {dom}(p)$ are indeed total. In particular, almost total partial (negative) p-morphisms are total. On the other hand, almost total partial implicative p-morphism need not be total in general, e.g., if U is a proper downset of $\mathbb {X}$ and y a maximal element of $\mathbb {Y}$ , the partial function $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ such that $\mathsf {dom}(p) = U$ and $p[U] = \{ y \}$ is an almost total partial positive morphism that fails to be total.

With every variety $\mathsf {K}$ among $\mathsf {PSL}, \mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ we associate a collection $\mathsf {K}^\partial $ consisting of the class of all posets with suitable partial functions between them as follows: ³

We will refer to the partial functions in $\mathsf {K}^\partial $ as to the arrows of $\mathsf {K}^\partial $ .

Every variety $\mathsf {K}$ among $\mathsf {PSL}, \mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ is related to $\mathsf {K}^\partial $ as follows. An element a of a semilattice ${\boldsymbol {A}}$ is said to be meet irreducible if it is not the maximum of ${\boldsymbol {A}}$ and, for every $b, c \in A$ ,

$$\begin{align*}\text{if }a = b \land c \text{, then either }a = b \text{ or }a = c. \end{align*}$$

A filter of ${\boldsymbol {A}}$ is a nonempty upset of $\langle A; \leqslant \rangle $ closed under binary meets. When ordered under the inclusion relation, the set of filters of ${\boldsymbol {A}}$ forms a lattice in which meets are intersections. Accordingly, a filter F of ${\boldsymbol {A}}$ is said to be meet irreducible when it is meet irreducible in the lattice of filters of ${\boldsymbol {A}}$ , i.e., when F is proper and either $F = G$ or $F = H$ for every pair $G, H$ of filters of ${\boldsymbol {A}}$ such that $F = G \cap H$ . The poset of meet irreducible filters of ${\boldsymbol {A}}$ will be denoted by ${\boldsymbol {A}}_\ast $ .

Remark 3.3. When the poset underlying a semilattice ${\boldsymbol {A}}$ is a distributive lattice, a filter F of ${\boldsymbol {A}}$ is meet irreducible iff it is prime, i.e., iff $A \smallsetminus F$ is nonempty and closed under binary joins [6, Theorem 12].

Let $\mathsf {K}$ be a variety among $\mathsf {PSL}, \mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ . Given ${\boldsymbol {A}}, {\boldsymbol {B}} \in \mathsf {K}$ and a homomorphism $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ , let $f_\ast \colon {\boldsymbol {B}}_\ast \rightharpoonup {\boldsymbol {A}}_\ast $ be the partial function with

defined as

for every $F \in \mathsf {dom}(f_\ast )$ .

Conversely, given a poset $\mathbb {X}$ , let $\mathsf {Up}_{\mathsf {K}}(\mathbb {X})$ be the reduct in the language of $\mathsf {K}$ of the Heyting algebra

$$\begin{align*}\langle \mathsf{Up}(\mathbb{X}); \cap, \cup, \to, \emptyset, X \rangle, \end{align*}$$

where $\mathsf {Up}(\mathbb {X})$ is the set of upsets of $\mathbb {X}$ and $\to $ is defined by

Notice that $\mathsf {Up}_{\mathsf {K}}(\mathbb {X}) \in \mathsf {K}$ , because $\mathsf {K}$ is the class of subreducts of Heyting algebras in the language of $\mathsf {K}$ . Lastly, given an arrow $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ in $\mathsf {K}^\partial $ , let $\mathsf {Up}_{\mathsf {K}}(p) \colon \mathsf {Up}_{\mathsf {K}}(\mathbb {Y}) \to \mathsf {Up}_{\mathsf {K}}(\mathbb {X})$ be the map defined for every $U \in \mathsf {Up}_{\mathsf {K}}(\mathbb {Y})$ as

. When $\mathsf {K} = \mathsf {HA}$ , we often drop the subscript $\mathsf {K}$ from $\mathsf {Up}_{\mathsf {K}}(\mathbb {X})$ and $\mathsf {Up}_{\mathsf {K}}(p)$ .

Remark 3.4. In the case of $\mathsf {HA}$ , the applications $(-)_{\ast }$ and $\mathsf {Up}(-)$ are the contravariant functors underlying Esakia duality [33, 34].

The rest of the section is devoted to the proof of the following result.

Proposition 3.5. Let $\mathsf {K}$ be a variety among $\mathsf {PSL}, \mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ . The following conditions hold for every ${\boldsymbol {A}}, {\boldsymbol {B}} \in \mathsf {K}$ and every pair $\mathbb {X}, \mathbb {Y}$ of posets $:$

1. (i) If $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ is a homomorphism, then $f_\ast \colon {\boldsymbol {B}}_\ast \rightharpoonup {\boldsymbol {A}}_\ast $ is an arrow in $\mathsf {K}^\partial $ .

2. (ii) If $p \colon \mathbb {X}\rightharpoonup \mathbb {Y}$ is an arrow in $\mathsf {K}^\partial $ , then $\mathsf {Up}_{\mathsf {K}}(p) \colon \mathsf {Up}_{\mathsf {K}}(\mathbb {Y}) \to \mathsf {Up}_{\mathsf {K}}(\mathbb {X})$ is a homomorphism.

Furthermore, if f is injective $($ resp. p is surjective $)$ , then $f_\ast $ is surjective $($ resp. $\mathsf {Up}_{\mathsf {K}}(p)$ is injective $)$ .

When ordered under the inclusion relation, the set $\mathsf {Fi}({\boldsymbol {A}})$ of filters of a semilattice ${\boldsymbol {A}}$ with maximum forms a lattice $\langle \mathsf {Fi}({\boldsymbol {A}}); \cap , + \rangle $ , where the join operation $+$ is defined as

We rely on the next observation.

Lemma 3.6. Let $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ be a homomorphism between two semilattices, F a filter of ${\boldsymbol {B}}$ , and $G \in {\boldsymbol {A}}_\ast $ . If $f^{-1}[F] \subseteq G$ and the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ , then there exists $H \in {\boldsymbol {B}}_\ast $ such that $F \subseteq H$ and $G = f^{-1}[H]$ .

Proof Consider the poset $\mathbb {X}$ whose universe is

$$\begin{align*}\{ P : P\text{ is a filter of }{\boldsymbol{B}} \text{ such that }F \cup f[G] \subseteq P \text{ and }P \cap f[A \smallsetminus G] = \emptyset \} \end{align*}$$

and whose order is the inclusion relation. By assumption, $\mathbb {X}$ is nonempty because it contains the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ . Since $\mathbb {X}$ is closed under unions of chains, we can apply Zorn’s Lemma obtaining that $\mathbb {X}$ has a maximal element H.

Claim 3.7. The filter H is meet irreducible.

Proof of the Claim

Suppose the contrary, with a view to contradiction. By assumption, G is a meet irreducible filter of ${\boldsymbol {A}}$ and, therefore, proper. Consequently, $A \smallsetminus G$ is nonempty, whence so is $f[A \smallsetminus G]$ . Since H is disjoint from $f[A \smallsetminus G]$ , we conclude that H is proper. Since H is not meet irreducible, this means that there are two filters $H_1, H_2$ of ${\boldsymbol {B}}$ other than H such that $H = H_1 \cap H_2$ . From the maximality of H in $\mathbb {X}$ it follows that neither $H_1$ nor $H_2$ is disjoint from $f[A \smallsetminus G]$ . Therefore, there are $a, b\in A \smallsetminus G$ such that

(5) $$ \begin{align} f(a) \in H_1 \, \, \text{ and } \, \, f(b) \in H_2. \end{align} $$

Now, from $a, b \in A \smallsetminus G$ it follows that G is properly contained in $G + {\uparrow }^{\boldsymbol {A}} a$ and $G + {\uparrow }^{\boldsymbol {A}} b$ . Since G a meet irreducible filter of ${\boldsymbol {A}}$ , this guarantees that

$$\begin{align*}G \subsetneq (G + {\uparrow}^{\boldsymbol{A}} a) \cap (G + {\uparrow}^{\boldsymbol{B}} a). \end{align*}$$

Accordingly, there are $c \in G$ and $d \in A \smallsetminus G$ such that

$$\begin{align*}a \land^{{\boldsymbol{A}}} c \leqslant d \, \, \text{ and } \, \, b \land^{{\boldsymbol{A}}} c \leqslant d. \end{align*}$$

Since f is a homomorphism, we obtain

(6) $$ \begin{align} f(a) \land^{\boldsymbol{B}} f(c) \leqslant f(d) \, \, \text{ and } \, \, f(b) \land^{\boldsymbol{B}} f(c) \leqslant f(d). \end{align} $$

Furthermore, from $c \in G$ and the assumption that $f[G] \subseteq H = H_1 \cap H_2$ it follows that $f(c) \in H_1 \cap H_2$ . Together with Conditions (5) and (6) and the fact that $H_1, H_2$ are filters of ${\boldsymbol {B}}$ , this implies that

$$\begin{align*}f(d) \in H_1 \cap H_2 = H, \end{align*}$$

a contradiction with the assumption that $d \in A \smallsetminus G$ and $H \cap f[A \smallsetminus G] = \emptyset $ . Hence, we conclude that H is meet irreducible.

By the claim, $H \in {\boldsymbol {B}}_\ast $ . Furthermore, since $H \in \mathbb {X}$ , we know that $F \subseteq H$ . Therefore, it only remains to prove that $G = f^{-1}[H]$ . The fact that $H \in \mathbb {X}$ guarantees that $f[G] \subseteq H$ and $H \cap f[A \smallsetminus G] = \emptyset $ . From $f[G] \subseteq H$ it follows $G \subseteq f^{-1}[f[G]] \subseteq f^{-1}[H]$ . To prove the other inclusion, consider $a \in f^{-1}[H]$ . Then $f(a) \in H$ . Since $H \cap f[A \smallsetminus G] = \emptyset $ and $a \in A$ , this implies that $a \in G$ as desired.

Lastly, we rely on the following technical lemma.

Lemma 3.8. Let $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ be a partial function between posets and $U,V \in \mathsf {Up}({\mathbb {Y}})$ . Then

$$\begin{align*}{\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus (U \cap V)] = {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus U] \cup {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus V]. \end{align*}$$

Moreover, if p is total and order preserving, it also holds

$$\begin{align*}{\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus (U \cup V)] = {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus U] \cap {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus V]. \end{align*}$$

Proof The proof of the first part of the statement is straightforward. As for the second part, suppose that p is total and order preserving. The inclusion from left to right follows from the fact that the function ${\downarrow }^{\mathbb {X}}p^{-1}[-] \colon \mathscr {P}({Y}) \to \mathscr {P}({X})$ is order preserving. To prove the other inclusion, consider $x \in {\downarrow }^{\mathbb {X}} p^{-1}[Y \smallsetminus U] \cap {\downarrow }^{\mathbb {X}} p^{-1}[Y \smallsetminus V]$ . Then there are $u, v \in X$ such that $p(u) \in Y \smallsetminus U$ , $p(v) \in Y \smallsetminus V$ , and $x \leqslant ^{\mathbb {X}}u, v$ . Since p is a total function, $x \in \mathsf {dom}(p)$ . Furthermore, as p is order preserving and $x \leqslant ^{\mathbb {X}}u, v$ , we obtain $p(x) \leqslant ^{\mathbb {Y}}p(u), p(v)$ . Together with the assumption that U and V are upsets and that $p(u) \notin U$ and $p(v) \notin V$ , this yields $p(x) \in Y \smallsetminus (U \cup V)$ . Hence, we conclude that $x \in {\downarrow }^{\mathbb {X}} p^{-1}[Y \smallsetminus (U \cup V)]$ .

In order to prove Proposition 3.5, it will be convenient to consider the cases of $\mathsf {PSL}$ and $\mathsf {ISL}$ separately. We begin by the case of $\mathsf {PSL}$ .

Lemma 3.9. Let ${\boldsymbol {A}}, {\boldsymbol {B}} \in \mathsf {PSL}$ with a homomorphism $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ , let $F \in \mathsf {Fi}({\boldsymbol {B}})$ , and let $G \in \mathsf {Fi}({\boldsymbol {A}})$ be maximal and proper. If $f^{-1}[F] \subseteq G$ , the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ .

Proof Suppose, with a view to contradiction, that $f^{-1}[F] \subseteq G$ and that the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is not disjoint from $f[A \smallsetminus G]$ . Then there exist $a_1, \dots , a_n \in G$ , $b_1, \dots , b_m \in F$ , and $c \in A \smallsetminus G$ such that

$$\begin{align*}f(a_1) \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} f(a_n) \land^{\boldsymbol{B}} b_1 \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} b_m \leqslant f(c). \end{align*}$$

Since G is maximal and proper, $G + {\uparrow }^{\boldsymbol {A}} c = A$ . Therefore, $c \land ^{\boldsymbol {A}} d = 0^{\boldsymbol {A}}$ for some $d \in G$ . By Condition (3), this yields $d \leqslant \lnot ^{\boldsymbol {A}} c$ and, since f is a homomorphism, $f(d) \leqslant \lnot ^{\boldsymbol {B}} f(c)$ .

As $d \in G$ , we may assume, without loss of generality, that $d \in \{ a_1, \dots , a_n \}$ . Therefore, from $f(d) \leqslant \lnot ^{\boldsymbol {B}} f(c)$ and the above display it follows

$$\begin{align*}f(a_1) \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} f(a_n) \land^{\boldsymbol{B}} b_1 \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} b_m \leqslant f(c) \land^{\boldsymbol{B}} \lnot^{\boldsymbol{B}} f(c) = 0^{\boldsymbol{B}}. \end{align*}$$

Since f is a homomorphism, we can apply Condition (3) obtaining

$$\begin{align*}b_1 \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} b_m \leqslant \lnot^{\boldsymbol{B}} f(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) = f(\lnot^{\boldsymbol{A}}(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n)). \end{align*}$$

As F is a filter of ${\boldsymbol {B}}$ containing $b_1, \dots , b_m$ , the above display guarantees that $f(\lnot ^{\boldsymbol {A}}(a_1 \land ^{\boldsymbol {A}} \dots \land ^{\boldsymbol {A}} a_n)) \in F$ . As a consequence, $\lnot ^{\boldsymbol {A}}(a_1 \land ^{\boldsymbol {A}} \dots \land ^{\boldsymbol {A}} a_n) \in f^{-1}[F] \subseteq G$ . But together with the fact that $a_1, \dots , a_n \in G$ and that G is a filter of ${\boldsymbol {A}}$ , this implies

$$\begin{align*}0^{\boldsymbol{A}} = (a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \land \lnot^{\boldsymbol{A}}(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \in G, \end{align*}$$

a contradiction with the assumption that G is proper.

The homomorphisms in $\mathsf {PSL}$ and the arrows in $\mathsf {PSL}^\partial $ are related as follows.

Proposition 3.10. Let ${\boldsymbol {A}}, {\boldsymbol {B}} \in \mathsf {PSL}$ and let $\mathbb {X},\mathbb {Y}$ be posets. The following conditions hold $:$

1. (i) If $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ is a homomorphism, then $f_{\ast } \colon {\boldsymbol {B}}_\ast \rightharpoonup {\boldsymbol {A}}_\ast $ is a partial negative p-morphism.

2. (ii) If $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ is a partial negative p-morphism, then $\mathsf {Up}_{\mathsf {PSL}}(p) \colon \mathsf {Up}_{\mathsf {PSL}}(\mathbb {Y}) \to \mathsf {Up}_{\mathsf {PSL}}(\mathbb {X})$ is a homomorphism.

Proof (i): The definition of $f_\ast $ guarantees that $f_\ast \colon {\boldsymbol {B}}_\ast \rightharpoonup {\boldsymbol {A}}_\ast $ is a well-defined partial order preserving map. Therefore, it suffices to prove that:

1. 1. ${\boldsymbol {B}}_\ast = {\downarrow }^{{\boldsymbol {B}}_\ast }\{ F \in {\boldsymbol {B}}_\ast : {\uparrow }^{{\boldsymbol {B}}_\ast }F \subseteq \mathsf {dom}(f_\ast )\}$ .

2. 2. For every $F \in \mathsf {dom}(f_\ast )$ and $G \in {\boldsymbol {A}}_\ast $ ,

   $$\begin{align*}\text{if }f_\ast(F) \subseteq G, \text{ there exists }H \in \mathsf{dom}(f_\ast)\text{ s.t. }F \subseteq H \text{ and }G \subseteq f_\ast(H). \end{align*}$$

Notice that inverse images under f of proper filters of ${\boldsymbol {B}}$ are proper filters of ${\boldsymbol {A}}$ , because f preserves binary meets and minimum elements. We will use this observation repeatedly.

To prove Condition (1), it suffices to establish the inclusion ${\boldsymbol {B}}_\ast \subseteq {\downarrow }^{{\boldsymbol {B}}_\ast }\{ F \in {\boldsymbol {B}}_\ast : {\uparrow }^{{\boldsymbol {B}}_\ast }F \subseteq \mathsf {dom}(f_\ast )\}$ as the other one is obvious. Accordingly, consider $F \in {\boldsymbol {B}}_\ast $ . Since F is a proper filter of ${\boldsymbol {B}}$ , the set $f^{-1}[F]$ is a proper filter of ${\boldsymbol {A}}$ . By Zorn’s Lemma, we can extend it to a maximal proper filter G of ${\boldsymbol {A}}$ . Being maximal and proper, G is meet irreducible and, therefore, it belongs to ${\boldsymbol {A}}_\ast $ . Furthermore, since $f^{-1}[F] \subseteq G$ , we can apply Lemma 3.9 obtaining that the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ . By Lemma 3.6, there exists $H \in {\boldsymbol {B}}_\ast $ such that $F \subseteq H$ and $G = f^{-1}[H]$ . Thus, $H \in \mathsf {dom}(f_\ast )$ and $f_\ast (H) = G$ . To conclude the proof, it only remains to show that ${\uparrow }^{{\boldsymbol {B}}_\ast } H \subseteq \mathsf {dom}(f_\ast )$ . To this end, consider $H^+ \in {\uparrow }^{{\boldsymbol {B}}_\ast } H$ . Since $H^+$ is a proper filter of ${\boldsymbol {B}}$ , the set $f^{-1}[H^+]$ is a proper filter of ${\boldsymbol {A}}$ . Furthermore, $G = f^{-1}[H] \subseteq f^{-1}[H^+]$ . Since G is a maximal proper filter of ${\boldsymbol {A}}$ and $f^{-1}[H^+]$ is a proper filter of ${\boldsymbol {A}}$ , this implies $f^{-1}[H^+] = G \in {\boldsymbol {A}}_\ast $ . Hence, we conclude that $H^+ \in \mathsf {dom}(f_\ast )$ as desired.

Then we turn to prove Condition (2). Consider $F \in \mathsf {dom}(f_\ast )$ and $G \in {\boldsymbol {A}}_\ast $ such that $f_\ast (F) \subseteq G$ , that is, $f^{-1}[F] \subseteq G$ . We may assume, without loss of generality, that G is maximal and proper (otherwise we use Zorn’s Lemma to extend it to such a filter). Therefore, we can apply Lemma 3.9 obtaining that the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ . By Lemma 3.6, there exists $H \in {\boldsymbol {B}}_\ast $ such that $F \subseteq H$ and $G = f^{-1}[H]$ . We conclude that $H \in \mathsf {dom}(f_\ast )$ and $G = f_\ast (H)$ .

(ii): To see that $\mathsf {Up}_{\mathsf {PSL}}(p) \colon \mathsf {Up}_{\mathsf {PSL}}(\mathbb {Y}) \to \mathsf {Up}_{\mathsf {PSL}}(\mathbb {X})$ preserves binary meets, recall from Lemma 3.8 that

$$\begin{align*}{\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus (U \cap V)] = {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus U] \cup {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus V], \end{align*}$$

for every $U,V \in \mathsf {Up}({\mathbb {Y}})$ . Therefore, we obtain

$$\begin{align*}X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus (U \cap V)] = ( X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus U]) \cap (X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus V]), \end{align*}$$

that is, $\mathsf {Up}_{\mathsf {PSL}}(p)(U \cap V) = \mathsf {Up}_{\mathsf {PSL}}(p)(U) \cap \mathsf {Up}_{\mathsf {PSL}}(p)(V)$ , as desired.

We now detail the proof that $\mathsf {Up}_{\mathsf {PSL}}(p)$ preserves the operation $\lnot $ (this, in turn, guarantees that $\mathsf {Up}_{\mathsf {PSL}}(p)$ preserves also the constant $0$ , because the latter is term-definable as $x \land \lnot x$ ). Consider $U \in \mathsf {Up}_{\mathsf {PSL}}(\mathbb {Y})$ . We need to prove that

$$\begin{align*}\mathsf{Up}_{\mathsf{PSL}}(p) (\lnot^{\mathsf{Up}_{\mathsf{PSL}}(\mathbb{Y})} (U)) = \lnot^{\mathsf{Up}_{\mathsf{PSL}}(\mathbb{X})}\mathsf{Up}_{\mathsf{PSL}}(p)(U). \end{align*}$$

Using the definitions of $\mathsf {Up}_{\mathsf {PSL}}(p)$ and of the operation $\lnot $ in $\mathsf {Up}_{\mathsf {PSL}}(\mathbb {Y})$ and $\mathsf {Up}_{\mathsf {PSL}}(\mathbb {X})$ , this amounts to

$$\begin{align*}X \smallsetminus {\downarrow}^{\mathbb{X}}(p^{-1}[{\downarrow}^{\mathbb{Y}}U]) = X \smallsetminus {\downarrow}^{\mathbb{X}}(X \smallsetminus {\downarrow}^{\mathbb{X}}(p^{-1}[Y \smallsetminus U])). \end{align*}$$

Clearly, it suffices to show that the complements of the sets in the above display coincide, namely,

(7) $$ \begin{align} {\downarrow}^{\mathbb{X}}(p^{-1}[{\downarrow}^{\mathbb{Y}}U]) = {\downarrow}^{\mathbb{X}}(X \smallsetminus {\downarrow}^{\mathbb{X}}(p^{-1}[Y \smallsetminus U])). \end{align} $$

To prove the inclusion from left to right in Condition (7), consider $x \in {\downarrow }^{\mathbb {X}}(p^{-1}[{\downarrow }^{\mathbb {Y}}U])$ . Then there are $z \in X$ and $u \in U$ such that $z \in \mathsf {dom}(p)$ and

$$\begin{align*}x \leqslant^{\mathbb{X}} z \, \, \text{ and } \, \, p(z) \leqslant^{\mathbb{Y}} u. \end{align*}$$

Since $p(z) \leqslant ^{\mathbb {Y}} u$ and $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ is a partial negative p-morphism, there exists $w \in \mathsf {dom}(p)$ such that $z \leqslant ^{\mathbb {X}} w$ and $u \leqslant ^{\mathbb {Y}} p(w)$ . Together with the above display, this yields $x \leqslant ^{\mathbb {X}} w$ . Therefore, to conclude that $x \in {\downarrow }^{\mathbb {X}}(X \smallsetminus {\downarrow }^{\mathbb {X}}(p^{-1}[Y \smallsetminus U]))$ , it suffices to show that $w \in X \smallsetminus {\downarrow }^{\mathbb {X}}(p^{-1}[Y \smallsetminus U])$ . Accordingly, consider $v \in \mathsf {dom}(p)$ such that $w \leqslant ^{\mathbb {X}} v$ . We need to show that $p(v) \in U$ . Since p is order preserving, from $w \leqslant ^{\mathbb {X}} v$ it follows $p(w) \leqslant ^{\mathbb {Y}} p(v)$ . Together with $u \leqslant ^{\mathbb {Y}} p(w)$ , this yields $u \leqslant ^{\mathbb {Y}}p(v)$ . Since U is an upset of $\mathbb {Y}$ and $u \in U$ , we conclude that $p(v) \in U$ as desired.

Lastly, we prove the inclusion from right to left in Condition (7). Consider $x \in {\downarrow }^{\mathbb {X}}(X \smallsetminus {\downarrow }^{\mathbb {X}}(p^{-1}[Y \smallsetminus U]))$ . Then there exists $z \in X$ such that $x \leqslant ^{\mathbb {X}} z$ and for every $w \in X$ ,

$$\begin{align*}\text{if }z \leqslant^{\mathbb{X}} w \text{ and }w \in \mathsf{dom}(p)\text{, then }p(w) \in U. \end{align*}$$

Since p is a partial negative p-morphism, $X = {\downarrow }^{\mathbb {X}}\mathsf {dom}(p)$ . Thus, there exists $w \in \mathsf {dom}(p)$ with $z \leqslant ^{\mathbb {X}} w$ . In view of the above display, we obtain $p(w) \in U$ . Since $x \leqslant ^{\mathbb {X}} z\leqslant ^{\mathbb {X}} w$ , this yields $x \in {\downarrow }^{\mathbb {X}}(p^{-1}[U]) \subseteq {\downarrow }^{\mathbb {X}}(p^{-1}[{\downarrow }^{\mathbb {Y}}U])$ .

Now, we turn our attention to the case of implicative semilattices.

Lemma 3.11. Let ${\boldsymbol {A}}, {\boldsymbol {B}} \in \mathsf {ISL}$ with a homomorphism $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ , let $F \in \mathsf {Fi}({\boldsymbol {B}})$ , and let $G \in \mathsf {Fi}({\boldsymbol {A}})$ . If $f^{-1}[F] \subseteq G$ , the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ .

Proof Suppose, with a view to contradiction, that $f^{-1}[F] \subseteq G$ and that the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ contains an element $c \in f[A \smallsetminus G]$ . Then there exist $a_1, \dots , a_n \in G$ and $b_1, \dots , b_m \in F$ such that

$$\begin{align*}f(a_1) \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} f(a_n) \land^{\boldsymbol{B}} b_1 \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} b_m \leqslant c. \end{align*}$$

Since f preserves binary meets, this yields

$$\begin{align*}f(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \land^{\boldsymbol{B}} b_1 \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} b_m \leqslant c. \end{align*}$$

Together $c \in f[A \smallsetminus G]$ , this implies that there exists $d \in A \smallsetminus G$ such that

$$\begin{align*}f(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \land^{\boldsymbol{B}} b_1 \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} b_m \leqslant f(d). \end{align*}$$

Applying Condition (4) and the fact that f preserves $\to $ to the above display, we obtain

$$\begin{align*}b_1 \land^{\boldsymbol{B}} \dots \land^{\boldsymbol{B}} b_m \leqslant f(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \to^{\boldsymbol{B}} f(d) = f((a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \to^{\boldsymbol{A}} d). \end{align*}$$

Lastly, as F is a filter of ${\boldsymbol {B}}$ containing $b_1, \dots , b_m$ , the above display guarantees that $f((a_1 \land ^{\boldsymbol {A}} \dots \land ^{\boldsymbol {A}} a_n) \to ^{\boldsymbol {A}} d) \in F$ . As a consequence, $(a_1 \land ^{\boldsymbol {A}} \dots \land ^{\boldsymbol {A}} a_n) \to ^{\boldsymbol {A}} d \in f^{-1}[F] \subseteq G$ . Together with the fact that $a_1, \dots , a_n \in G$ and that G is a filter of ${\boldsymbol {A}}$ , this implies

$$\begin{align*}(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \land^{\boldsymbol{A}} ((a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \to^{\boldsymbol{A}} d) \in G. \end{align*}$$

Since G is an upset and, by Condition (4), we have

$$\begin{align*}(a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \land^{\boldsymbol{A}} ((a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n) \to^{\boldsymbol{A}} d) \leqslant d, \end{align*}$$

this implies $d \in G$ , a contradiction with the assumption that $d \in A \smallsetminus G$ .

The homomorphisms in $\mathsf {ISL}$ and the arrows in $\mathsf {ISL}^\partial $ are related as follows.

Proposition 3.12. Let ${\boldsymbol {A}}, {\boldsymbol {B}} \in \mathsf {ISL}$ and let $\mathbb {X},\mathbb {Y}$ be posets. The following conditions hold $:$

1. (i) If $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ is a homomorphism, then $f_{\ast } \colon {\boldsymbol {B}}_\ast \rightharpoonup {\boldsymbol {A}}_\ast $ is a partial positive p-morphism.

2. (ii) If $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ is a partial positive p-morphism, then $\mathsf {Up}_{\mathsf {ISL}}(p) \colon \mathsf {Up}_{\mathsf {ISL}}(\mathbb {Y}) \to \mathsf {Up}_{\mathsf {ISL}}(\mathbb {X})$ is a homomorphism.

Proof (i): The definition of $f_\ast $ guarantees that $f_\ast \colon {\boldsymbol {B}}_\ast \rightharpoonup {\boldsymbol {A}}_\ast $ is a well-defined partial order preserving map. Therefore, it suffices to prove that for every $F \in \mathsf {dom}(f_\ast )$ and $G \in {\boldsymbol {A}}_\ast $ ,

$$\begin{align*}\text{if }f_\ast(F) \subseteq G, \text{ there exists }H \in \mathsf{dom}(f_\ast)\text{ s.t. }F \subseteq H \text{ and }G = f_\ast(H). \end{align*}$$

Accordingly, let $F \in \mathsf {dom}(f_\ast )$ and $G \in {\boldsymbol {A}}_\ast $ be such that $f_\ast (F) \subseteq G$ , that is, $f^{-1}[F] \subseteq G$ . By Lemma 3.11, the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ . Therefore, we can apply Lemma 3.6 obtaining an $H \in {\boldsymbol {B}}_\ast $ that contains F such that $G = f^{-1}[H]$ . Since $G \in {\boldsymbol {A}}_\ast $ , we conclude that $H \in \mathsf {dom}(f_\ast )$ and $G = f_{\ast }(H)$ as desired.

(ii): The proof of this condition coincides with that of [4, Theorem 3.15] (although the respective statements are slightly different).

We are now ready to prove Proposition 3.5.

Proof The cases where $\mathsf {K}$ is $\mathsf {PSL}$ , $\mathsf {ISL}$ , or $\mathsf {bISL}$ follow from Propositions 3.10 and 3.12, while the case where $\mathsf {K} = \mathsf {HA}$ is well known (see Remark 3.4). Therefore it only remains to detail the cases of $\mathsf {PDL}$ and $\mathsf {IL}$ . We detail the case of $\mathsf {PDL}$ only, as that of $\mathsf {IL}$ is analogous.

To prove Condition (i), consider ${\boldsymbol {A}}, {\boldsymbol {B}} \in \mathsf {PDL}$ and let $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ be a homomorphism. Since f is a homomorphism of pseudocomplemented semilattices, $f_\ast \colon {\boldsymbol {B}}_\ast \rightharpoonup {\boldsymbol {A}}_\ast $ is a partial negative p-morphism by Proposition 3.10(i). To prove that $f_\ast $ is total, consider $F \in {\boldsymbol {B}}_\ast $ . Since ${\boldsymbol {B}}$ is a distributive lattice, F is a prime filter in view of Remark 3.3. As f preserves binary joins, $f^{-1}[F]$ is a prime filter of ${\boldsymbol {A}}$ , whence $f^{-1}[F] \in {\boldsymbol {A}}_\ast $ by Remark 3.3. Thus, we conclude that $F \in \mathsf {dom}(f_\ast )$ and, therefore, that $f_\ast $ is total. This shows that $f_\ast $ is a negative p-morphism.

To prove Condition (ii), let $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ be a negative p-morphism. By Proposition 3.10(ii), $\mathsf {Up}_{\mathsf {PDL}}(p)$ is a homomorphism of pseudocomplemented semilattices. Therefore, it only remains to prove that it preserves binary joins. To this end, consider $U, V \in \mathsf {Up}(\mathbb {Y})$ . Since

$$ \begin{align*} \mathsf{Up}_{\mathsf{PDL}}(p)(U \lor^{\mathsf{Up}_{\mathsf{PDL}}(\mathbb{Y})} V)&= X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus (U \cup V)]\\ \mathsf{Up}_{\mathsf{PDL}}(p)(U) \lor^{\mathsf{Up}_{\mathsf{PDL}}(\mathbb{X})} \mathsf{Up}_{\mathsf{PDL}}(p)(V)&= (X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \kern1.3pt{\smallsetminus}\kern1.3pt U]) \cup (X \kern1.3pt{\smallsetminus}\kern1.3pt {\downarrow}^{\mathbb{X}} p^{-1}[Y \kern1.3pt{\smallsetminus}\kern1.3pt V]), \end{align*} $$

it suffices to show that

$$\begin{align*}(X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus U]) \cup (X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus V]) = X \smallsetminus {\downarrow}^{\mathbb{X}} p^{-1}[Y \smallsetminus (U \cup V)]. \end{align*}$$

As p is order preserving and total, we can apply the second part of Lemma 3.8 obtaining that the above display holds. As a consequence, $\mathsf {Up}_{\mathsf {PDL}}(p)$ is a homomorphism as desired.

It only remains to prove the last part of the statement, namely, that for every variety $\mathsf {K}$ among $\mathsf {PSL}, \mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ , every homomorphism $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ in $\mathsf {K}$ , and every arrow $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ in $\mathsf {K}^\partial $ , if f is injective (resp. p is surjective), then $f_\ast $ is surjective (resp. $\mathsf {Up}_{\mathsf {K}}(p)$ is injective).

Suppose first that $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}$ is injective and consider $G \in {\boldsymbol {A}}_\ast $ . Since G is proper, we can choose an element $a \in G$ and consider the filter of ${\boldsymbol {B}}$ . Since f is order reflecting, $f^{-1}[F] \subseteq {\uparrow }^{\boldsymbol {A}} a$ . Together with $a \in G$ and the fact that G is an upset, this implies $f^{-1}[F] \subseteq G$ . We will prove that the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ . Suppose, on the contrary, that there exists some $b \in B$ in the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ and in $f[A \smallsetminus G]$ . Since $b \in f[A \smallsetminus G]$ there exists $c \in A \smallsetminus G$ such that $f(c) = b$ . Since $F = {\uparrow }^{\boldsymbol {B}} f(a)$ and b belongs to the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ , there are $a_1, \dots , a_n \in G$ such that

$$\begin{align*}f(a \land^{\boldsymbol{A}} a_1 \land^{\boldsymbol{A}} \dots \land^{\boldsymbol{A}} a_n )= f(a) \land^{\boldsymbol{B}} f(a_1) \land^{\boldsymbol{B}} \dots \land^{{\boldsymbol{B}}} f(a_n) \leqslant b = f(c). \end{align*}$$

As f is order reflecting, this implies $a \land ^{\boldsymbol {A}} a_1 \land ^{\boldsymbol {A}} \dots \land ^{\boldsymbol {A}} a_n \leqslant a$ . As G is a filter and $a, a_1, \dots , a_n \in G$ , we obtain that $c \in G$ , a contradiction with the assumption that $c \in A \smallsetminus G$ . In sum, $f^{-1}[F] \subseteq G$ and the filter of ${\boldsymbol {B}}$ generated by $F \cup f[G]$ is disjoint from $f[A \smallsetminus G]$ . Therefore, we can apply Lemma 3.6 obtaining an $H \in {\boldsymbol {B}}_\ast $ such that $G = f^{-1}[H]$ . Hence, $H \in \mathsf {dom}(f_\ast )$ and $f_\ast (H) = G$ and we conclude that $f_\ast $ is surjective.

Lastly, consider a surjective arrow $p \colon \mathbb {X} \rightharpoonup \mathbb {Y}$ in $\mathsf {K}^\partial $ and let $U, V$ be distinct upsets of $\mathbb {Y}$ . By symmetry, we may assume that there exists $y \in U \smallsetminus V$ . Since p is surjective, there exists $x \in \mathsf {dom}(p)$ such that $p(x) = y$ . Since p is order preserving, $p(x) \in U$ , and U is an upset, we have $x \notin {\downarrow }^{\mathbb {X}}p^{-1}[Y \smallsetminus U]$ , whence $x \in X \smallsetminus {\downarrow }^{\mathbb {X}}p^{-1}[Y \smallsetminus U] = \mathsf {Up}_{\mathsf {K}}(p)(U)$ . On the other hand, as $p(x) \in U \smallsetminus V \subseteq Y \smallsetminus V$ , we obtain $x \in {\downarrow }^{\mathbb {X}}p^{-1}[Y \smallsetminus V]$ , whence $x \notin X \smallsetminus {\downarrow }^{\mathbb {X}}p^{-1}[Y \smallsetminus V] = \mathsf {Up}_{\mathsf {K}}(p)(V)$ . Hence, we conclude that $\mathsf {Up}_{\mathsf {K}}(p)(U) \ne \mathsf {Up}_{\mathsf {K}}(p)(V)$ and, therefore, that $\mathsf {Up}_{\mathsf {K}}(p)$ is injective as desired.

4 Sahlqvist theory for $\mathsf {IPC}$

Sahlqvist theory [71] is usually formulated in the setting of modal logic (see, e.g., [7, 72]). However, the Gödel–McKinsey–Tarski translation of the intuitionistic propositional calculus $\mathsf {IPC}$ into the modal system $\mathsf {S4}$ allows to extend Sahlqvist theory to $\mathsf {IPC}$ , as shown in [22]. ⁴ In this section, we will review this process in such a way that it will help set the stage for the study of fragments of $\mathsf {IPC}$ .

Consider the modal language

$$ \begin{align*} \mathcal{L}_{\Box}\quad \!\!\! ::= & \quad x \mid \varphi \land \psi \mid \varphi \lor \psi \mid \varphi \to \psi \mid \lnot \varphi \mid \Box \varphi \mid \Diamond \varphi \mid 0 \mid 1. \end{align*} $$

Formulas of $\mathcal {L}_\Box $ will be assumed to have variables in a denumerable set ${Var = \{ x_n : n \in \mathbb {Z}^+ \}}$ and arbitrary elements of $Var$ will often be denoted by $x, y$ , and z.

Definition 4.1. Let $\varphi $ be a formula of $\mathcal {L}_\Box $ and x a variable. An occurrence of x in $\varphi $ is said to be positive (resp. negative) if the sum of negations and antecedents of implications within whose scopes it appears is even (resp. odd). Moreover, we say a x is positive (resp. negative) in $\varphi $ if every occurrence of x in $\varphi $ is positive (resp. negative). Lastly, $\varphi $ is said to be positive (resp. negative) if every variable is positive (resp. negative) in $\varphi $ .

Formulas of the form $\Box ^n x$ with $x \in Var$ and $n \in \mathbb {N}$ will be called boxed atoms. Notice that the elements of $Var$ are also boxed atoms, because $x = \Box ^0 x$ for every $x \in Var$ .

Definition 4.2. A formula of $\mathcal {L}_\Box $ is said to be:

1. (i) A modal Sahlqvist antecedent if it is constructed from boxed atoms, negative formulas, and the constants $0$ and $1$ using only $\land $ , $\lor $ , and $\Diamond $ .

2. (ii) A modal Sahlqvist implication if it is positive, or it is of the form $\lnot \varphi $ for a modal Sahlqvist antecedent $\varphi $ , or it is of the form $\varphi \to \psi $ for a modal Sahlqvist antecedent $\varphi $ and a positive formula $\psi $ .

Remark 4.3. When applied to modal logic, our definition of a modal Sahlqvist implication is intentionally redundant. For if $\varphi $ is positive and $\psi $ a modal Sahlqvist antecedent, then $\varphi $ is equivalent to $1 \to \varphi $ and $\lnot \psi $ is equivalent to $\psi \to 0$ . Accordingly, in modal logic the third possibility in the definition of a modal Sahlqvist implication subsumes (up lo logical equivalence) the first two.

In the next definition $x \leqslant y$ is a shorthand for the equation $x \land y \thickapprox x$ .

Definition 4.4. A modal Sahlqvist quasiequation is an expression $\Phi $ of the form

$$\begin{align*}\varphi_1 \land y \leqslant z \, \& \cdots \& \, \varphi_n \land y \leqslant z \Longrightarrow y \leqslant z, \end{align*}$$

where y and z are distinct variables that do not occur in $\varphi _1, \dots , \varphi _n$ and each $\varphi _i$ is constructed from modal Sahlqvist implications using only $\land , \lor $ , and $\Box $ . If, in addition, $\Phi $ does not contain any occurrence of $\Box $ or $\Diamond $ , we say that $\Phi $ is simply a Sahlqvist quasiequation.

Example 4.5. For every $n \in \mathbb {Z}^+$ , the bounded top width n axiom ⁵ [74] is the formula of $\mathsf {IPC}$

When $n = 1$ , the formula $\mathsf {btw}_n$ is equivalent over $\mathsf {IPC}$ to the weak excluded middle law $\lnot x \lor \lnot \lnot x$ [53]. Notably, each $\mathsf {btw}_n$ can be rendered as the Sahlqvist quasiequation

in the sense that a Heyting algebra validates $\mathsf {btw}_n$ iff it validates $\Phi _n$ .

Similarly, the excluded middle $x \lor \lnot x$ and the Gödel–Dummett axiom ${(x_1 \to x_2) \lor (x_2 \to x_1)}$ [31, 50] can be rendered, respectively, as the Sahlqvist quasiequations

$$\begin{align*}{}&x \land y \leqslant z \, \& \, \lnot x \land y \leqslant z \Longrightarrow y \leqslant z \, \, \text{ and }\\&\quad (x_1 \to x_2) \land y \leqslant z \, \& \, (x_2 \to x_1) \land y \leqslant z \Longrightarrow y \leqslant z. \\[-35pt] \end{align*}$$

In the modal logic literature, the role of modal Sahlqvist quasiequations is played by the so-called modal Sahlqvist formulas, i.e., formulas that can be constructed from modal Sahlqvist implications using only $\land , \lor $ , and $\Box $ . ⁶ When $\Box $ and $\Diamond $ do not occur in a modal Sahlqvist formula $\varphi $ , we will say that $\varphi $ is simply a Sahlqvist formula.

In order to clarify the relation between (modal) Sahlqvist quasiequations and formulas, recall that a modal algebra is a structure $\langle A; \land , \lor , \lnot , \Box , 0, 1 \rangle $ where $\langle A; \land ,\lor , \lnot , 0, 1 \rangle $ is a Boolean algebra and for every $a, b \in A$ ,

$$\begin{align*}\Box (a \land b) = \Box a \land \Box b \, \, \text{ and } \, \, \Box 1 = 1. \end{align*}$$

We say that a formula $\varphi $ is valid in a modal (resp. Heyting) algebra ${\boldsymbol {A}}$ , in symbols ${\boldsymbol {A}} \vDash \varphi $ , when ${\boldsymbol {A}}$ satisfies the equation $\varphi \thickapprox 1$ .

Proposition 4.6. A modal Sahlqvist quasiequation

$$\begin{align*}\Phi = \varphi_1 \land y \leqslant z \, \& \cdots \& \, \varphi_n \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

is valid in a modal algebra ${\boldsymbol {A}}$ iff ${\boldsymbol {A}} \vDash \varphi _1 \lor \dots \lor \varphi _n$ .

Proof Suppose that ${\boldsymbol {A}} \vDash \Phi $ and consider $\vec {a} \in A$ . For every $i \leqslant n$ , we have

$$\begin{align*}\varphi_i(\vec{a}) \land 1 = \varphi_i(\vec{a}) \leqslant\varphi_1(\vec{a}) \lor \dots \lor \varphi_n(\vec{a}). \end{align*}$$

Since ${\boldsymbol {A}} \vDash \Phi $ , this implies $1 \leqslant \varphi _1(\vec {a}) \lor \dots \lor \varphi _n(\vec {a})$ . As $1$ is the maximum of ${\boldsymbol {A}}$ , we conclude that $\varphi _1(\vec {a}) \lor \dots \lor \varphi _n(\vec {a}) = 1$ as desired.

Conversely, suppose that ${\boldsymbol {A}} \vDash \varphi _1 \lor \dots \lor \varphi _n$ and consider $\vec {a}, b, c \in A$ such that $\varphi _i(\vec {a}) \land b \leqslant c$ for every $i \leqslant n$ . Using the distributive laws, we obtain

$$\begin{align*}(\varphi_1(\vec{a}) \lor \dots \lor \varphi_n(\vec{a})) \land b = (\varphi_1(\vec{a}) \land b) \lor \dots \lor(\varphi_n(\vec{a}) \land b) \leqslant c. \end{align*}$$

Since ${\boldsymbol {A}} \vDash \varphi _1 \lor \dots \lor \varphi _n$ , this yields $b = 1 \land b \leqslant c$ , whence ${\boldsymbol {A}} \vDash \Phi $ .

A similar argument yields the following:

Corollary 4.7. A Sahlqvist quasiequation

$$\begin{align*}\varphi_1 \land y \leqslant z \, \& \cdots \& \, \varphi_n \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

is valid in a Heyting algebra ${\boldsymbol {A}}$ iff ${\boldsymbol {A}} \vDash \varphi _1 \lor \dots \lor \varphi _n$ .

The reason why (modal) Sahlqvist quasiequations and formulas are two faces of the same coin is that, in view of Proposition 4.6 and Corollary 4.7, a (resp. modal) Sahlqvist quasiequation

$$\begin{align*}\varphi_1 \land y \leqslant z \, \& \cdots \& \, \varphi_n \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

is valid in a Heyting (resp. modal) algebra ${\boldsymbol {A}}$ iff so is the (resp. modal) Sahlqvist formula $\varphi _1 \lor \dots \lor \varphi _n$ . Conversely, a (resp. modal) Sahlqvist formula $\varphi $ is valid in ${\boldsymbol {A}}$ iff so is the (resp. modal) Sahlqvist quasiequation $\varphi \land y \leqslant z \Longrightarrow y \leqslant z$ .

Remark 4.8. The focus on Sahlqvist quasiequations (as opposed formulas or equations) is motivated by the fact that we deal with fragments of $\mathsf {IPC}$ where formulas have a very limited expressive power. For instance, in $\mathsf {PSL}$ there are only three nonequivalent equations [54], while there are infinitely many nonequivalent Sahlqvist quasiequations, as shown in Example 4.5.

In addition, we cannot remove the “context” y from Sahlqvist quasiequations. For instance, the Sahlqvist quasiequation

$$\begin{align*}\Phi = \lnot x \land y \leqslant z \, \& \, \lnot \lnot x \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

corresponding to the weak excluded middle law (see Example 4.5) is not equivalent to its context free version $\Psi = \lnot x \leqslant z \, \& \, \lnot \lnot x \leqslant z \Longrightarrow z \thickapprox 1$ over $\mathsf {PSL}$ , for $\Psi $ holds in the pseudocomplemented semilattice ${\boldsymbol {A}}$ depicted in Figure 1, while $\Phi $ fails in ${\boldsymbol {A}}$ as witnessed by the assignment

$$\begin{align*}{}x \longmapsto a \qquad y \longmapsto b \qquad z \longmapsto c. \end{align*}$$

Figure 1 A pseudocomplemented semilattice.

With every Kripke frame $\mathbb {X} = \langle X, R \rangle $ we can associate a modal algebra

where $\lnot $ and $\Box $ are defined for every $Y \subseteq X$ as

Conversely, with a modal algebra ${\boldsymbol {A}}$ we can associate a Kripke frame

, where X is the set of ultrafilters of ${\boldsymbol {A}}$ and

Notably, ${\boldsymbol {A}}$ embeds into the algebra $\mathscr {P}_{\mathsf {M}}({{\boldsymbol {A}}_+})$ , known as the canonical extension of ${\boldsymbol {A}}$ [55, 56].

Our aim is to extend the next classical version of Sahlqvist theorem to $\mathsf {IPC}$ .

Modal Sahlqvist Theorem 4.9 [7, Theorems 3.54 and 5.91].

The following conditions hold for a modal Sahlqvist quasiequation $\Phi$

1. (i) Canonicity $:$ If a modal algebra ${\boldsymbol {A}}$ validates $\Phi $ , then also $\mathscr {P}_{\mathsf {M}}({{\boldsymbol {A}}_+})$ validates $\Phi $ .

2. (ii) Correspondence $:$ There is an effectively computable first-order sentence $\mathsf {mtr}(\Phi )$ ⁷ in the language of Kripke frames such that $\mathscr {P}_{\mathsf {M}}({\mathbb {X}}) \vDash \Phi $ iff $\mathbb {X} \vDash \mathsf {mtr}(\Phi )$ , for every Kripke frame $\mathbb {X}$ .

Let $\mathcal {L}$ be the language of $\mathsf {IPC}$ , i.e., the language obtained from $\mathcal {L}_\Box $ by removing $\Box $ and $\Diamond $ . Recall that the Gödel–McKinsey–Tarski translation [49, 63] associates with every formula $\varphi $ of $\mathcal {L}$ a formula $\varphi _g$ of $\mathcal {L}_\Box $ , defined recursively as follows: for every $x \in Var$ ,

Given a Sahlqvist quasiequation

$$\begin{align*}\Phi = \varphi_1 \land y \leqslant z \, \& \cdots \& \, \varphi_n \land y \leqslant z \Longrightarrow y \leqslant z, \end{align*}$$

we set

The following observation is an immediate consequence of the definitions.

Lemma 4.10. If $\Phi $ is a Sahlqvist quasiequation, then $\Phi _g$ is a modal Sahlqvist quasiequation.

The next result is instrumental to extend Sahlqvist theorem to $\mathsf {IPC}$ .

Proposition 4.11. The following conditions hold $:$

1. (i) $\mathsf {Up}(\mathbb {X}) \vDash \Phi $ iff $\mathscr {P}_{\mathsf {M}}({\mathbb {X}}) \vDash \Phi _g$ , for every poset $\mathbb {X}$ and Sahlqvist quasiequation $\Phi $ .

2. (ii) For every Heyting algebra ${\boldsymbol {A}}$ there exists a modal algebra $\mathsf {f}({\boldsymbol {A}})$ with ${\boldsymbol {A}}_\ast \cong \mathsf {f}({\boldsymbol {A}})_+$ and such that ${\boldsymbol {A}} \vDash \Phi $ iff $\mathsf {f}({\boldsymbol {A}}) \vDash \Phi _g$ , for every Sahlqvist quasiequation $\Phi $ .

Proof (i): It is well known that

(8) $$ \begin{align} \mathsf{Up}(\mathbb{X}) \vDash \varphi \iff \mathscr{P}_{\mathsf{M}}({\mathbb{X}}) \vDash \varphi_g \end{align} $$

for every formula $\varphi $ of $\mathcal {L}$ and poset $\mathbb {X}$ (see, e.g., [17, Corollary 3.82]). Then for every poset $\mathbb {X}$ and Sahlqvist quasiequation $\Phi = \varphi _1 \land y \leqslant z \, \& \cdots \& \, \varphi _n \land y \leqslant z \Longrightarrow y \leqslant z$ , we have

$$ \begin{align*} \mathsf{Up}(\mathbb{X}) \vDash \Phi \, \, &\Longleftrightarrow \, \, \mathsf{Up}(\mathbb{X}) \vDash \varphi_1 \lor \dots \lor \varphi_n\\ \, \, &\Longleftrightarrow \, \,\mathscr{P}_{\mathsf{M}}({\mathbb{X}}) \vDash (\varphi_1 \lor \dots \lor \varphi_n)_g \\ \, \,&\Longleftrightarrow \, \,\mathscr{P}_{\mathsf{M}}({\mathbb{X}}) \vDash \varphi_{1g} \lor \dots \lor \varphi_{ng}\\ \, \,&\Longleftrightarrow \, \,\mathscr{P}_{\mathsf{M}}({\mathbb{X}}) \vDash \Phi_g. \end{align*} $$

The equivalences above are justified as follows: the first and the last follow, respectively, from Corollary 4.7 and Proposition 4.6, the second holds by Condition (8), and the third by the definition of the Gödel–McKinsey–Tarski translation.

(ii): Let $\mathsf {f}({\boldsymbol {A}})$ be the subalgebra of $\mathscr {P}_{\mathsf {M}}({{\boldsymbol {A}}_\ast })$ generated by the sets of the form

for every $a \in A$ . In view of [62, Lemmas 3.1 and 3.2], for every formula $\varphi $ of $\mathcal {L}$ we have

$$\begin{align*}{\boldsymbol{A}} \vDash \varphi \, \,\Longleftrightarrow \, \,\mathsf{f}({\boldsymbol{A}})\vDash \varphi_g. \end{align*}$$

As in the proof of Condition (i), this implies that ${\boldsymbol {A}} \vDash \Phi $ iff $\mathsf {f}({\boldsymbol {A}}) \vDash \Phi _g$ , for every Sahlqvist quasiequation $\Phi $ . For a proof that ${\boldsymbol {A}}_\ast \cong \mathsf {f}({\boldsymbol {A}})_+$ , see, e.g., [34, Construction 2.5.7 and Theorem 3.4.6(1)].

As a consequence, we obtain a version of Sahlqvist theorem for $\mathsf {IPC}$ :

Intuitionistic Sahlqvist Theorem 4.12 [22, Theorems 6.1 and 7.1].

The following conditions hold for a Sahlqvist quasiequation $\Phi :$

1. (i) Canonicity $:$ If a Heyting algebra ${\boldsymbol {A}}$ validates $\Phi $ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\Phi $ .

2. (ii) Correspondence $:$ There is an effectively computable first-order sentence $\mathsf {tr}(\Phi )$ in the language of posets such that $\mathsf {Up}(\mathbb {X}) \vDash \Phi $ iff $\mathbb {X} \vDash \mathsf {tr}(\Phi _g)$ , for every poset  $\mathbb {X}$ .

Proof (i): Suppose that ${\boldsymbol {A}} \vDash \Phi $ . In view of Proposition 4.11(ii), we have $\mathsf {f}({\boldsymbol {A}}) \vDash \Phi _g$ . As $\Phi _g$ is a modal Sahlqvist quasiequation by Lemma 4.10, we can apply the canonicity part of the Modal Sahlqvist Theorem obtaining $\mathscr {P}_{\mathsf {M}}({\mathsf {f}({\boldsymbol {A}})_+}) \vDash \Phi _g$ . Since ${\boldsymbol {A}}_\ast \cong \mathsf {f}({\boldsymbol {A}})_+$ by Proposition 4.11(ii), this amounts to $\mathscr {P}_{\mathsf {M}}({{\boldsymbol {A}}_\ast }) \vDash \Phi _g$ . Together with by Proposition 4.11(i), this implies that $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ as desired.

(ii): From Proposition 4.11(i) it follows that $\mathsf {Up}(\mathbb {X}) \vDash \Phi $ iff $\mathscr {P}_{\mathsf {M}}({\mathbb {X}}) \vDash \Phi _g$ . Furthermore, as $\Phi _g$ is a modal Sahlqvist quasiequation by Lemma 4.10, we can apply the correspondence part of the Modal Sahlqvist Theorem obtaining that $\mathscr {P}_{\mathsf {M}}({\mathbb {X}}) \vDash \Phi _g$ iff $\mathbb {X} \vDash \mathsf {mtr}(\Phi _g)$ , where the first-order sentence $\mathsf {mtr}(\Phi _g)$ is effectively computable. Therefore, setting , we are done.

Example 4.13. Let $n \in \mathbb {Z}^+$ and consider the Sahlqvist quasiequation $\Phi _n$ associated with the formula $\mathsf {btw}_n$ defined in Example 4.5. Since $\Phi _n$ and $\mathsf {btw}_n$ are equivalent over Heyting algebras, for every poset $\mathbb {X}$ we have

$$\begin{align*}\mathsf{Up}(\mathbb{X}) \vDash \Phi_n \, \,\Longleftrightarrow\, \, \mathsf{Up}(\mathbb{X}) \vDash \mathsf{btw}_n. \end{align*}$$

On the other hand, it is known that $\mathsf {Up}(\mathbb {X})\vDash \mathsf {btw}_n$ iff for every $x \in X$ and $y_1, \dots , y_{n+1} \in {\uparrow }x$ there exist $z_1, \dots , z_n \in {\uparrow }x$ such that $y_1, \dots , y_{n+1} \in {\downarrow }\{z_1, \dots , z_n \}$ (see, e.g., [17, Exercise 2.11]).

As the latter condition can be rendered as a first-order sentence $\Psi _n$ in the language of posets, we obtain the following instance of the correspondence part of the Intuitionistic Sahlqvist Theorem, for every poset $\mathbb {X}$ ,

$$\begin{align*}\mathsf{Up}(\mathbb{X}) \vDash \Phi_n \, \,\Longleftrightarrow \, \,\mathbb{X} \vDash \Psi_n, \end{align*}$$

whence $\mathsf {tr}(\Phi _{n})$ is logically equivalent to $\Psi _n$ over the class of posets. When $n = 1$ , the condition $\Psi _n$ expresses the demand that the principal upsets of $\mathbb {X}$ are up-directed.

By the same token, when $\Phi $ is the Sahlqvist quasiequation associated with the excluded middle axiom, $\mathsf {tr}(\Phi )$ expresses the demand that the poset $\mathbb {X}$ is discrete. Lastly, when $\Phi $ is the Sahlqvist quasiequation associated with the Gödel–Dummett axiom, $\mathsf {tr}(\Phi )$ is the sentence expressing the demand that $\mathbb {X}$ is a root system, i.e., that ${\uparrow }x$ is a chain, for every $x \in X$ (see [17, Proposition 2.36] or [52]).

Examples of quasiequations that cannot be rendered as Sahlqvist ones abound, however.

Example 4.14. The Scott axiom is the formula of $\mathsf {IPC}$

It is well known that the equation $\mathsf {Scott} \thickapprox 1$ is not canonical [73] (see also [47, Section 5]). By the Intuitionistic Sahlqvist Theorem, this means that this equation is not equivalent (over Heyting algebras) to any Sahlqvist quasiequation.

5 Sahlqvist theory for fragments of $\mathsf {IPC}$ with conjunction

Recall that $\mathcal {L}$ is the algebraic language of $\mathsf {IPC}$ , namely,

$$ \begin{align*} \mathcal{L} = x \mid \varphi \land \psi \mid \varphi \lor \psi \mid \varphi \to \psi \mid \lnot \varphi \mid 0 \mid 1. \end{align*} $$

The aim of this section is to extend Sahlqvist theory to fragments of $\mathsf {IPC}$ including the connective $\land $ . ⁸ As the correspondence part of Sahlqvist theorem is left unchanged by switching to fragments, the main result of this section takes the form of a canonicity result.

Theorem 5.1. Let $\Phi $ be a Sahlqvist quasiequation in a sublanguage $\mathcal {L}_\land $ of $\mathcal {L}$ containing $\land $ . If an $\mathcal {L}_\land $ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra validates $\Phi $ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\Phi $ .

In order to prove the above result, we begin by ruling out some limit cases.

Proposition 5.2. Let $\Phi $ be a Sahlqvist quasiequation in a language $\mathcal {L}_\land \subseteq \{ \land , \lor , 0, 1 \}$ . If an $\mathcal {L}_\land $ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra validates $\Phi $ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\Phi $ .

Proof It is well known that, in view of the poorness of the language $\mathcal {L}_\land $ , the class $\mathsf {K}$ of $\mathcal {L}_\land $ -subreducts of Heyting algebras is a minimal quasivariety. ⁹ This means that every quasiequation in $\mathcal {L}_\land $ is either true in $\mathsf {K}$ or false in all the nontrivial members of  $\mathsf {K}$ .

Suppose that $\Phi $ is valid in some ${\boldsymbol {A}} \in \mathsf {K}$ . If $\mathsf {K} \vDash \Phi $ , then $\Phi $ is also valid in the $\mathcal {L}_\land $ -reduct of the Heyting algebra $\mathsf {Up}({\boldsymbol {A}}_\ast )$ . This, in turn, implies that $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ as desired. Then we consider the case where $\Phi $ is false in all the nontrivial members of $\mathsf {K}$ . In this case, the assumption that ${\boldsymbol {A}} \vDash \Phi $ forces ${\boldsymbol {A}}$ to be trivial. Therefore, ${\boldsymbol {A}}_\ast $ is the empty poset and the Heyting algebra $\mathsf {Up}({\boldsymbol {A}}_\ast )$ is trivial. As a consequence, $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates every quasiequation and, in particular, $\Phi $ .

In order to prove Theorem 5.1, it only remains to consider the cases where $\mathcal {L}_\land $ contains $\land $ and either $\lnot $ or $\to $ . Up to term-equivalence, this amounts to proving that for every variety $\mathsf {K}$ among $\mathsf {PSL}, \mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ the following holds: for every Sahlqvist quasiequation $\Phi $ in the language of $\mathsf {K}$ and every ${\boldsymbol {A}} \in \mathsf {K}$ , if ${\boldsymbol {A}}$ validates $\Phi $ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\Phi $ .

The next result does this for the case where $\mathsf {K}$ is any variety among $\mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ (i.e., all cases except $\mathsf {K} = \mathsf {PSL})$ .

Proposition 5.3. Let $\mathsf {K}$ be a variety among $\mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ and $\Phi $ a Sahlqvist quasiequation in the language of $\mathsf {K}$ . For every ${\boldsymbol {A}} \in \mathsf {K}$ , if ${\boldsymbol {A}}$ validates $\Phi $ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\Phi $ .

Proof Consider a variety $\mathsf {K}$ among $\mathsf {(b)ISL}, \mathsf {PDL}$ , $\mathsf {IL}$ , and $\mathsf {HA}$ , a Sahlqvist quasiequation $\Phi $ in the language of $\mathsf {K}$ , and an algebra ${\boldsymbol {A}} \in \mathsf {K}$ such that ${\boldsymbol {A}} \vDash \Phi $ . By Theorem 2.7, ${\boldsymbol {A}}$ embeds into the appropriate reduct ${\boldsymbol {B}}^-$ of a Heyting algebra ${\boldsymbol {B}}$ such that ${\boldsymbol {B}}^- \in \mathbb {U}({\boldsymbol {A}})$ . Since $\Phi $ is a universal sentence valid in ${\boldsymbol {A}}$ , from ${\boldsymbol {B}}^- \in \mathbb {U}({\boldsymbol {A}})$ it follows ${\boldsymbol {B}}^- \vDash \Phi $ . As ${\boldsymbol {B}}^-$ is the reduct of ${\boldsymbol {B}}$ in the language of $\mathsf {K}$ , this guarantees that ${\boldsymbol {B}} \vDash \Phi $ .

Given that $\Phi $ is a Sahlqvist quasiequation, we can apply the canonicity part of the Intuitionistic Sahlqvist Theorem obtaining that $\mathsf {Up}({\boldsymbol {B}}_\ast ) \vDash \Phi $ . Since ${\boldsymbol {B}}_\ast = {\boldsymbol {B}}^-_\ast $ , the algebra $\mathsf {Up}_{\mathsf {K}}({\boldsymbol {B}}^{-}_\ast )$ is the reduct of $\mathsf {Up}({\boldsymbol {B}}_\ast )$ in the language of $\mathsf {K}$ . Consequently, from $\mathsf {Up}({\boldsymbol {B}}_\ast ) \vDash \Phi $ it follows that $\mathsf {Up}_{\mathsf {K}}({\boldsymbol {B}}_\ast ) \vDash \Phi $ .

Now, recall that there exists an embedding $f \colon {\boldsymbol {A}} \to {\boldsymbol {B}}^-$ . By Conditions (i) and (ii) of Proposition 3.5, the map $\mathsf {Up}_{\mathsf {K}}(f_\ast ) \colon \mathsf {Up}_{\mathsf {K}}({\boldsymbol {A}}_\ast ) \to \mathsf {Up}_{\mathsf {K}}({\boldsymbol {B}}^{-}_\ast )$ is a homomorphism between members of $\mathsf {K}$ . Furthermore, applying the last part of the same proposition to the assumption that f is injective, we obtain that $\mathsf {Up}_{\mathsf {K}}(f_\ast )$ is also injective, whence $\mathsf {Up}_{\mathsf {K}}({\boldsymbol {A}}_\ast ) \in \mathbb {I}\mathbb {S}(\mathsf {Up}_{\mathsf {K}}({\boldsymbol {B}}^{-}_\ast ))$ . Since the validity of universal sentences persists under the formation of subalgebras and isomorphic copies, from $\mathsf {Up}_{\mathsf {K}}({\boldsymbol {B}}^-_\ast ) \vDash \Phi $ it follows that $\mathsf {Up}_{\mathsf {K}}({\boldsymbol {A}}_\ast ) \vDash \Phi $ and, therefore, $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ , thus concluding the proof.

In order to complete the proof of Theorem 5.1, it only remains to prove the following:

Proposition 5.4. Let $\Phi $ be Sahlqvist quasiequation in the language of $\mathsf {PSL}$ . For every ${\boldsymbol {A}} \in \mathsf {PSL}$ , if ${\boldsymbol {A}}$ validates $\Phi $ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\Phi $ .

The proof result proceeds through a series of technical observations. An element a of a semilattice ${\boldsymbol {A}}$ is said to be join irreducible if it is not the minimum of ${\boldsymbol {A}}$ and for every pair of elements $b, c \in A$ such that the join $b \lor c$ exists in ${\boldsymbol {A}}$ , if $a = b \lor c$ , then either $a = b$ or $a = c$ . We denote by $\mathsf {J}({\boldsymbol {A}})$ the subposet of ${\boldsymbol {A}}$ whose universe is the set of join irreducible elements.

Lemma 5.5. The following conditions hold for a finite semilattice ${\boldsymbol {A}}:$

1. (i) If $a \nleqslant b$ , there exists $c \in \mathsf {J}({\boldsymbol {A}})$ such that $c \leqslant a$ and $c \nleqslant b$ .

2. (ii) An element $a \in A$ is the minimum of ${\boldsymbol {A}}$ iff there is no $c \in \mathsf {J}({\boldsymbol {A}})$ such that $c \leqslant a$ .

Proof This is an immediate consequence of the fact that every element of a finite semilattice ${\boldsymbol {A}}$ is the join of a subset of $\mathsf {J}({\boldsymbol {A}})$ .

Furthermore, we rely on the following properties of pseudocomplemented semilattices.

Lemma 5.6. The following conditions hold for every ${\boldsymbol {A}} \in \mathsf {PSL}:$

1. (i) If $\varphi (x_1, \dots , x_n)$ is a negative formula, the term function $\varphi ^{\boldsymbol {A}}(x_1, \dots , x_n)$ is order reversing in every argument, i.e., for every $a_1, \dots , a_n, b_1, \dots , b_n \in A$ ,

   $$\begin{align*}\text{if }a_i \leqslant b_i \text{ for every }i \leqslant n \text{, then }\varphi^{{\boldsymbol{A}}}(b_1, \dots, b_n) \leqslant \varphi^{{\boldsymbol{A}}}(a_1, \dots, a_n). \end{align*}$$

2. (ii) If ${\boldsymbol {A}}$ is finite and $X \subseteq A$ , the join $\bigvee X$ exists in ${\boldsymbol {A}}$ and $\bigwedge _{a \in X} \lnot a = \lnot \bigvee X$ .

Proof Condition (i) follows from the fact that $\lnot $ is order reversing in $\mathsf {PSL}$ [38, Condition (9)], while $\land $ is order preserving in both arguments. For Condition (ii), see [38, Condition (19)].

The following construction will be instrumental to deal with finite members of $\mathsf {PSL}$ .

Definition 5.7. With every finite semilattice ${\boldsymbol {A}}$ we associate an algebra

where $\mathsf {Dw}(\mathsf {J}({\boldsymbol {A}}))$ is the set of downsets of $\mathsf {J}({\boldsymbol {A}})$ and $\lnot $ is defined by

Furthermore, let $\epsilon _{\boldsymbol {A}} \colon {\boldsymbol {A}} \to {\boldsymbol {A}}^+$ be the map defined by the rule

Lemma 5.8. Let ${\boldsymbol {A}} \in \mathsf {PSL}$ be finite. Then ${\boldsymbol {A}}^+$ is the $\langle \land , \lnot , 0, 1 \rangle $ -reduct of a Heyting algebra, it belongs to $\mathsf {PSL}$ , and the map $\epsilon _{\boldsymbol {A}} \colon {\boldsymbol {A}} \to {\boldsymbol {A}}^+$ is an embedding.

Proof Notice that ${\boldsymbol {A}}^+$ coincides with the algebra $\mathsf {Up}_{\mathsf {PSL}}(\mathbb {X})$ , where $\mathbb {X}$ is the order dual of $\mathsf {J}({\boldsymbol {A}})$ . Since $\mathsf {Up}_{\mathsf {PSL}}(\mathbb {X})$ is a pseudocomplemented semilattice, we infer that so is ${\boldsymbol {A}}^+$ . Furthermore, the definition of ${\boldsymbol {A}}^+$ guarantees that it is a distributive lattice (whose join operation is $\cup $ ). Lastly, since ${\boldsymbol {A}}$ is finite, so is ${\boldsymbol {A}}^+$ . Therefore, ${\boldsymbol {A}}^+$ is a finite distributive pseudocomplemented lattice. By Proposition 2.5(i), we conclude that ${\boldsymbol {A}}^+$ is the $\langle \land , \lnot , 0, 1 \rangle $ -reduct of a Heyting algebra.

Then we turn to prove that $\epsilon _{\boldsymbol {A}} \colon {\boldsymbol {A}} \to {\boldsymbol {A}}^+$ is an embedding. Clearly, it is well defined and preserves $\land , 0$ , and $1$ . Furthermore, it is injective by Lemma 5.6(i). To prove that it also preserves $\lnot $ , consider $a \in A$ . We will prove that for every $b \in \mathsf {J}({\boldsymbol {A}})$ ,

$$ \begin{align*} b \in \lnot^{{\boldsymbol{A}}^+}\epsilon_{{\boldsymbol{A}}}(a) \, \,&\Longleftrightarrow \, \,\epsilon_{{\boldsymbol{A}}}(a) \cap {\downarrow}b = \emptyset \, \,\Longleftrightarrow \, \,c \nleqslant a \land^{\boldsymbol{A}} b, \text{ for every }c \in \mathsf{J}({\boldsymbol{A}})\\ \, \,& \Longleftrightarrow \, \, a \land^{\boldsymbol{A}} b = 0 \, \,\Longleftrightarrow \, \, b \leqslant \lnot^{\boldsymbol{A}} a \, \,\Longleftrightarrow\, \, b \in \epsilon_{{\boldsymbol{A}}}(\lnot^{{\boldsymbol{A}}} a). \end{align*} $$

The first of the above equivalences holds by the definition of $\lnot $ in ${\boldsymbol {A}}^+$ , the second and the last by the definition of $\epsilon _{\boldsymbol {A}}$ , the third by Lemma 5.6(ii), and the fourth by Condition (3). This shows that $\lnot ^{{\boldsymbol {A}}^+}\epsilon _{{\boldsymbol {A}}}(a) = \epsilon _{{\boldsymbol {A}}}(\lnot ^{{\boldsymbol {A}}} a)$ . Hence, we conclude that $\epsilon _{\boldsymbol {A}} \colon {\boldsymbol {A}} \to {\boldsymbol {A}}^+$ preserves $\lnot $ and, therefore, it is an embedding.

Remark 5.9. The embedding $\epsilon _{\boldsymbol {A}} \colon {\boldsymbol {A}} \to {\boldsymbol {A}}^+$ need not be an isomorphism, because ${\boldsymbol {A}}^+$ is always a distributive lattice, while the (semi)lattice ${\boldsymbol {A}}$ may fails to be distributive.

We rely on the following technical observation.

Lemma 5.10. Let ${\boldsymbol {A}} \in \mathsf {PSL}$ be finite and $\varphi (x_1,\dots ,x_n)$ a formula in the language of $\mathsf {PSL}$ . For every $D_1,\dots ,D_n \in \mathsf {Dw}(\mathsf {J}({\boldsymbol {A}}))$ , we have

$$\begin{align*}\lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+} (D_1,\dots,D_n) = \lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+}(\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1\bigg),\dots,\epsilon_{{\boldsymbol{A}}}\bigg(\bigvee^{\boldsymbol{A}} D_n\bigg)). \end{align*}$$

Proof. We begin by proving the following:

Claim 5.11. For every $D,V \in \mathsf {Dw}(\mathsf {J}({\boldsymbol {A}}))$ , we have

$$\begin{align*}\lnot^{{\boldsymbol{A}}^+}(D \cap V) = \lnot^{{\boldsymbol{A}}^+} \bigg(\epsilon_{{\boldsymbol{A}}}\bigg(\bigvee^{{\boldsymbol{A}}} D\bigg) \cap V\bigg). \end{align*}$$

Proof of the Claim

In order to prove the inclusion from right to left, observe that for every $a \in D$ we have $a \leqslant \bigvee ^{{\boldsymbol {A}}}D$ and, therefore, $a \in \epsilon _{{\boldsymbol {A}}}(\bigvee ^{{\boldsymbol {A}}} D)$ . Consequently, $D \subseteq \epsilon _{{\boldsymbol {A}}}(\bigvee ^{{\boldsymbol {A}}} D)$ . This, in turn, implies $D \cap V \subseteq \epsilon _{{\boldsymbol {A}}}(\bigvee ^{{\boldsymbol {A}}} D) \cap V$ . Bearing in mind that ${\boldsymbol {A}}^+ \in \mathsf {PSL}$ (Lemma 5.8), we can apply Lemma 5.6(i) obtaining that the operation $\lnot ^{{\boldsymbol {A}}^+}$ is order reversing. Thus, $\lnot ^{{\boldsymbol {A}}^+} (\epsilon _{{\boldsymbol {A}}}(\bigvee ^{{\boldsymbol {A}}} D) \cap V) \subseteq \lnot ^{{\boldsymbol {A}}^+}(D \cap V)$ as desired.

In order to prove the inclusion from left to right, we reason by contraposition. Consider $a \in \mathsf {J}({\boldsymbol {A}}) \smallsetminus \lnot ^{{\boldsymbol {A}}^+} (\epsilon _{{\boldsymbol {A}}}(\bigvee ^{{\boldsymbol {A}}} D) \cap V)$ . By the definitions of $\lnot ^{{\boldsymbol {A}}^+}$ and $\epsilon _{\boldsymbol {A}}$ , there exists $b \in V$ such that $b \leqslant \bigvee ^{{\boldsymbol {A}}} D, a$ . We have two cases depending on whether or not there exists $d \in D$ such that $b \nleqslant \lnot ^{{\boldsymbol {A}}}d$ .

Suppose first that such a d exists. In view of Condition (3) we get $0 < b \land ^{{\boldsymbol {A}}}d$ . Therefore, Lemma 5.5(ii) gives us some $c \in \mathsf {J}({\boldsymbol {A}})$ such that $c \leqslant b, d$ . Since $b \in V$ , $c \in \mathsf {J}({\boldsymbol {A}})$ , and V is a downset of $\mathsf {J}({\boldsymbol {A}})$ , we have $c \in V$ . Furthermore, from $c \leqslant d \leqslant \bigvee ^{{\boldsymbol {A}}}D$ and $c \in \mathsf {J}({\boldsymbol {A}})$ it follows that $c \in \epsilon _{{\boldsymbol {A}}}\big(\bigvee ^{{\boldsymbol {A}}}D\big)$ . Lastly, since $c \leqslant b \leqslant a$ , we have $c \in {\downarrow }a$ . Thus, $c \in \epsilon _{{\boldsymbol {A}}}\big(\bigvee ^{{\boldsymbol {A}}}D\big) \cap V \cap {\downarrow }a$ . By the definition of $\lnot ^{{\boldsymbol {A}}^+}$ , this amounts to $a \notin \lnot ^{{\boldsymbol {A}}^+}(\epsilon _{{\boldsymbol {A}}}\big(\bigvee ^{{\boldsymbol {A}}}D\big) \cap V)$ and we are done.

To conclude the proof, it only remains to show that the case where $b \leqslant \lnot ^{{\boldsymbol {A}}}d$ for every $d \in D$ never happens. Suppose the contrary. By Lemma 5.6(ii), we have

$$\begin{align*}b \leqslant \bigwedge^{{\boldsymbol{A}}}_{d \in D}\lnot d = \lnot^{{\boldsymbol{A}}} \bigvee^{{\boldsymbol{A}}}D. \end{align*}$$

As we assumed that $b \leqslant \bigvee ^{{\boldsymbol {A}}}D$ , this yields $b \leqslant \big(\bigvee ^{{\boldsymbol {A}}}D\big) \land ^{{\boldsymbol {A}}}\big(\lnot ^{{\boldsymbol {A}}} \bigvee ^{{\boldsymbol {A}}}D\big)$ which, by Condition (3), amounts to $b = 0$ . But this contradicts with the fact that $b \in \mathsf {J}({\boldsymbol {A}})$ .

To prove the main statement, we reason by induction on the construction of $\varphi $ . In the base case, $\varphi $ is either a constant or a variable. The case where $\varphi $ is a constant is straightforward. If $\varphi $ is a variable $x_i$ , by applying the claim in the third equality below, we obtain

$$ \begin{align*} \lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+} (D_1,\dots,D_n) &= \lnot^{{\boldsymbol{A}}^+}D_i = \lnot^{{\boldsymbol{A}}^+}(D_i \cap \mathsf{J}({\boldsymbol{A}})) = \lnot^{{\boldsymbol{A}}^+}\bigg(\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}}D_i\bigg) \cap \mathsf{J}({\boldsymbol{A}})\bigg) \\ &=\lnot^{{\boldsymbol{A}}^+}\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}}D_i\bigg)\kern-1pt = \lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+}\bigg(\kern-1pt\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1\bigg),\dots,\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_n\bigg)\!\!\bigg). \end{align*} $$

In the step case, the principal connective of $\varphi $ is either $\lnot $ or $\land $ . The case where it is $\lnot $ follows immediately from the inductive hypothesis. Therefore, we detail only the case where the principal connective of $\varphi $ is $\land $ . Since the operation $\land $ is associative and commutative in $\mathsf {PSL}$ , we may assume that $\varphi $ is of the form

$$\begin{align*}\lnot \alpha_1 \land \dots \land \lnot \alpha_{m} \land \beta_1 \land \dots \land \beta_k \land x_{i_1} \land \dots \land x_{i_t}, \end{align*}$$

where $i_1, \dots , i_t \leqslant n$ and each $\beta _j$ is a constant. Furthermore, $m, k$ , or t can be $0$ . As the inductive hypothesis applies to each $\alpha _j$ , we obtain

$$\begin{align*}\lnot^{{\boldsymbol{A}}^+}\alpha_j^{{\boldsymbol{A}}^+}(D_1, \dots, D_n) = \lnot^{{\boldsymbol{A}}^+}\alpha_j^{{\boldsymbol{A}}^+}\bigg(\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1\bigg),\dots,\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_n\bigg)\bigg), \text{ for every }j \leqslant m. \end{align*}$$

Furthermore, as the various $\beta _j$ are constants, we have

$$\begin{align*}\beta_j^{{\boldsymbol{A}}^+}(D_1, \dots, D_n) = \beta_j^{{\boldsymbol{A}}^+}\bigg(\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1\bigg),\dots,\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_n\bigg)\bigg), \text{ for every }j \leqslant k. \end{align*}$$

Therefore, setting

we obtain

$$\begin{align*}\lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+} (D_1,\dots,D_n) = \lnot^{{\boldsymbol{A}}^+}(D_{i_1} \cap \dots \cap D_{i_t} \cap V). \end{align*}$$

Lastly, applying t times the claim to the above display, we get

$$\begin{align*}\lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+} (D_1,\dots,D_n) = \lnot^{{\boldsymbol{A}}^+}\bigg(\epsilon_{{\boldsymbol{A}}}\bigg(\bigvee^{{\boldsymbol{A}}}D_{i_1}\bigg) \cap \dots \cap \epsilon_{{\boldsymbol{A}}}\bigg(\bigvee^{{\boldsymbol{A}}}D_{i_t}\bigg) \cap V\bigg) \end{align*}$$

which, by the definition of V, amounts to

$$\begin{align*}{} \lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+} (D_1,\dots,D_n) = \lnot^{{\boldsymbol{A}}^+} \varphi^{{\boldsymbol{A}}^+}\bigg(\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1\bigg),\dots,\epsilon_{{\boldsymbol{A}}}\bigg(\bigvee^{\boldsymbol{A}} D_n\bigg)\bigg). \\[-36pt] \end{align*}$$

The next result is the hearth of the proof of Proposition 5.4.

Proposition 5.12. Let ${\boldsymbol {A}} \in \mathsf {PSL}$ be finite and $\Phi $ a Sahlqvist quasiequation in the language of $\mathsf {PSL}$ . If ${\boldsymbol {A}}$ validates $\Phi $ , then also ${\boldsymbol {A}}^+$ validates $\Phi $ .

Proof We will reason by contraposition. Consider a Sahlqvist quasiequation

$$\begin{align*}\Phi = \varphi_1(x_1, \dots, x_k) \land y \leqslant z \, \& \dots \& \, \varphi_n(x_1, \dots, x_k) \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

in the language of $\mathsf {PSL}$ such that ${\boldsymbol {A}}^+ \nvDash \Phi $ . We need to prove that ${\boldsymbol {A}} \nvDash \Phi $ .

Since ${\boldsymbol {A}}^+$ is the $\langle \land , \lnot , 0, 1 \rangle $ -reduct of a Heyting algebra (Lemma 5.8), we can apply Corollary 4.7 to the assumption that ${\boldsymbol {A}}^+ \nvDash \Phi $ , obtaining $D_1, \dots , D_k \in \mathsf {Dw}(\mathsf {J}({\boldsymbol {A}}))$ such that

$$\begin{align*}\varphi_1^{{\boldsymbol{A}}^+}(D_1, \dots, D_k) \cup \dots \cup \varphi_n^{{\boldsymbol{A}}^+}(D_1, \dots, D_k) \ne \mathsf{J}({\boldsymbol{A}}). \end{align*}$$

Let then $a \in \mathsf {J}({\boldsymbol {A}})$ be such that

(9) $$ \begin{align} a \notin \varphi_1^{{\boldsymbol{A}}^+}(D_1, \dots, D_k) \cup \dots \cup \varphi_n^{{\boldsymbol{A}}^+}(D_1, \dots, D_k). \end{align} $$

Recall that ${\boldsymbol {A}}$ is a finite semilattice with a maximum and, therefore, it is also a lattice. Thereby, for every $m \leqslant k$ we can define an element of ${\boldsymbol {A}}$ as follows:

We will prove that

(10) $$ \begin{align} a \nleqslant (\varphi_1^{\boldsymbol{A}}(b_1, \dots, b_k) \land^{\boldsymbol{A}} a) \lor^{{\boldsymbol{A}}} \dots \lor^{{\boldsymbol{A}}} (\varphi_n^{\boldsymbol{A}}(b_1, \dots, b_k) \land^{\boldsymbol{A}} a). \end{align} $$

This, in turn, implies that ${\boldsymbol {A}} \nvDash \Phi $ , as witnessed by the assignment

$$\begin{align*}x_m \longmapsto b_m \quad y \longmapsto a \quad z \longmapsto(\varphi_1^{\boldsymbol{A}}(b_1, \dots, b_k) \land^{\boldsymbol{A}} a) \lor^{{\boldsymbol{A}}} \dots \lor^{{\boldsymbol{A}}} (\varphi_n^{\boldsymbol{A}}(b_1, \dots, b_k) \land^{\boldsymbol{A}} a). \end{align*}$$

Therefore, to conclude the proof, it suffices to establish Condition (10).

Suppose, with a view to contradiction, that Condition (10) fails. Then

$$\begin{align*}a = (\varphi_1^{\boldsymbol{A}}(b_1, \dots, b_k) \land^{\boldsymbol{A}} a) \lor^{{\boldsymbol{A}}} \dots \lor^{{\boldsymbol{A}}} (\varphi_n^{\boldsymbol{A}}(b_1, \dots, b_k) \land^{\boldsymbol{A}} a). \end{align*}$$

Since a is join irreducible, by symmetry we may assume that $a = \varphi _1^{\boldsymbol {A}}(b_1, \dots , b_k) \land ^{\boldsymbol {A}} a$ , that is,

(11) $$ \begin{align} a \leqslant \varphi_1^{\boldsymbol{A}}(b_1, \dots, b_k). \end{align} $$

Now, recall that $\varphi _1$ is obtained from Sahlqvist implications using only $\land , \lor $ , and $\Box $ . Since $\varphi _1$ is in the language of $\mathsf {PSL}$ , this means that $\varphi _1$ is a conjunction of Sahlqvist implications. Consequently, we may assume that

(12) $$ \begin{align} \varphi_1 = \bigwedge_{i \leqslant p} \gamma_j \land \bigwedge_{j \leqslant q} \lnot \psi_i, \end{align} $$

where the various $\gamma _i$ and $\psi _j$ are, respectively, Sahlqvist antecedents and positive formulas, both in the language of $\mathsf {PSL}$ . Furthermore, p or q can be $0$ . Without loss of generality, we may assume each $\gamma _i$ is a variable. This is because if $\gamma _i = \lnot \alpha $ then $\alpha $ is a negative formula and, therefore, a Sahlqvist antecedent. Consequently, we may assume that $\gamma _i = \lnot \psi _j$ for some $j \leqslant q$ and remove $\gamma _i$ from the big conjunction on the left-hand side of the above display. On the other hand, if $\gamma _i = \alpha \land \beta $ , then both $\alpha $ and $\beta $ are positive formulas and, therefore, we may assume that there are $i_1, i_2 \leqslant p$ such that $\gamma _{i_1} = \alpha $ and $\gamma _{i_2} = \beta $ and remove $\gamma _i$ from the big conjunction on the left-hand side of the above display. Iterating this process, we may assume that in the above display every $\gamma _i$ is either a constant or a variable, while the various $\psi _j$ are still Sahlqvist antecedents. Lastly, if some $\gamma _i$ is the constant $1$ , we can remove it from the big conjunction on the left-hand side of the above display, thereby producing a new formula that is still equivalent to $\varphi _1$ in $\mathsf {PSL}$ . This is possible because $\varphi _1$ cannot simply be the constant $1$ , otherwise Condition (10) would hold, contradicting the assumption. Moreover, no $\gamma _i$ is the constant $0$ , otherwise Condition (11) would imply that $a = 0$ , contradicting the assumption that $a \in \mathsf {J}({\boldsymbol {A}})$ . Therefore, we may assume that each $\gamma _i$ in Condition (12) is a variable. In addition, we may also assume that the various $\gamma _i$ are pairwise distinct and, renaming the variables when necessary, that each $\gamma _i$ is the variable $x_i$ , thereby obtaining

$$\begin{align*}\varphi_1 = x_{1} \land \dots \land x_{p} \land \lnot \psi_1 \land \dots \land \lnot \psi_q, \end{align*}$$

where the various $\psi _j$ are Sahlqvist antecedents in the language of $\mathsf {PSL}$ .

In view of Condition (11), this yields

(13) $$ \begin{align} a \leqslant b_{1} \land^{{\boldsymbol{A}}} \dots \land^{{\boldsymbol{A}}} b_{p} \land^{{\boldsymbol{A}}} \lnot \psi_1^{{\boldsymbol{A}}}(b_1, \dots, b_k) \land^{{\boldsymbol{A}}} \dots \land^{{\boldsymbol{A}}} \lnot \psi_q^{{\boldsymbol{A}}}(b_1, \dots, b_k). \end{align} $$

On the other hand, from Condition (9) it follows that

$$\begin{align*}a \notin D_{1} \cap \dots \cap D_{p} \cap \lnot^{{\boldsymbol{A}}^+} \psi_1^{{\boldsymbol{A}}^+}(D_1, \dots, D_k) \cap \dots \cap \lnot^{{\boldsymbol{A}}^+} \psi_q^{{\boldsymbol{A}}^+}(D_1, \dots, D_k). \end{align*}$$

We have two cases depending on whether

$$\begin{align*}a \notin D_{1} \cap \dots \cap D_{p}\, \, \text{ or }\, \, a \notin \lnot^{{\boldsymbol{A}}^+} \psi_1^{{\boldsymbol{A}}^+}(D_1, \dots, D_k) \cap \dots \cap \lnot^{{\boldsymbol{A}}^+} \psi_q^{{\boldsymbol{A}}^+}(D_1, \dots, D_k). \end{align*}$$

Suppose first that $a \notin D_{1} \cap \dots \cap D_{p}$ . By symmetry, we may assume that $a \notin D_{1}$ . From Condition (13) and the definition of $b_{1}$ it follows that

$$\begin{align*}a \leqslant b_{1} = \bigvee_{d \in D_{1}}^{{\boldsymbol{A}}}(d \land^{{\boldsymbol{A}}} a). \end{align*}$$

This amounts to $a = \bigvee _{d \in D_{1}}^{{\boldsymbol {A}}}(d \land ^{{\boldsymbol {A}}} a)$ which, in turn, implies that $a \leqslant d$ for some $d \in D_{1}$ because $a \in \mathsf {J}({\boldsymbol {A}})$ . Since $a \in \mathsf {J}({\boldsymbol {A}})$ and $D_{1}$ is a downset of $\mathsf {J}({\boldsymbol {A}})$ , we conclude that $a \in D_{1}$ , a contradiction.

Then we consider the case where $a \notin \lnot ^{{\boldsymbol {A}}^+} \psi _1^{{\boldsymbol {A}}^+}(D_1, \dots , D_k) \cap \dots \cap \lnot ^{{\boldsymbol {A}}^+} \psi _q^{{\boldsymbol {A}}^+} (D_1, \dots , D_k)$ . By symmetry, we may assume that $a \notin \lnot ^{{\boldsymbol {A}}^+} \psi _1^{{\boldsymbol {A}}^+}(D_1, \dots , D_k)$ . Applying in sequence Lemma 5.10 and the fact that $\epsilon _{\boldsymbol {A}} \colon {\boldsymbol {A}} \to {\boldsymbol {A}}^+$ is a homomorphism (Lemma 5.8), we deduce

$$ \begin{align*} a &\notin \lnot^{{\boldsymbol{A}}^+} \psi_1^{{\boldsymbol{A}}^+}(D_1, \dots, D_k) \\ &= \lnot^{{\boldsymbol{A}}^+} \psi_1^{{\boldsymbol{A}}^+}\bigg(\epsilon_{\boldsymbol{A}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1\bigg),\dots,\epsilon_{{\boldsymbol{A}}}\bigg(\bigvee^{\boldsymbol{A}} D_k\bigg)\bigg)\\ & = \epsilon_{{\boldsymbol{A}}}\bigg(\lnot^{{\boldsymbol{A}}} \psi_1^{{\boldsymbol{A}}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1, \dots, \bigvee^{{\boldsymbol{A}}} D_k\bigg)\bigg). \end{align*} $$

Since $a \in \mathsf {J}({\boldsymbol {A}})$ , by the definition of $\epsilon _{\boldsymbol {A}}$ this amounts to

(14) $$ \begin{align} a \nleqslant \lnot^{{\boldsymbol{A}}} \psi_1^{{\boldsymbol{A}}}\bigg(\bigvee^{{\boldsymbol{A}}} D_1, \dots, \bigvee^{{\boldsymbol{A}}} D_k\bigg). \end{align} $$

Now, as $\psi _1$ is a Sahlqvist antecedent in the language of $\mathsf {PSL}$ , it is a conjunction of variables, negative formulas, and constants. As before, we can remove the constants from this conjunction. Therefore, we may assume that $\psi _1$ is of the form

(15) $$ \begin{align} x_{1} \land \dots \land x_{p'} \land \alpha_1 \land \dots \land \alpha_{q'}, \end{align} $$

where the various $\alpha _j$ are negative formulas. Furthermore, $p'$ or $q'$ can be $0$ .

As the various $\alpha _j$ are negative formulas, the term function $\alpha _j^{\boldsymbol {A}}$ is order reversing in every argument by Lemma 5.6(i). Bearing in mind that for every $m \leqslant k$ we have

$$\begin{align*}b_m = \bigvee^{{\boldsymbol{A}}}_{d \in D_m} (d \land^{{\boldsymbol{A}}} a) \leqslant \bigvee^{\boldsymbol{A}} D_m, \end{align*}$$

this implies that for every $j \leqslant q'$ ,

$$\begin{align*}\alpha_j^{{\boldsymbol{A}}}\bigg(\bigvee^{{\boldsymbol{A}}}D_1, \dots, \bigvee^{{\boldsymbol{A}}}D_k\bigg) \leqslant \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k). \end{align*}$$

Since $\psi _1$ is the formula in Condition (15), we obtain

$$\begin{align*}\psi_1^{{\boldsymbol{A}}}\bigg(\bigvee^{{\boldsymbol{A}}}D_1, \dots, \bigvee^{{\boldsymbol{A}}}D_k\bigg) \leqslant \bigwedge^{{\boldsymbol{A}}}_{i \leqslant p'}\bigvee^{{\boldsymbol{A}}}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k). \end{align*}$$

By applying the fact that the negation operation is order reversing in $\mathsf {PSL}$ to the above display and Condition (14), we obtain

$$\begin{align*}a \nleqslant \lnot^{\boldsymbol{A}}\Big(\bigwedge^{{\boldsymbol{A}}}_{i \leqslant p'}\bigvee^{{\boldsymbol{A}}}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k)\Big). \end{align*}$$

In view of Condition (3), this amounts to

(16) $$ \begin{align} 0 < a \land^{\boldsymbol{A}} \bigwedge_{i \leqslant p'} \bigvee^{{\boldsymbol{A}}}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k). \end{align} $$

We will prove that

(17) $$ \begin{align} 0 < a \land^{\boldsymbol{A}} b_{1} \land^{\boldsymbol{A}} \bigvee^{{\boldsymbol{A}}}_{2 \leqslant i \leqslant p'}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k). \end{align} $$

By applying Condition (3) to Condition (16) and, subsequently, Lemma 5.6(ii), we obtain

$$\begin{align*}a \land^{\boldsymbol{A}}\bigvee^{{\boldsymbol{A}}}_{2 \leqslant i \leqslant p'}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k) \nleqslant \lnot \bigvee^{{\boldsymbol{A}}}D_{1} = \bigwedge^{{\boldsymbol{A}}}_{d \in D_{1}} \lnot^{\boldsymbol{A}} d. \end{align*}$$

Consequently, there exists $d_1 \in D_{1}$ such that

$$\begin{align*}a \land^{\boldsymbol{A}}\bigvee^{{\boldsymbol{A}}}_{2 \leqslant i \leqslant p'}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k) \nleqslant \lnot^{\boldsymbol{A}} d_1. \end{align*}$$

By applying Condition (3) twice, this yields

(18) $$ \begin{align} a\land^{\boldsymbol{A}}\bigvee^{{\boldsymbol{A}}}_{2 \leqslant i \leqslant p'}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k) \nleqslant \lnot^{{\boldsymbol{A}}}(d_1 \land^{\boldsymbol{A}} a). \end{align} $$

By the definition of $b_{1}$ and Lemma 5.6(ii) we have

$$\begin{align*}\lnot^{\boldsymbol{A}} b_{1} = \lnot^{\boldsymbol{A}} \bigvee^{\boldsymbol{A}}_{d \in D_{1}}(d \land^{\boldsymbol{A}} a) = \bigwedge^{\boldsymbol{A}}_{d \in D_{1}}(\lnot^{{\boldsymbol{A}}}(d \land^{\boldsymbol{A}} a)) \leqslant \lnot^{{\boldsymbol{A}}}(d_1 \land^{\boldsymbol{A}} a). \end{align*}$$

Together with Condition (18), this yields

$$\begin{align*}a\land^{\boldsymbol{A}}\bigvee^{{\boldsymbol{A}}}_{2 \leqslant i \leqslant p'}D_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k) \nleqslant \lnot^{\boldsymbol{A}} b_{1}. \end{align*}$$

By Condition (3) this amounts to Condition (17) as desired.

Iterating $p-1$ times the argument described for Condition (17), where the role of $D_1$ is taken successively by $D_2, \dots , D_{p'}$ , we obtain

$$\begin{align*}0 < a \land^{\boldsymbol{A}} \bigwedge^{\boldsymbol{A}}_{i \leqslant p'} b_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k). \end{align*}$$

By Condition (3) and the fact that $\psi _1$ is the formula in Condition (15) this amounts to

$$\begin{align*}a \nleqslant \lnot^{\boldsymbol{A}}\bigg(\bigwedge^{\boldsymbol{A}}_{i \leqslant p'} b_{i} \land^{\boldsymbol{A}} \bigwedge^{{\boldsymbol{A}}}_{j \leqslant q'} \alpha_j^{{\boldsymbol{A}}}(b_1, \dots, b_k)\bigg) = \lnot^{\boldsymbol{A}} \psi_1^{\boldsymbol{A}}(b_1, \dots, b_k), \end{align*}$$

a contradiction with Conditions (11) and (12).

We are now ready to conclude the proof of Proposition 5.4.

Proof Suppose that ${\boldsymbol {A}} \vDash \Phi $ . In view of Proposition 2.8, the finitely generated subalgebras of ${\boldsymbol {A}}$ are finite. Therefore, we can apply Lemma 5.8 obtaining that every finitely generated subalgebra ${\boldsymbol {C}}$ of ${\boldsymbol {A}}$ embeds into ${\boldsymbol {C}}^+$ . Together with Proposition 2.9, this implies that there exist a family $\{ {\boldsymbol {A}}_i : i \in I \}$ of finitely generated subalgebras of ${\boldsymbol {A}}$ and an ultrafilter U on I with an embedding

$$\begin{align*}f \colon {\boldsymbol{A}} \to \prod_{i \in I}{\boldsymbol{A}}_i^+ /U. \end{align*}$$

Consider $i \in I$ . Since the validity of universal sentences persists in subalgebras, from ${\boldsymbol {A}} \vDash \Phi $ it follows ${\boldsymbol {A}}_i \vDash \Phi $ . Therefore, Proposition 5.12 guarantees that ${\boldsymbol {A}}_i^+\vDash \Phi $ . As a consequence, all the factors of the ultraproduct in the above display validate $\Phi $ . Since the validity of universal sentences persists in ultraproducts, we conclude that ${\boldsymbol {B}}^{-} \vDash \Phi $ for .

Now, recall from Lemma 5.8 that each ${\boldsymbol {A}}_i^+$ is the $\langle \land , \lnot , 0, 1 \rangle $ -reduct of a Heyting algebra ${\boldsymbol {B}}_i$ . Therefore, ${\boldsymbol {B}}^-$ is the $\langle \land , \lnot , 0, 1 \rangle $ -reduct of the ultraproduct . As $\Phi $ is in the language of $\mathsf {PSL}$ and ${\boldsymbol {B}}^- \vDash \Phi $ , this implies that ${\boldsymbol {B}} \vDash \Phi $ . Lastly, since $\mathsf {HA}$ is closed under , we have ${\boldsymbol {B}} \in \mathsf {HA}$ .

In sum, ${\boldsymbol {A}}$ embeds into some ${\boldsymbol {B}}^- \in \mathsf {PSL}$ that is the $\langle \land , \lnot , 0, 1 \rangle $ -reduct of a Heyting algebra ${\boldsymbol {B}}$ such that ${\boldsymbol {B}} \vDash \Phi $ . Because of this, we can repeat the argument detailed in the last two paragraphs of the proof of Proposition 5.3, thereby obtaining $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ .

As a consequence of Theorem 5.1, we obtain the following:

Corollary 5.13. Let $\Phi $ be a Sahlqvist quasiequation in a sublanguage $\mathcal {L}_\land $ of $\mathcal {L}$ containing $\land $ . For every $\mathcal {L}_\land $ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra, it holds that ${\boldsymbol {A}} \vDash \Phi \text { iff } {\boldsymbol {A}}_\ast \vDash \mathsf {tr}(\Phi )$ .

Proof In view of the correspondence part of the Intuitionistic Sahlqvist Theorem, we have that $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ iff ${\boldsymbol {A}}_\ast \vDash \mathsf {tr}(\Phi )$ . Therefore, in order to complete the proof, it suffices to show that ${\boldsymbol {A}} \vDash \Phi $ iff $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ .

On the one hand, Theorem 5.1 guarantees that ${\boldsymbol {A}} \vDash \Phi $ implies $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ . On the other hand, $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ implies ${\boldsymbol {A}} \vDash \Phi $ , because ${\boldsymbol {A}}$ embeds into the $\mathcal {L}_\land $ -reduct of $\mathsf {Up}({\boldsymbol {A}}_\ast )$ via the map defined by the rule

$$\begin{align*}a \longmapsto \{ F \in {\boldsymbol{A}}_\ast : a \in F \} \end{align*}$$

and¹⁰ the validity of universal sentences persists in subalgebras.

Example 5.14. In view of Example 4.13 and Corollary 5.13, a pseudocomplemented semilattice ${\boldsymbol {A}}$ validates the Sahlqvist quasiequation $\Phi _n$ associated with the bounded top width n axiom $\mathsf {btw}_n$ iff every $(n+1)$ -element antichain in a principal upset of ${\boldsymbol {A}}_\ast $ is below one that has at most n elements.

6 Abstract algebraic logic

In this section we will review the rudiments of abstract algebraic logic necessary to formulate a version of Sahlqvist theory amenable to arbitrary deductive systems [19, 26, 35, 36]. Recall that $Var$ is the set of variables $\{ x_n : n \in \mathbb {Z}^+ \}$ . A logic (or a deductive system) $\vdash $ is a consequence relation on the set of formulas with variables in $Var$ of an algebraic language that, moreover, is substitution invariant, in the sense that for every set $\Gamma \cup \{ \varphi \}$ of formulas and substitution $\sigma $ ,

$$\begin{align*}\text{if }\Gamma \vdash \varphi, \text{ then }\sigma[\Gamma] \vdash \sigma(\varphi). \end{align*}$$

Furthermore, we will assume that logics $\vdash $ are finitary, in the sense that

$$\begin{align*}\text{if }\Gamma \vdash \varphi \text{, there exists a finite }\Sigma \subseteq \Gamma \text{ s.t. }\Sigma \vdash \varphi. \end{align*}$$

We denote the set of formulas over which a logic $\vdash $ is defined and the corresponding algebra of formulas by $Fm(\vdash )$ and $\boldsymbol {Fm}(\vdash )$ , respectively. In addition, given $\Gamma \cup \{ \varphi _1, \dots , \varphi _n, \psi _1, \dots , \psi _m \} \subseteq Fm(\vdash )$ , we often write $\Gamma , \varphi _1, \dots , \varphi _n \vdash \psi _1, \dots , \psi _m$ to signify that $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \} \vdash \psi _i$ for every $i \leqslant m$ .

Henceforth, we will assume that the algebras and logics under consideration are of the same similarity type. Let $\vdash $ be a logic and ${\boldsymbol {A}}$ an algebra. A subset F of A is said to be a deductive filter of $\vdash $ on ${\boldsymbol {A}}$ when for every $\Gamma \cup \{ \varphi \} \subseteq Fm(\vdash )$ such that $\Gamma \vdash \varphi $ and every homomorphism $f \colon \boldsymbol {Fm}(\vdash ) \to {\boldsymbol {A}}$ ,

$$\begin{align*}\text{if }f[\Gamma] \subseteq F, \text{ then } f(\varphi) \in F. \end{align*}$$

Example 6.1. If ${\boldsymbol {A}}$ is a Heyting algebra, the deductive filters of $\mathsf {IPC}$ on ${\boldsymbol {A}}$ coincide with the lattice filters of ${\boldsymbol {A}}$ .

The set $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ of deductive filters of $\vdash $ on ${\boldsymbol {A}}$ is a closure system on A, whence for every $X \subseteq A$ there exists the least deductive filter of $\vdash $ on ${\boldsymbol {A}}$ containing X, in symbols $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({X})$ . Given $a_1,\dots ,a_n \in A$ , we often write $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({a_1,\dots ,a_n})$ as a shorthand for $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\{a_1,\dots ,a_n\}})$ . Furthermore, when ordered under the inclusion relation, $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ is a complete lattice in which meets are intersections and joins are defined for every $F, G \in \mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ as

When ${\boldsymbol {A}} = \boldsymbol {Fm}(\vdash )$ , we will omit the superscript ${\boldsymbol {A}}$ from $+^{\boldsymbol {A}}$ and $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({-})$ .

In order to describe the structure of the lattice $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ , recall that an element a of a complete lattice ${\boldsymbol {B}}$ is called compact when for every $X \subseteq B$ ,

$$\begin{align*}\text{if }a \leqslant \bigvee X\text{, there exists a finite }Y \subseteq X \text{ s.t. }a \leqslant \bigvee Y. \end{align*}$$

Notice that if two elements $a,b \in B$ are compact, then so is their join $a \lor b$ . Consequently, when endowed with the restriction of the operation $\lor $ , the set of the compact elements of ${\boldsymbol {B}}$ forms a semilattice ordered, in the sense of Condition (2), under the restriction of the dual of the lattice order of ${\boldsymbol {B}}$ . Lastly, a complete lattice ${\boldsymbol {B}}$ is said to be algebraic when every element is the join of a set of compact ones. We will rely on the following classical representation theorem for algebraic lattices:

Theorem 6.2 [51, Theorem 42].

Every algebraic lattice is isomorphic to the lattice of filters of the semilattice of its compact elements.

We denote the set of compact elements of $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ by $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ .

Remark 6.3. When endowed with the restriction of the operation $+^{\boldsymbol {A}}$ , the set $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ forms a semilattice ordered under the superset relation.

In order to describe the elements of $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ , we say that a deductive filter $F \in \mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ is finitely generated when there exists a finite set $X \subseteq A$ such that $F = \mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({X})$ .

Proposition 6.4. Let $\vdash $ be a logic and ${\boldsymbol {A}}$ an algebra. Then $\langle \mathsf {Fi}_\vdash ({{\boldsymbol {A}}}); \cap , +^{\boldsymbol {A}} \rangle $ is an algebraic lattice whose compact elements are the finitely generated ones.

Proof This well-known fact is essentially [35, Theorem 2.23.1].

Example 6.5. In view of the above result and Example 6.1, the compact deductive filters of $\mathsf {IPC}$ on a Heyting algebra ${\boldsymbol {B}}$ coincide with the finitely generated lattice filters of ${\boldsymbol {B}}$ . Since the latter are precisely the principal upsets of ${\boldsymbol {B}}$ and the order of the semilattice $\mathsf {Fi}_{\mathsf {IPC}}^\omega ({\boldsymbol {B}})$ is the superset relation (see Remark 6.3), we conclude that the poset associated with the semilattice $\mathsf {Fi}_{\mathsf {IPC}}^\omega ({\boldsymbol {B}})$ is isomorphic to the lattice order of ${\boldsymbol {B}}$ .

Among the deductive filters of $\vdash $ , those on $\boldsymbol {Fm}(\vdash )$ will be of special interest. They are called theories and coincide with the sets $\Gamma \subseteq Fm(\vdash )$ such that $\varphi \in \Gamma $ for every $\varphi \in Fm(\vdash )$ with $\Gamma \vdash \varphi $ . The algebraic lattice of theories of $\vdash $ will be denoted by $\mathsf {Th}({\vdash })$ and the semilattice of its compact elements by $\mathsf {Th}^\omega ({\vdash })$ .

The structure of compact deductive filters (resp. theories) can be used to capture the validity of various metalogical properties, as we proceed to explain. A finite set $\Gamma \subseteq Fm(\vdash )$ is said to be inconsistent in a logic $\vdash $ if $\Gamma \vdash \varphi $ for every $\varphi \in Fm(\vdash )$ .

Definition 6.6. A logic $\vdash $ is said to have:

1. (i) The inconsistency lemma (IL, for short) when for every $n \in \mathbb {Z}^+$ there exists a finite set $\thicksim _n\!\!(x_1, \dots , x_n) \subseteq Fm(\vdash )$ such that

   

   for every finite $\Gamma \cup \{\varphi _1,\dots ,\varphi _1\} \subseteq Fm(\vdash )$ .

2. (ii) The deduction theorem (DT, for short) when for every $n, m \in \mathbb {Z}^+$ there exists a finite set $(x_1, \dots , x_n)\!\Rightarrow _{nm}\!\!(y_1, \dots , y_m) \subseteq Fm(\vdash )$ such that

   

   for every finite $\Gamma \cup \{\varphi _1,\dots ,\varphi _n,\psi _1,\dots ,\psi _m\} \subseteq Fm(\vdash )$ .

3. (iii) The proof by cases (PC, for short) when for every $n, m \in \mathbb {Z}^+$ there exists a finite set such that

   

   for every finite $\Gamma \cup \{\varphi _1,\dots ,\varphi _n,\psi _1,\dots ,\psi _m, \gamma \} \subseteq Fm(\vdash )$ . ¹¹

Example 6.7. The logic $\mathsf {IPC}$ has the IL, the DT, and the PC witnessed, respectively, by the sets:

for every $n,m \in \mathbb {Z}^+$ .

Henceforth, we will focus on the following class of logics [8, 24–26]:

Definition 6.8. A logic $\vdash $ is said to be protoalgebraic if there exists a nonempty ¹² finite set $\Delta (x, y)$ of formulas such that

$$\begin{align*}\emptyset \vdash \Delta(x, x) \, \, \text{ and } \, \, x, \Delta(x, y) \vdash y. \end{align*}$$

The class of protoalgebraic logics embraces most of the traditional logics. This is because if a logic $\vdash $ possesses a term-definable connective $\to $ such that $\emptyset \vdash x \to x$ and $x, x \to y \vdash y$ (as it is the case for $\mathsf {IPC}$ ), then it is protoalgebraic, as witnessed by the set .

For protoalgebraic logics $\vdash $ , the IL, the DT, and the PC admit a transparent description in terms of the structure of the semilattices $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ of compact deductive filters (see Remark 6.3). More precisely, we have the following:

Theorem 6.9 [67, Theorem 3.7].

Let $\vdash $ be a protoalgebraic logic. The following conditions are equivalent $:$

1. (i) The logic $\vdash $ has the inconsistency lemma.

2. (ii) The semilattice $\mathsf {Th}^\omega ({\vdash })$ is pseudocomplemented.

3. (iii) The semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is pseudocomplemented, for every algebra ${\boldsymbol {A}}$ .

Furthermore, if the inconsistency lemma for $\vdash $ is witnessed by , then the operation $\lnot $ of the pseudocomplemented semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is defined as follows $:$ for every $a_1, \dots , a_n \in A$ ,

$$\begin{align*}\lnot \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1, \dots, a_n}) = \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\thicksim^{{\boldsymbol{A}}}_n \!\!(a_1, \dots, a_n)}). \end{align*}$$

The ¹³ next result is [24, Theorem 2.11] (see also [10–12]).

Theorem 6.10. Let $\vdash $ be a protoalgebraic logic. The following conditions are equivalent $:$

1. (i) The logic $\vdash $ has the deduction theorem.

2. (ii) The semilattice $\mathsf {Th}^\omega ({\vdash })$ is implicative.

3. (iii) The semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is implicative, for every algebra ${\boldsymbol {A}}$ .

Furthermore, if the deduction theorem for $\vdash $ is witnessed by , then the operation $\to $ of the implicative semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is defined as follows $:$ for every $a_1, \dots , a_n, b_1, \dots , b_m \in A$ ,

$$\begin{align*}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1, \dots, a_n}) \to \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({b_1, \dots, b_m}) = \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({(a_1, \dots, a_n)\!\Rightarrow_{nm}^{{\boldsymbol{A}}} \!\!(b_1, \dots, b_m)}). \end{align*}$$

Lastly, the next result originates in [23] (see also [27] and [26, Section 2.5]).

Theorem 6.11. Let $\vdash $ be a protoalgebraic logic. The following conditions are equivalent $:$

1. (i) The logic $\vdash $ has the proof by cases.

2. (ii) The semilattice $\mathsf {Th}^\omega ({\vdash })$ is a distributive lattice.

3. (iii) The semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is a distributive lattice, for every algebra ${\boldsymbol {A}}$ .

In this case, the lattice structure of the poset associated with the semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is $\langle \mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}}); +^{\boldsymbol {A}}, \cap \rangle $ . ¹⁴ Furthermore, if the proof by cases for $\vdash $ is witnessed by

, then for every $a_1, \dots , a_n, b_1, \dots , b_m \in A$ ,

Remark 6.12. As we mentioned, $\mathsf {IPC}$ is protoalgebraic and it has the IL, the DT, and the PC. Therefore Condition (iii) of Theorems 6.9, 6.10, and 6.11 holds for $\mathsf {IPC}$ . This should not come as a surprise, at least in the case where ${\boldsymbol {A}}$ is a Heyting algebra. This is because, in view of Example 6.5, the poset underlying $\mathsf {Fi}_{\mathsf {IPC}}^\omega ({\boldsymbol {A}})$ is isomorphic to the lattice order of the Heyting algebra ${\boldsymbol {A}}$ , which is obviously pseudocomplemented, implicative, and distributive.

7 Sahlqvist theory for protoalgebraic logics

The aim of this section is to extend Sahlqvist theory to protoalgebraic logics. To this end, it is convenient to introduce some terminology. A formula $\varphi $ is said to be a theorem of a logic $\vdash $ when $\emptyset \vdash \varphi $ .

Remark 7.1. Every protoalgebraic logic $\vdash $ has a theorem $\top (x)$ . To prove this, let $\Delta (x, y)$ be the set witnessing the protoalgebraicity of $\vdash $ . Since $\Delta (x, y)$ is nonempty, we can choose a formula $\varphi (x, y) \in \Delta (x, y)$ . The definition of a protoalgebraic logic guarantees that $\emptyset \vdash \Delta (x, x)$ and, therefore, that $\emptyset \vdash \varphi (x, x)$ . Thus, setting , we are done.

Recall that $\mathcal {L}$ is the algebraic language of $\mathsf {IPC}$ .

Definition 7.2. A formula $\varphi $ of $\mathcal {L}$ is compatible with a protoalgebraic logic $\vdash $ when:

1. (i) If $0$ or $\lnot $ occurs in $\varphi $ , then $\vdash $ has the IL.

2. (ii) If $\to $ occurs in $\varphi $ , then $\vdash $ has the DT.

3. (iii) If $\lor $ occurs in $\varphi $ , then $\vdash $ has the PC.

Remark 7.3. Every formula of $\mathcal {L}$ is compatible with $\mathsf {IPC}$ , because $\mathsf {IPC}$ has the IL, the DT, and the PC in view of Example 6.7.

Remark 7.4. Let $\varphi (x_1, \dots , x_n)$ be a formula of $\mathcal {L}$ compatible with a protoalgebraic logic $\vdash $ . In view of Condition (iii) of Theorems 6.9, 6.10, and 6.11, the formula $\varphi $ can be interpreted in the semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ , thus inducing a term-function

$$\begin{align*}\varphi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})} \colon \mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})^n \to \mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}}) \end{align*}$$

on every algebra ${\boldsymbol {A}}$ .

If the logic $\vdash $ in the next definition has the IL (resp. the DT or the PC), we denote the finite sets of formulas witnessing this property by $\thicksim _n\!\!(x_1, \dots , x_n)$ (resp. $(x_1, \dots , x_n)\!\Rightarrow _{nm}\!\!(y_1, \dots , y_m)$ or ).

Definition 7.5. With every $n \in \mathbb {Z}^+$ and formula $\varphi (x_1, \dots , x_n)$ of $\mathcal {L}$ that is compatible with a protoalgebraic logic $\vdash $ and every $k \in \mathbb {Z^+}$ we will associate a finite set

$$\begin{align*}\boldsymbol{\varphi}^k(x_1^1, \dots, x_1^k, \dots, x_n^1, \dots, x_n^k) \end{align*}$$

of formulas of $\vdash $ . The case where $\varphi $ is a variable $x_m$ or a constant is handled as follows:

where $\top (x)$ is a theorem of $\vdash $ (see Remark 7.1). ¹⁵ When $\varphi $ is a complex formula, we proceed as follows:

1. (i) If $\varphi = \psi \land \chi $ , we set

   

2. (ii) If $\varphi = \lnot \psi $ and $\boldsymbol {\psi }^k = \{ \psi _1, \dots , \psi _m \}$ , we set

   

3. (iii) If $\varphi = \psi \to \chi $ , $\boldsymbol {\psi }^k = \{\psi _1,\dots ,\psi _m\}$ , and $\boldsymbol {\chi }^k = \{\chi _1,\dots ,\chi _t\}$ , we set

   

4. (iv) If $\varphi = \psi \lor \chi $ , $\boldsymbol {\psi }^k = \{\psi _1,\dots ,\psi _m\}$ , and $\boldsymbol {\chi }^k = \{\chi _1,\dots ,\chi _t\}$ , we set

   

Example 7.6. In view of Remark 7.3, the formula $\varphi = x_1 \to x_2$ is compatible with $\mathsf {IPC}$ . Therefore, we can associate with $\varphi $ and every $k \in \mathbb {Z}^+$ a finite set $\boldsymbol {\varphi }^k$ of formulas of $\mathsf {IPC}$ . The construction of $\boldsymbol {\varphi }^k$ depends on the sets of formulas witnessing the DT for $\mathsf {IPC}$ , described in Example 6.7. As a result, we obtain

$$\begin{align*}{}\boldsymbol{\varphi}^k = \{ x_1^1 \to (x_1^2 \to ( \dots ( x_1^k \to x_2^i)\dots)) : i \leqslant k \}. \\[-32pt] \end{align*}$$

The connection between $\varphi (x_1, \dots , x_n)$ and $\boldsymbol {\varphi }^k(x_1^1, \dots , x_1^k, \dots , x_n^1, \dots , x_n^k)$ is made apparent by the following observation, where the function

$$\begin{align*}\varphi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})} \colon \mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})^n \to \mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}}) \end{align*}$$

should be interpreted as in Remark 7.4.

Lemma 7.7. Let $\varphi (x_1, \dots , x_n)$ be a formula of $\mathcal {L}$ compatible with a protoalgebraic logic $\vdash $ . For every algebra ${\boldsymbol {A}}$ , every $k \in \mathbb {Z}^+$ , and every $a_1^1, \dots , a_1^k, \dots , a_n^1, \dots , a_n^k \in A$ , it holds

$$\begin{align*}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\varphi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}) = \varphi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}),\dots,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k})). \end{align*}$$

Proof The proof proceeds by induction on the construction of $\varphi $ . In the base case, $\varphi $ is either a variable $x_m$ or one of the constants $1$ and $0$ . The case of $x_m$ follows immediately from the definition of $\boldsymbol {x_m}^k$ . Therefore, we only detail the cases of $1$ and  $0$ .

On the one hand, we have that

$$ \begin{align*} \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{1}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}) &= \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\top(a_1^1)})\\ & = 1^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}\\ &= 1^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}),\dots,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k})). \end{align*} $$

The first equality above holds by the definition of $\boldsymbol {1}^k$ and the third is straightforward. To prove the second, recall that $\top (x_1^1)$ is a theorem of $\vdash $ and, therefore, $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\top (a_1^1)})$ is the least compact deductive filter of $\vdash $ on ${\boldsymbol {A}}$ . As $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is ordered under the superset relation (see Remark 6.3), this implies that $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\top ^{\boldsymbol {A}}(a_1^1)})$ is the top element of the semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ , that is, $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\top ^{\boldsymbol {A}}(a_1^1)}) = 1^{\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})}$ .

On the other hand, we have that

The equalities above are justified as follows: the first holds by the definition of $\boldsymbol {0}^{k}$ , the second by the definition of $+^{\boldsymbol {A}}$ and $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({-})$ , the third by the last part of Theorem 6.9, the fourth by the fact that, in view of Theorem 6.9(iii), $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is a pseudocomplemented semilattice and, therefore, $0$ is term-definable as $x \land \lnot x$ , and the last one is straightforward.

In the inductive step, $\varphi $ is a complex formula. If $\varphi = \psi \land \chi $ , we have that

$$ \begin{align*} & \,\,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\varphi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}) \\ = & \,\,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({(\boldsymbol{\psi \land \chi})^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}) \\ =& \,\,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\psi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k) \cup\boldsymbol{\chi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k) })\\ =& \,\,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\psi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}) +^{\boldsymbol{A}} \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\chi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k) })\\ =& \,\,\psi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}),\dots,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k}))\\&\hspace{3pt} +^{\boldsymbol{A}}\chi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}),\dots,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k}))\\ =& \,\,\varphi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}),\dots,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k})). \end{align*} $$

The first equality above holds because $\varphi = \psi \land \chi $ , the second by the definition of $(\boldsymbol {\psi \land \chi })^{k}$ , the third by the definition of $+^{\boldsymbol {A}}$ and $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({-})$ , the fourth by the inductive hypothesis, and the last one because $\varphi = \psi \land \chi $ and $+^{\boldsymbol {A}}$ is the operation of the semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ .

It only remains to consider the cases where $\varphi $ is of the form $\lnot \psi $ , $\psi \to \chi $ , or $\psi \lor \chi $ . Since they are handled essentially in the same way, we only detail the case where $\varphi = \lnot \psi $ . Suppose that $\boldsymbol {\psi }^k = \{ \chi _1, \dots , \chi _m \}$ . Then we have that

$$ \begin{align*} & \,\,\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\varphi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}) \\ =& \, \, \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({(\boldsymbol{\lnot \psi})^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)})\\ = & \, \, \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\sim_m\!\!(\chi_1^{\boldsymbol{A}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k), \dots, \chi_m^{\boldsymbol{A}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k))}) \\ = & \, \, \lnot^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\chi_1^{\boldsymbol{A}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k), \dots, \chi_m^{\boldsymbol{A}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)})\\ = & \, \, \lnot^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\psi}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)})\\ = & \, \, \lnot^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})} \psi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}), \dots, \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k}))\\ = & \, \, \varphi^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})} (\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}), \dots, \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k})). \end{align*} $$

The first equality above holds because $\varphi = \lnot \psi $ , the second by the definition of $(\boldsymbol {\lnot \psi })^k$ and the assumption that $\boldsymbol {\psi }^k = \{ \chi _1, \dots , \chi _m \}$ , the third by the last part of Theorem 6.9, the fourth by the assumption that $\boldsymbol {\psi }^k = \{ \chi _1, \dots , \chi _m \}$ , and the fifth by the inductive hypothesis, and the last one because $\varphi = \lnot \psi $ .

The notion of compatibility can be extended to Sahlqvist quasiequations as follows:

Definition 7.8. A Sahlqvist quasiequation $(\varphi _1 \land y \leqslant z \, \& \dots \& \, \varphi _m \land y \leqslant z) \Longrightarrow y \leqslant z$ is said to be compatible with a protoalgebraic logic $\vdash $ if so are $\varphi _1, \dots , \varphi _m$ .

In the case of protoalgebraic logics, the role of Sahlqvist quasiequations is played by the following metarules:

Definition 7.9. Given a Sahlqvist quasiequation

$$\begin{align*}\Phi = \varphi_1(x_1, \dots, x_n) \land y \leqslant z \, \& \dots \& \, \varphi_m(x_1, \dots, x_n) \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

compatible with a protoalgebraic logic $\vdash $ , let $\mathsf {R}_\vdash (\Phi )$ be the set of metarules of the form

where $k \in \mathbb {Z}^+$ and $\Gamma \cup \{ \psi \} \cup \{ \gamma _i^j : i \leqslant n, j \leqslant k \}$ is a finite subset of $Fm(\vdash )$ .

We rely on the following observation, which generalizes [60, Theorem 5.3].

Proposition 7.10. The following conditions are equivalent for a Sahlqvist quasiequation $\Phi $ compatible with a protoalgebraic logic $\vdash :$

1. (i) The logic $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ .

2. (ii) The semilattice $\mathsf {Th}^\omega ({\vdash })$ validates $\Phi $ .

3. (iii) The semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ validates $\Phi $ , for every algebra ${\boldsymbol {A}}$ .

The proof of Proposition 7.10 depends on the next well-known property of protoalgebraic logics.

Proposition 7.11 [35, Proposition 6.12].

Let $\vdash $ be a protoalgebraic logic, ${\boldsymbol {A}}$ an algebra, and $X \cup \{a\} \subseteq A$ . Then $a \in \mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({X})$ iff there exist a finite $\Gamma \cup \{\varphi \} \subseteq Fm(\vdash )$ and a homomorphism $f \colon \boldsymbol {Fm}(\vdash ) \to {\boldsymbol {A}}$ such that $\Gamma \vdash \varphi $ , $f[\Gamma ] \subseteq X \cup \mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\emptyset })$ , and $f(\varphi ) = a$ .

Proof of Proposition 7.10

Throughout the proof we will assume that

$$\begin{align*}\Phi = \varphi_1(x_1, \dots, x_n) \land y \leqslant z \, \& \dots \& \, \varphi_m(x_1, \dots, x_n) \land y \leqslant z \Longrightarrow y \leqslant z. \end{align*}$$

(ii) $\Rightarrow $ (i): Let $k \in \mathbb {Z}^+$ and let $\Gamma \cup \{ \psi \} \cup \{ \gamma _i^j : i \leqslant n, j \leqslant k \}$ be a finite subset of $Fm(\vdash )$ such that

(19) $$ \begin{align} \Gamma \, {\cup} \, \boldsymbol{\varphi_i}^k(\gamma_1^1, \dots, \gamma_1^k, \dots, \gamma_n^1, \dots, \gamma_n^k) \vdash \psi, \text{ for every } i \leqslant m. \end{align} $$

We want to prove that $\Gamma \vdash \psi $ .

Consider $i \leqslant m$ . We have that

$$ \begin{align*} \mathsf{Fg}_\vdash({\psi}) &\subseteq \mathsf{Fg}_\vdash({\Gamma \cup \boldsymbol{\varphi_i}^k(\gamma_1^1, \dots, \gamma_1^k, \dots, \gamma_n^1, \dots, \gamma_n^k)})\\ &=\mathsf{Fg}_\vdash({\Gamma}) + \mathsf{Fg}_\vdash({\boldsymbol{\varphi_i}^k(\gamma_1^1, \dots, \gamma_1^k, \dots, \gamma_n^1, \dots, \gamma_n^k)})\\ &=\mathsf{Fg}_\vdash({\Gamma}) + \varphi_i^{\mathsf{Th}^\omega({\vdash})}(\mathsf{Fg}_\vdash({\gamma_1^1, \dots, \gamma_1^k}), \dots, \mathsf{Fg}_\vdash({\gamma_n^1, \dots, \gamma_n^k})), \end{align*} $$

where the first step follows from Condition (19), the second from the definition of $\mathsf {Fg}_\vdash ({-})$ and $+$ , and the last one from Lemma 7.7.

Since the semilattice $\mathsf {Th}^\omega ({\vdash })$ is ordered under the superset relation and its operation is $+$ (see Remark 6.3), the above display yields

$$\begin{align*}\mathsf{Fg}_\vdash({\Gamma}) \land^{\mathsf{Th}^\omega({\vdash})}\varphi_i^{\mathsf{Th}^\omega({\vdash})}(\mathsf{Fg}_\vdash({\gamma_1^1, \dots, \gamma_1^k}), \dots, \mathsf{Fg}_\vdash({\gamma_n^1, \dots, \gamma_n^k})) \leqslant \mathsf{Fg}_\vdash({\psi}). \end{align*}$$

As this holds for every $i \leqslant m$ , we can apply the assumption that $\mathsf {Th}^\omega ({\vdash })$ validates $\Phi $ , obtaining $\mathsf {Fg}_\vdash ({\Gamma }) \leqslant \mathsf {Fg}_\vdash ({\psi })$ . But, since the order of $\mathsf {Th}^\omega ({\vdash })$ is the superset relation, this amounts to $\mathsf {Fg}_\vdash ({\psi }) \subseteq \mathsf {Fg}_\vdash ({\Gamma })$ , whence $\Gamma \vdash \psi $ as desired.

(iii) $\Rightarrow $ (ii): This implication is straightforward, since $\mathsf {Th}^\omega ({\vdash }) = \mathsf {Fi}_\vdash ^\omega ({\boldsymbol {Fm}(\vdash )})$ .

(i) $\Rightarrow $ (iii): Let ${\boldsymbol {A}}$ be an algebra and let $F, G_1,\dots ,G_{n}, H\in \mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ be such that

(20) $$ \begin{align} H \subseteq F +^{\boldsymbol{A}} \varphi_{i}^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(G_1,\dots,G_{n}) \text{, for every }i \leqslant m. \end{align} $$

We want to prove that $H \subseteq F$ .

Recall that $\vdash $ has theorems, because it is protoalgebraic (see Remark 7.1). Consequently, $G_1, \dots , G_n$ are nonempty. Furthermore, they are finitely generated. This is because, in view of Proposition 6.4, compact and finitely generated deductive filters coincide. Therefore, there are $k \in \mathbb {Z}^+$ and $a_1^1, \dots , a_1^k, \dots , a_n^1, \dots , a_n^k \in A$ such that

$$\begin{align*}G_1 = \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1^1, \dots, a_1^k}), \dots, G_n = \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_n^1, \dots, a_n^k}). \end{align*}$$

Together with Lemma 7.7, this implies that

(21) $$ \begin{align} \varphi_{i}^{\mathsf{Fi}_\vdash^\omega({{\boldsymbol{A}}})}(G_1,\dots,G_{n}) = \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\varphi_i}^k(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}), \text{ for every }i \leqslant m. \end{align} $$

In order to prove that $H \subseteq F$ , let $a \in H$ . From Conditions (20) and (21) it follows that

$$\begin{align*}a \in F +^{\boldsymbol{A}} \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\boldsymbol{\varphi_i}^k(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)}), \text{ for every }i \leqslant m. \end{align*}$$

Thus, from Proposition 7.11 we deduce that for each $i \leqslant m$ there exists a homomorphism $f_i \colon \boldsymbol {Fm}(\vdash ) \to {\boldsymbol {A}}$ and a finite set $\Psi _i \cup \{\psi _i\} \subseteq Fm(\vdash )$ such that

(22) $$ \begin{align} \Psi_i \vdash \psi_i, \, \, \, f_i[\Psi_i] \subseteq F \cup \boldsymbol{\varphi_i}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k), \, \, \text{ and } \,\, f_i(\psi_i) = a. \end{align} $$

As the sets $\Psi _1, \dots , \Psi _m$ are finite and $\vdash $ is substitution invariant, we may assume, without loss of generality, that if $i < j \leqslant m$ , then the set of variables occurring in the members of $\Psi _i \cup \{\psi _i\}$ is disjoint from the set of variables occurring in the members of $\Psi _j \cup \{\psi _j\}$ . Consequently, we may also assume that $f_1 = \dots = f_m$ . Accordingly, from now on, we will denote these maps by f and drop the subscripts. Lastly, we may assume that there exists a set of variables $\{ z_j^t : j \leqslant n, t \leqslant k \}$ not occurring in any $\Psi _i \cup \{ \psi _i \}$ such that $f(z_j^t) = a_j^t$ for every $j \leqslant n$ and $t \leqslant k$ .

Now, in view of Condition (22), we can split each $\Psi _i$ into two subsets $\Psi _i^1$ and $\Psi _i^2$ such that

(23) $$ \begin{align} f[\Psi_i^1] \subseteq F, \quad f[\Psi_i^2] \subseteq \boldsymbol{\varphi_i}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k), \,\, \text{ and } \, \,\Psi_i = \Psi_i^1 \cup \Psi_i^1. \end{align} $$

We will construct a finite set $\Gamma \subseteq f^{-1}[F]$ as follows. First, we stipulate that ${\Psi _1^1 \cup \dots \cup \Psi _m^1 \subseteq \Gamma }$ , as the above display guarantees that $\Psi _1^1 \cup \dots \cup \Psi _m^1 \subseteq f^{-1}[F]$ .

Then let $\Delta (x, y)$ be the finite set of formulas witnessing the protoalgebraicity of $\vdash $ . We will make extensive use of the observation that, since $\emptyset \vdash \Delta (x, x)$ and F is a deductive filter, we have that $\Delta ^{{\boldsymbol {A}}}(b, b) \subseteq F$ for every $b \in F$ .

Recall from Condition (22) that $f(\psi _1) = \dots = f(\psi _m) = a$ . Therefore,

$$\begin{align*}f[\bigcup_{i, j \leqslant m}\Delta(\psi_i, \psi_j)] = \Delta^{\boldsymbol{A}}(a, a) \subseteq F \end{align*}$$

and so we may assume that $\Gamma $ contains $\bigcup \{ \Delta (\psi _i, \psi _j) : i, j \leqslant m \}$ . Moreover, by Condition (23), we have that

$$\begin{align*}f[\Psi_i^2] \subseteq \boldsymbol{\varphi_i}^{k{\boldsymbol{A}}}(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)\text{, for every }i \leqslant m. \end{align*}$$

Accordingly, for every $i \leqslant m$ and $\alpha \in \Psi _i^2$ , there exists a formula $\beta _\alpha \in \boldsymbol {\varphi _i}^{k}(z_1^1, \dots , z_1^k, \dots , z_n^1, \dots , z_n^k)$ such that

$$ \begin{align*} f(\alpha) &= \beta_\alpha(a_1^1, \dots, a_1^k, \dots, a_n^1, \dots, a_n^k)\\ &= \beta_\alpha(f(z_1^1), \dots, f(z_1^k), \dots, f(z_n^1), \dots, f(z_n^k))\\ & = f(\beta_\alpha) \end{align*} $$

and, therefore, $f[\Delta (\beta _\alpha , \alpha )] \subseteq F$ . Consequently, we can add the sets $\Delta (\beta _\alpha , \alpha )$ to $\Gamma $ , thereby completing its definition.

To conclude the proof, it suffices to show that

(24) $$ \begin{align} \Gamma \cup \boldsymbol{\varphi_i}^k(z_1^1, \dots, z_1^k, \dots, z_n^1, \dots, z_n^k) \vdash \psi_1, \text{ for every }i \leqslant m. \end{align} $$

For if this is the case, the assumption that $\vdash $ validates the rules in $\mathsf {R}_\vdash (\Phi )$ implies that $\Gamma \vdash \psi _1$ . Moreover, since $f[\Gamma ] \subseteq F$ and F is a deductive filter, we deduce $a = f(\psi _1) \in F$ as desired.

Accordingly, we turn to prove Condition (24). Consider $i \leqslant m$ . First, observe that

(25) $$ \begin{align} \Gamma \, {\cup} \, \boldsymbol{\varphi_i}^k(z_1^1, \dots, z_1^k, \dots, z_n^1, \dots, z_n^k) \vdash \Psi_i^1, \end{align} $$

because $\Psi _i^1 \subseteq \Gamma $ . We will prove that

(26) $$ \begin{align} \Gamma \cup \boldsymbol{\varphi_i}^k(z_1^1, \dots, z_1^k, \dots, z_n^1, \dots, z_n^k) \vdash \Psi_i^2. \end{align} $$

To this end, consider a formula $\alpha \in \Psi _i^2$ . By the construction of $\Gamma $ , we have

$$\begin{align*}\beta_\alpha \in \boldsymbol{\varphi_i}^k(z_1^1, \dots, z_1^k, \dots, z_n^1, \dots, z_n^k) \, \, \text{ and } \, \, \Delta(\beta_\alpha,\alpha) \subseteq \Gamma. \end{align*}$$

As the definition of a protoalgebraic logic gives $\beta _\alpha , \Delta (\beta _\alpha , \alpha ) \vdash \alpha $ , the above display guarantees that $\Gamma \cup \boldsymbol {\varphi _i}^k(z_1^1, \dots , z_1^k, \dots , z_n^1, \dots , z_n^k) \vdash \alpha $ , thereby establishing Condition (26).

Now, recall that $\Psi _i = \Psi _i^1 \cup \Psi _i^2$ and $\Psi _i \vdash \psi _i$ (see Conditions (22) and (23), if necessary). Together with the Conditions (25) and (26), this yields

$$\begin{align*}\Gamma \cup \boldsymbol{\varphi_i}^k(z_1^1, \dots, z_1^k, \dots, z_n^1, \dots, z_n^k) \vdash \psi_i. \end{align*}$$

Finally, since by the construction of $\Gamma $ we have $\Delta (\psi _i,\psi _1) \subseteq \Gamma $ and, by protoalgebraicity, $\psi _i, \Delta (\psi _i, \psi _1) \vdash \psi _1$ , we conclude that $\Gamma \vdash \psi _1$ .

Remark 7.12. A logic $\vdash $ is said to have a conjunction if it possesses a term-definable binary connective $\land $ such that

$$\begin{align*}x, y \vdash x \land y \qquad x \land y \vdash x \qquad x \land y \vdash y. \end{align*}$$

In this case, for every algebra ${\boldsymbol {A}}$ and $a_1, \dots , a_n \in A$ ,

$$\begin{align*}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a_1, \dots, a_n}) = \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({ a_1 \land \dots \land a_n }). \end{align*}$$

Consequently, the members of $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ are precisely the principal deductive filters of $\vdash $ on ${\boldsymbol {A}}$ , i.e., the sets of the form $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({a})$ for some $a \in A$ .

As a consequence, if the logic $\vdash $ in the statement of Proposition 7.10 has a conjunction, then the positive integer k in the proof of the implication (i) $\Rightarrow $ (iii) can be taken to be $1$ . Accordingly, for logics $\vdash $ with a conjunction, Condition (i) of Proposition 7.10 can be replaced by the simpler demand that $\vdash $ validates the metarules of the form

where $\Gamma \cup \{ \psi \} \cup \{ \gamma _1, \dots , \gamma _n \}$ is a finite subset of $Fm(\vdash )$ .

A similar simplification is possible when the logic $\vdash $ has the DT or the PC, as we proceed to explain. Suppose first that $\vdash $ has the DT. Given two finite subsets $\Gamma = \{ \varphi _1, \dots , \varphi _n \}$ and $\Sigma = \{ \psi _1, \dots , \psi _m \}$ of $Fm(\vdash )$ , we will write

$$\begin{align*}\Gamma \Rightarrow \Sigma\,\, \text{ as a shorthand for }\,\, (\varphi_1, \dots, \varphi_n)\Rightarrow_{nm}(\psi_1, \dots, \psi_m), \end{align*}$$

where $\Rightarrow _{nm}$ is one of the sets witnessing the DT for $\vdash $ . In the presence of the DT, Condition (i) of Proposition 7.10 becomes equivalent to the simpler demand that

(27) $$ \begin{align} ((\boldsymbol{\varphi_1}^k \Rightarrow y) \cup \dots \cup (\boldsymbol{\varphi_m}^k \Rightarrow y)) \Rightarrow y \end{align} $$

is a set of theorems of $\vdash $ for every $k \in \mathbb {Z}^+$ , where y is a variable that does not occur in any $\boldsymbol {\varphi _i}^k = \boldsymbol {\varphi _i}^k(x_1^1, \dots , x_1^k, \dots , x_n^1, \dots , x_n^k)$ . We leave the easy proof, which relies only on the basic properties of the DT, to the reader.

Lastly, we turn to the case where $\vdash $ has the PC. Given finite subsets $\Gamma _1 = \{ \varphi _1, \dots , \varphi _{n_1} \}, \dots , \Gamma _m = \{ \varphi _1, \dots , \varphi _{n_m} \}$ of $Fm(\vdash )$ , we will define recursively a finite set

of formulas, for every $2 \leqslant p \leqslant m$ . First, if $p =2$ , we let

where

is one of the sets witnessing the PC for $\vdash $ . On the other hand, if $2 < p < m$ and

, we let

In the presence of the PC, Condition (i) of Proposition 7.10 becomes equivalent to the simpler demand that

(28)

is a set of theorems of $\vdash $ for every $k \in \mathbb {Z}^+$ . ¹⁶ Also in this case, we leave the easy proof, which relies only on the basic properties of the PC, to the reader.

Sahlqvist theory for protoalgebraic logics centers on the following notion.

Definition 7.13. Let $\vdash $ be a logic and ${\boldsymbol {A}}$ an algebra. The spectrum of ${\boldsymbol {A}}$ relative to $\vdash $ , in symbols $\mathsf {Spec}_{\vdash }({\boldsymbol {A}})$ , is the poset of meet irreducible deductive filters of $\vdash $ on ${\boldsymbol {A}}$ ordered under the inclusion relation. When ${\boldsymbol {A}} = \boldsymbol {Fm}(\vdash )$ , we write $\mathsf {Spec}(\vdash )$ as a shorthand for $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ .

Remark 7.14. In view of Remark 3.3 and Example 6.1, the spectrum of a Heyting algebra ${\boldsymbol {A}}$ relative to $\mathsf {IPC}$ is the poset of prime filters of ${\boldsymbol {A}}$ .

Our main result establishes a correspondence between the validity of the metarules of the form $\mathsf {R}_\vdash (\Phi )$ and the structure of spectra $\mathsf {Spec}_{\vdash }({\boldsymbol {A}})$ . ¹⁷

Abstract Sahlqvist Theorem 7.15. The following conditions are equivalent for a Sahlqvist quasiequation $\Phi $ compatible with a protoalgebraic logic $\vdash :$

1. (i) The logic $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ .

2. (ii) $\mathsf {Spec}(\vdash ) \vDash \mathsf {tr}(\Phi )$ .

3. (iii) $\mathsf {Spec}_\vdash ({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi )$ , for every algebra ${\boldsymbol {A}}$ .

Proof (i) $\Rightarrow $ (iii): Let ${\boldsymbol {A}}$ be an algebra. By applying Proposition 7.10 to the assumption that $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ , we obtain that the semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ validates $\Phi $ .

Then let $\mathcal {L}_\land $ be the sublanguage of $\mathcal {L}$ consisting of the connectives of $\mathsf {IPC}$ that occur in $\Phi $ with the addition of $\land $ . As $\Phi $ is compatible with $\vdash $ , from Theorems 6.9, 6.10, and 6.11 it follows that $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is an $\mathcal {L}_\land $ -subreduct of a Heyting algebra. Furthermore, observe that $\Phi $ is a Sahlqvist quasiequation in $\mathcal {L}_\land $ . Therefore, we can apply Corollary 5.13 obtaining that $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})_\ast \vDash \mathsf {tr}(\Phi )$ .

Now, recall from Proposition 6.4 that the lattice $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ is algebraic. Therefore, from Theorem 6.2 we deduce that $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ is isomorphic to the lattice of filters of the semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ . Thus, the poset of meet irreducible elements of $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ , namely $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ , is isomorphic to the poset of meet irreducible filters of $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ , namely $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})_\ast $ . Consequently, from $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})_\ast \vDash \mathsf {tr}(\Phi )$ it follows that $\mathsf {Spec}_\vdash ({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi )$ as desired.

(iii) $\Rightarrow $ (ii): Straightforward.

(ii) $\Rightarrow $ (i): Assume $\mathsf {Spec}(\vdash ) \vDash \mathsf {tr}(\Phi )$ . As in the proof of the implication (i) $\Rightarrow $ (iii), we have $\mathsf {Spec}(\vdash ) \cong \mathsf {Th}^\omega ({\vdash })_\ast $ . Consequently, we obtain $\mathsf {Th}^\omega ({\vdash })_\ast \vDash \mathsf {tr}(\Phi )$ . Now, let $\mathcal {L}_\land $ be the language defined in the proof of the implication (i) $\Rightarrow $ (iii). The same argument shows that $\mathsf {Th}^\omega ({\vdash })$ is an $\mathcal {L}_\land $ -subreduct of a Heyting algebra and that $\Phi $ is a Sahlqvist quasiequation in $\mathcal {L}_\land $ . Therefore, we can apply Corollary 5.13 to $\mathsf {Th}^\omega ({\vdash })_\ast \vDash \mathsf {tr}(\Phi )$ , obtaining that $\mathsf {Th}^\omega ({\vdash }) \vDash \Phi $ . Lastly, by Proposition 7.10 we conclude that $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ as desired.

Under additional assumptions, the Abstract Sahlqvist Theorem can be formulated in a more algebraic fashion. Given a quasivariety $\mathsf {K}$ and an algebra ${\boldsymbol {A}}$ , we say that a congruence $\theta $ of ${\boldsymbol {A}}$ is a $\mathsf {K}$ -congruence of ${\boldsymbol {A}}$ when ${\boldsymbol {A}} / \theta \in \mathsf {K}$ . When ordered under the inclusion relation, the set of $\mathsf {K}$ -congruences of ${\boldsymbol {A}}$ forms an algebraic lattice, which we denote by $\mathsf {Con}_{\mathsf {K}}({\boldsymbol {A}})$ . The poset of meet irreducible elements of $\mathsf {Con}_{\mathsf {K}}({\boldsymbol {A}})$ will then be denoted by $\mathsf {Spec}_{\mathsf {K}}({\boldsymbol {A}})$ .

A logic $\vdash $ is algebraized [9] by a quasivariety $\mathsf {K}$ when there exist finite sets $\Delta (x, y)$ and $\tau (x)$ of formulas and equations, respectively, such that

$$\begin{align*}\mathsf{K} \vDash x \thickapprox y \, \,\text{ iff } \, \,\{ \epsilon(\varphi) \thickapprox \delta(\varphi) : \epsilon \thickapprox \delta \in \tau \text{ and } \varphi \in \Delta \} \end{align*}$$

and, for every finite $\Gamma \cup \{ \varphi \} \subseteq Fm(\vdash )$ ,

In this case, for every algebra ${\boldsymbol {A}}$ , the lattices $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ and $\mathsf {Con}_{\mathsf {K}}({\boldsymbol {A}})$ are isomorphic (see, e.g., [35, Theorem 3.58]) and, therefore, so are $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ and $\mathsf {Spec}_{\mathsf {K}}({\boldsymbol {A}})$ . Furthermore, the set of formulas $\Delta (x, y)$ witnesses the protoalgebraicity of $\vdash $ .

Example 7.16. The intuitionistic propositional calculus $\mathsf {IPC}$ is algebraized by the variety $\mathsf {HA}$ of Heyting algebras, as witnessed by the sets $\Delta = \{ x \to y, y \to x \}$ and $\tau = \{ x \thickapprox 1 \}$ .

Corollary 7.17. Let $\Phi $ be a Sahlqvist quasiequation compatible with a logic $\vdash $ that is algebraized by a quasivariety $\mathsf {K}$ . Then $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ iff $\mathsf {Spec}_{\mathsf {K}}({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi )$ , for every ${\boldsymbol {A}} \in \mathsf {K}$ .

Proof The “only if” part follows from the implication (i) $\Rightarrow $ (iii) of the Abstract Sahlqvist Theorem and the observation that $\mathsf {Spec}_\vdash ({\boldsymbol {A}}) \cong \mathsf {Spec}_{\mathsf {K}}({\boldsymbol {A}})$ , for every algebra ${\boldsymbol {A}}$ . To prove the “if” part, suppose that $\mathsf {Spec}_{\mathsf {K}}({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi )$ , for every ${\boldsymbol {A}} \in \mathsf {K}$ . Then consider an algebra ${\boldsymbol {A}}$ , not necessarily in $\mathsf {K}$ . By the Correspondence Theorem for quasivarieties, there exists ${\boldsymbol {B}} \in \mathsf {K}$ such that $\mathsf {Spec}_{\mathsf {K}}({\boldsymbol {A}}) \cong \mathsf {Spec}_{\mathsf {K}}(\boldsymbol {B})$ (see, e.g., [13, Thm. II.6.20]). Together with the assumption, this implies that $\mathsf {Spec}_{\mathsf {K}}({\boldsymbol {A}})\vDash \mathsf {tr}(\Phi )$ , thus establishing Condition (iii) of the Abstract Sahlqvist Theorem. By the implication (iii) $\Rightarrow $ (i) of the same theorem, we conclude that $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ as desired.

8 The excluded middle and the bounded top width laws

We proceed to illustrate how the Abstract Sahlqvist Theorem can be used to obtain concrete correspondence results, some known and some new.

Definition 8.1. A logic $\vdash $ is said to have the excluded middle law (EML, for short) when for every $n \in \mathbb {Z}^+$ there exists a finite set $\sim _n\!\!(x_1, \dots , x_n) \subseteq Fm(\vdash )$ such that

$$\begin{align*}\{ x_1, \dots, x_n \} \, \cup \sim_n\!\!(x_1, \dots, x_n) \text{ is inconsistent} \end{align*}$$

and the metarule

is valid in $\vdash $ , for every finite $\Gamma \cup \{ \varphi _1, \dots , \varphi _n, \psi \} \subseteq Fm(\vdash )$ .

Remark 8.2. Every logic with the EML has the IL, as witnessed by the sets $\sim _n\!\!(x_1, \dots , x_n)$ .

In the presence of the IL, the semantic counterpart of the EML is the following property:

Definition 8.3. A logic $\vdash $ is said to be semisimple when the order of $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ is the identity relation, for every algebra ${\boldsymbol {A}}$ .

Theorem 8.4 [66].

A protoalgebraic logic has the excluded middle law iff it has the inconsistent lemma and is semisimple.

Proof In view of Remark 8.2, it suffices to prove that a protoalgebraic logic $\vdash $ with the IL has the EML iff it is semisimple. Accordingly, let $\{ \sim _n\!\!(x_1, \dots , x_n) : n \in \mathbb {Z}^+ \}$ be a family of sets witnessing the IL for $\vdash $ . Moreover, observe that the Sahlqvist quasiequation

$$\begin{align*}\Phi = x \land y \leqslant z \, \& \, \lnot x \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

corresponding to the excluded middle axiom $x \lor \lnot x$ is compatible with $\vdash $ , because $\vdash $ has the IL.

Now, recall from Example 4.13 that a poset validates $\mathsf {tr}(\Phi )$ iff its order is the identity relation. Consequently, $\vdash $ is semisimple iff $\mathsf {Spec}_{\vdash }({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi )$ , for every algebra ${\boldsymbol {A}}$ . By the Abstract Sahlqvist Theorem, the latter condition is equivalent to the demand that $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ , namely,

for every finite $\Gamma \cup \{ \varphi _1, \dots , \varphi _n, \psi \} \subseteq Fm(\vdash )$ . But, since the IL guarantees that the sets of the form $\{ x_1, \dots , x_n \} \, \cup \sim _n\!\!(x_1, \dots , x_n)$ are inconsistent, this amounts to the demand that $\vdash $ has the EML.

In order to derive a similar result for the bounded top width axioms, we adopt the following convention: if a family $\{ \sim _n\!\!(x_1, \dots , x_n) : n \in \mathbb {Z}^+ \}$ of sets of formulas witnesses the IL for a logic $\vdash $ , then for every finite set $\Gamma = \{ \gamma _1, \dots , \gamma _n \}$ of formulas we will write

$$\begin{align*}\sim\!\Gamma \,\,\text{ as a shorthand for }\,\, \sim_n\!\!(\gamma_1, \dots, \gamma_n). \end{align*}$$

Definition 8.5. Let $\vdash $ be a logic with the IL witnessed by a family $\{ \sim _m\!\!(x_1, \dots , x_m) : m \in \mathbb {Z}^+ \}$ and let $n \in \mathbb {Z}^+$ . The logic $\vdash $ has the bounded top width n law ( $\text {BTWL}_n$ , for short) if it validates the metarule

for every finite $\Gamma \cup \{ \gamma _1^1, \dots , \gamma _1^k, \dots , \gamma _{n+1}^1, \dots , \gamma _{n+1}^k, \psi \} \subseteq Fm(\vdash )$ .

In the presence of the IL, the semantic counterpart of the $\text {BTWL}_n$ can de described as follows:

Theorem 8.6. A protoalgebraic logic $\vdash $ with the inconsistency lemma has the bounded top width n law iff for every algebra ${\boldsymbol {A}}$ and every $F \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ , there are a positive integer $m \leqslant n$ and maximal elements $G_1, \dots , G_m$ of $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ such that every $H \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ extending F is contained in some $G_i$ .

Proof Notice that $\vdash $ has the $\text {BTWL}_n$ precisely when it validates the metarules in $\mathsf {R}_\vdash (\Phi _n)$ induced by the Sahlqvist quasiequation $\Phi _n$ corresponding to the axiom $\mathsf {btw}_n$ , defined in Example 4.5. Furthermore, $\Phi _n$ is compatible with $\vdash $ , because $\vdash $ has the IL by assumption. Therefore, we can apply the Abstract Sahlqvist Theorem, obtaining that $\vdash $ has the $\text {BTWL}_n$ iff $\mathsf {Spec}_\vdash ({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi _{n})$ , for every algebra ${\boldsymbol {A}}$ . In view of Example 4.13, the latter amounts to the demand that for every algebra ${\boldsymbol {A}}$ and every $F, H_1, \dots , H_{n+1} \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ such that F is contained in each $H_i$ , there are $G_1, \dots , G_n \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ extending F such that each $H_i$ is contained in at least one $G_j$ . Therefore, it only remains to prove that this condition is equivalent to that in the right-hand side of the statement.

The fact that the condition in the statement implies the one above is clear. To prove the converse, consider an algebra ${\boldsymbol {A}}$ satisfying the condition above. Then let M be the set of maximal proper deductive filters of $\vdash $ on ${\boldsymbol {A}}$ .

Claim 8.7. Every element of $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ is contained in some element of M.

Proof of the Claim

Suppose, with a view to contradiction, that there exists some $F \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ that cannot be extended to an element of M. Then consider the subposet of $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ with universe

Since F is meet irreducible, it is different from A and, therefore, it belongs to Y. Consequently, the poset Y is nonempty and we can apply Zorn’s Lemma to deduce that there exists a maximal chain C in Y.

We will prove that the join of C in $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ is A. Suppose, with a view to contradiction, that $\bigvee C \subsetneq A$ . Observe that the maximality of C guarantees that $F \in C$ , whence $F \subseteq \bigvee C$ . Together with the assumption that $F \notin {\downarrow }M$ , this implies that $\bigvee C \notin {\downarrow }M$ . Since by assumption $\bigvee C \ne A$ , there exists a proper $G \in \mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ such that $\bigvee C \subsetneq G$ . As a consequence $G \notin C$ , which, by the maximality of C, yields $G \notin Y$ . Since $F \subseteq \bigvee C \subseteq G$ and $F \notin {\downarrow }M$ , this means that $G = A$ , a contradiction with the assumption that G is proper. Hence, we conclude that $\bigvee C = A$ .

Now, consider one of the finite sets $\sim _n\!\!(x_1, \dots , x_n)$ witnessing the IL for $\vdash $ . Since the IL guarantees that the finite set

$$\begin{align*}\{ x_1, \dots, x_n \} \, \cup \sim_n\!\!(x_1, \dots, x_n) \end{align*}$$

is inconsistent, we obtain that

$$\begin{align*}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\{a_1, \dots, a_n\} \, \cup \sim_n\!\!(a_1, \dots, a_n)}) = A, \end{align*}$$

for every and $a_1, \dots , a_n \in A$ . Therefore, the deductive filter A is finitely generated.

By Proposition 6.4, this implies that A is a compact element of $\mathsf {Fi}_\vdash ({{\boldsymbol {A}}})$ . As a consequence, from $\bigvee C = A$ it follows that there exists a finite $C' \subseteq C$ such that $\bigvee C' = A$ . Since $F \in C$ , we may assume that $C'$ contains F and, therefore, is nonempty. As $C'$ is a finite nonempty chain, we have $\bigvee C' \in C'$ , whence $A = \bigvee C' \in C' \subseteq C \subseteq Y$ . But this contradicts the definition of Y, according to which $A \notin Y$ .

Now, consider an element $F \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ and let

Clearly, $M_F$ is a set of maximal elements of $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ . Furthermore, in view of the claim, every element of $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ extending F is contained in some element of $M_F$ . Therefore, to conclude the proof, it suffices to show that $\vert M_F \vert \leqslant n$ . Suppose, with a view to contradiction, that there are distinct $H_1, \dots , H_{n+1} \in M_F$ . As $M_F \subseteq \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ , we can apply the assumption obtaining that there are $G_1, \dots , G_n \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ such that each $H_i$ is contained into some $G_j$ . Therefore, there are $m < k \leqslant n+1$ and $j \leqslant n$ such that $H_m, H_k \subseteq G_j$ . Since $G_j$ is proper (because it belongs to $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ ), the maximality of $H_m$ and $H_k$ implies that $H_m = G = H_j$ . But this contradicts the assumption that $H_1, \dots , H_{n+1}$ are all different.

It is easy to see that a logic $\vdash $ with the IL has the $\text {BTWL}_1$ iff it has the weak excluded middle law (WEML, for short) in the sense that it validates the metarule

for every finite $\Gamma \cup \{ \varphi _1, \dots , \varphi _n, \psi \} \subseteq Fm(\vdash )$ . Bearing this in mind, from Theorem 8.6 we deduce:

Corollary 8.8 [60, Theorem 6.3].

A protoalgebraic logic $\vdash $ with the inconsistency lemma has the weak excluded middle law iff for every algebra ${\boldsymbol {A}}$ and every $F \in \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ , there exists the greatest element of $\mathsf {Spec}_\vdash ({\boldsymbol {A}})$ extending F.

9 Sahlqvist theory for fragments of $\mathsf {IPC}$ with implication

The Abstract Sahlqvist Theorem can be also employed to derive Sahlqvist theorems for concrete deductive systems. In this section, we will do this for fragments of $\mathsf {IPC}$ including the connective $\to $ . To this end, it is convenient to recall some basic concepts. Let ${\boldsymbol {A}}$ be a subreduct of a Heyting algebra in a language $\mathcal {L}_\to $ containing $\to $ . Then, the formula $x \to x$ induces a constant term function on ${\boldsymbol {A}}$ , whose constant value will be denoted by $1$ . Accordingly, a formula $\varphi $ of $\mathcal {L}_\to $ is valid in ${\boldsymbol {A}}$ , in symbols ${\boldsymbol {A}} \vDash \varphi $ , when ${\boldsymbol {A}}$ satisfies the equation $\varphi \thickapprox 1$ . Furthermore, a subset F of A is said to be an implicative filter of ${\boldsymbol {A}}$ if it contains $1$ and, for every $a, b \in A$ ,

$$\begin{align*}\text{if }\, a, a\to b \in F, \,\text{ then } \, b \in F. \end{align*}$$

When ordered under the inclusion relation, the set of implicative filters of ${\boldsymbol {A}}$ forms a lattice. We denote its subposet of meet irreducible elements by ${\boldsymbol {A}}_\ast $ .

Remark 9.1. When the language of ${\boldsymbol {A}}$ contains $\land $ , Condition (4) guarantees that the implicative and semilattice filters of ${\boldsymbol {A}}$ coincide. Therefore, there is not clash in our usage of the notation ${\boldsymbol {A}}_\ast $ both for the posets of meet irreducible semilattice and implicative filters.

The importance of implicative filters is made apparent by the following observation.

Proposition 9.2. Let $\mathsf {L}$ be a fragment of $\mathsf {IPC}$ containing $\to $ . Then, for every subreduct ${\boldsymbol {A}}$ in the language of $\mathsf {L}$ of a Heyting algebra, the deductive filters of $\mathsf {L}$ on ${\boldsymbol {A}}$ coincide with the implicative filters of ${\boldsymbol {A}}$ .

Proof Since $\mathsf {L}$ is an implicative logic in the sense of [68], the result follows from [35, Proposition 2.28].

Given a finite set $\Gamma \cup \{ \varphi \}$ of formulas of $\mathsf {IPC}$ , with $\Gamma = \{ \gamma _1, \dots , \gamma _n \}$ , we write

$$\begin{align*}\Gamma \to \varphi \, \, \text{ as a shorthand for the singleton } \, \, \{\gamma_1 \to (\gamma_2 \to (\dots (\gamma_{n} \to \varphi)\dots ))\}. \end{align*}$$

Recall from Remark 7.3 that every formula $\varphi $ of $\mathsf {IPC}$ is compatible with $\mathsf {IPC}$ . Accordingly, given $k \in \mathbb {Z}^+$ , we denote by $\boldsymbol {\varphi }^k$ the finite set of formulas of $\mathsf {IPC}$ associated with $\varphi $ . Moreover, with every Sahlqvist quasiequation

$$\begin{align*}\Phi = \varphi_1 \land y \leqslant z \, \& \dots \& \, \varphi_m \land y \leqslant z \Longrightarrow y \leqslant z, \end{align*}$$

we associate the set of formulas

where y is a variable that does not occur in $\boldsymbol {\varphi _1}^k, \dots , \boldsymbol {\varphi _m}^k$ .

Example 9.3. Consider the Sahlqvist quasiequation

$$\begin{align*}\Phi = (x_1 \to x_2) \land y \leqslant z \, \& \, (x_2 \to x_1) \land y \leqslant z \Longrightarrow y \leqslant z \end{align*}$$

corresponding to the Gödel–Dummett axiom (see Example 4.5). In view of Example 7.6, for every $k \in \mathbb {Z}^+$ , the sets $(\boldsymbol {x_1 \to x_2})^k \to y$ and $(\boldsymbol {x_2 \to x_1})^k \to y$ are the singletons containing, respectively, the formulas

and

Consequently, $\mathsf {A}(\Phi )$ is the set $\{ \psi _1^k \to (\psi _2^k \to y) : k \in \mathbb {Z}^+\}$ .

Given an algebra ${\boldsymbol {A}}$ , we denote by $\mathbb {V}({\boldsymbol {A}})$ the variety generated by ${\boldsymbol {A}}$ . We rely on the following observation.

Lemma 9.4. Let $\Phi $ be a Sahlqvist quasiequation in a sublanguage $\mathcal {L}_\to $ of $\mathcal {L}$ containing $\to $ . For every $\mathcal {L}_\to $ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra,

$$\begin{align*}{\boldsymbol{A}} \vDash \mathsf{A}(\Phi) \, \, \Longleftrightarrow \, \, {\boldsymbol{B}}_\ast \vDash \mathsf{tr}(\Phi) \text{, for every } {\boldsymbol{B}} \in \mathbb{V}({\boldsymbol{A}}). \end{align*}$$

Proof Throughout the proof we will assume that

$$\begin{align*}\Phi = \varphi_1 \land y \leqslant z \, \& \dots \& \, \varphi_m \land y \leqslant z \Longrightarrow y \leqslant z. \end{align*}$$

Furthermore, let $\mathsf {L}$ be the $\mathcal {L}_\to $ -fragment of $\mathsf {IPC}$ and let $\mathsf {L}({\boldsymbol {A}})$ be the extension of $\mathsf {L}$ axiomatized, relatively to $\mathsf {L}$ , by the formulas valid in ${\boldsymbol {A}}$ . It is well known that $\mathsf {L}({\boldsymbol {A}})$ is algebraized by $\mathbb {V}({\boldsymbol {A}})$ .

We begin by proving the following equivalences:

$$ \begin{align*} {\boldsymbol{A}} \vDash \mathsf{A}(\Phi) \, \,& \Longleftrightarrow \, \,\emptyset \vdash_{\mathsf{L}({\boldsymbol{A}})} \mathsf{A}(\Phi)\\ \, \,& \Longleftrightarrow \, \,\mathsf{L}({\boldsymbol{A}}) \text{ validates the metarules in }\mathsf{R}_{\mathsf{L}({\boldsymbol{A}})}(\Phi)\\ \, \,& \Longleftrightarrow \, \,{\boldsymbol{B}}_\ast \vDash \mathsf{tr}(\Phi) \text{, for every } {\boldsymbol{B}} \in \mathbb{V}({\boldsymbol{A}}). \end{align*} $$

The first equivalence follows from the definition of $\mathsf {L}$ . For the second, observe that, being a fragment of $\mathsf {IPC}$ with $\to $ , the logic $\mathsf {L}$ inherits the DT of $\mathsf {IPC}$ . Since the DT persists in axiomatic extensions, the DT of $\mathsf {IPC}$ holds also in $\mathsf {L}({\boldsymbol {A}})$ . Consequently, the second equivalence follows from the part of Remark 7.12 devoted to the DT. To prove the third one, we begin by showing that $\Phi $ is compatible with $\mathsf {L}({\boldsymbol {A}})$ . Suppose, for instance, that the connective $\lor $ occurs in some $\varphi _i$ . Then $\mathcal {L}_\to $ contains $\lor $ . Since the PC persists in axiomatic extensions of fragments of $\mathsf {IPC}$ with $\lor $ , we conclude that $\mathsf {L}({\boldsymbol {A}})$ has the PC as desired. A similar argument applies to the cases where $0, \lnot $ , or $\to $ occur in some $\varphi _i$ , thereby yielding that $\Phi $ is compatible with $\mathsf {L}({\boldsymbol {A}})$ . Furthermore, recall that $\mathbb {V}({\boldsymbol {A}})$ algebraizes $\mathsf {L}({\boldsymbol {A}})$ . Lastly, Proposition 9.2 guarantees that $\mathsf {Spec}_{\mathsf {L}({\boldsymbol {A}})}({\boldsymbol {B}}) = {\boldsymbol {B}}_\ast $ , for every ${\boldsymbol {B}} \in \mathbb {V}({\boldsymbol {A}})$ . Therefore, we can apply Corollary 7.17, thus establishing the third equivalence.

Notably, one can view $\mathsf {A}(\Phi )$ as the equational version of the quasiequation $\Phi $ , as made precise by the next observation.

Proposition 9.5. A Heyting algebra ${\boldsymbol {A}}$ validates a Sahlqvist quasiequation $\Phi $ iff it validates the formulas in $\mathsf {A}(\Phi )$ .

Proof In view of Lemma 9.4, it suffices to establish the following equivalences:

$$ \begin{align*} {\boldsymbol{B}}_\ast \vDash \mathsf{tr}(\Phi) \text{, for every } {\boldsymbol{B}} \in \mathbb{V}({\boldsymbol{A}})\, \,& \Longleftrightarrow \, \,{\boldsymbol{B}} \vDash \Phi \text{, for every } {\boldsymbol{B}} \in \mathbb{V}({\boldsymbol{A}})\\ \, \,& \Longleftrightarrow \, \, {\boldsymbol{A}} \vDash \Phi. \end{align*} $$

To this end, we will assume that

$$\begin{align*}\Phi = \varphi_1 \land y \leqslant z \, \& \dots \& \, \varphi_m \land y \leqslant z \Longrightarrow y \leqslant z. \end{align*}$$

The first equivalence holds by Corollary 5.13. To prove the nontrivial part of the second, suppose that ${\boldsymbol {A}} \vDash \Phi $ . In view of Corollary 4.7, the equation $\varphi _1 \lor \dots \lor \varphi _n \thickapprox 1$ is valid in ${\boldsymbol {A}}$ . Therefore, it is also valid $\mathbb {V}({\boldsymbol {A}})$ . With another application of Corollary 4.7, we conclude that $\Phi $ is valid in all the members of $\mathbb {V}({\boldsymbol {A}})$ as desired.

As in the case of Theorem 5.1, Sahlqvist Theorem from fragments of $\mathsf {IPC}$ with $\to $ takes the form of a canonicity result.

Theorem 9.6. Let $\Phi $ be a Sahlqvist quasiequation in a sublanguage $\mathcal {L}_\to $ of $\mathcal {L}$ containing $\to $ . If an $\mathcal {L}_\to $ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra validates $\mathsf {A}(\Phi )$ , then also $\mathsf {Up}({\boldsymbol {A}}_\ast )$ validates $\mathsf {A}(\Phi )$ .

Proof Suppose that ${\boldsymbol {A}} \vDash \mathsf {A}(\Phi )$ . In view of Lemma 9.4, this yields ${\boldsymbol {A}}_\ast \vDash \mathsf {tr}(\Phi )$ . Therefore, we can apply the correspondence part of the Intuitionistic Sahlqvist Theorem, obtaining $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \Phi $ . Lastly, by Proposition 9.5, this amounts to $\mathsf {Up}({\boldsymbol {A}}_\ast ) \vDash \mathsf {A}(\Phi )$ .

Bearing in mind that $\Phi $ and $\mathsf {A}(\Phi )$ axiomatize the same class of Heyting algebras (Proposition 9.5), a straightforward adaptation of the proof of Corollary 5.13 yields the following:

Corollary 9.7. Let $\Phi $ be a Sahlqvist quasiequation in a sublanguage $\mathcal {L}_\to $ of $\mathcal {L}$ containing $\to $ . For every $\mathcal {L}_\to $ -subreduct ${\boldsymbol {A}}$ of a Heyting algebra, it holds that ${\boldsymbol {A}} \vDash \mathsf {A}(\Phi ) \text { iff } {\boldsymbol {A}}_\ast \vDash \mathsf {tr}(\Phi )$ .

Example 9.8. The $\langle \to \rangle $ -subreduct of Heyting algebras are called Hilbert algebras [29, 30]. Let $\Phi $ be the Sahlqvist quasiequation corresponding to the Gödel–Dummett axiom. Since a Hilbert algebra validates $\mathsf {A}(\Phi )$ iff it validates the single formula $\varphi = ((x \to y) \to z) \to ( ((y \to z) \to z) \to z$ , in view of Corollary 9.7 and Example 4.13, we obtain that

$$\begin{align*}{\boldsymbol{A}} \vDash \varphi \, \, \Longleftrightarrow \, \, {\boldsymbol{A}}_\ast \text{ is a root system}, \end{align*}$$

for every Hilbert algebra [64, Theorem 4.5].

10 A correspondence theorem for intuitionistic linear logic

We close this paper by deriving a correspondence theorem for intuitionistic linear logic [48] from the Abstract Sahlqvist Theorem (cf. [75, 76]). To this end, recall that a commutative FL-algebra is a structure ${\boldsymbol {A}} = \langle A; \land , \lor , \cdot , \to , 0, 1 \rangle $ comprising a commutative monoid $\langle A; \cdot , 1 \rangle $ and a lattice $\langle A; \land , \lor \rangle $ such that for every $a, b, c \in A$ ,

(29) $$ \begin{align} a \cdot b \leqslant c \, \,\Longleftrightarrow\, \, a \leqslant b \to c. \end{align} $$

The class of commutative FL-algebras forms a variety which we denote by $\mathsf {FL}_{\mathsf e}$ [41]. Intuitionistic linear logic ( $\mathsf {ILL}$ ) is the logic formulated in the language of commutative FL-algebras defined, for every set $\Gamma \cup \{ \varphi \}$ of formulas, as follows:

It is well known that every axiomatic extension $\vdash $ of $\mathsf {ILL}$ is algebraized by the variety $\mathsf {K}_\vdash $ of commutative FL-algebras axiomatized by the set of equations $\{ \varphi \geqslant 1 : \emptyset \vdash \varphi \}$ , as witnessed by the sets

and

[40, Theorem 3.3]. In particular, $\mathsf {ILL}$ is algebraized by $\mathsf {FL}_{\mathsf {e}}$ .

Given an algebra ${\boldsymbol {A}}$ in the language of $\mathsf {ILL}$ , an element $a \in A$ , and $n \in \mathbb {Z}^+$ , we define an element $a^n$ of A by setting

We will rely on the following property of $\mathsf {ILL}$ :

Proposition 10.1 [40, Theorem 4.9].

For every algebra ${\boldsymbol {A}}$ and $X \cup \{ a, b \} \subseteq A$ ,

$$\begin{align*}a \in \mathsf{Fg}^{{\boldsymbol{A}}}_{\mathsf{ILL}}({X \cup \{ b \}}) \, \, \text{ iff } \, \, (1 \land b)^n \to a \in \mathsf{Fg}^{{\boldsymbol{A}}}_{\mathsf{ILL}}({X})\text{, for some }n \in \mathbb{Z}^+. \end{align*}$$

When ${\boldsymbol {A}}$ is the algebra of formulas $\boldsymbol {Fm}(\mathsf {ILL})$ , this specializes to the following:

Corollary 10.2. For every set $\Gamma \cup \{ \psi , \varphi \}$ of formulas of $\mathsf {ILL}$ , we have

$$\begin{align*}\Gamma, \psi \vdash_{\mathsf{ILL}} \varphi \, \, \text{ iff } \, \, \Gamma \vdash_{\mathsf{ILL}} (1 \land \psi)^n \to \varphi\text{, for some }n \in \mathbb{Z}^+. \end{align*}$$

In order to obtain a correspondence theorem for $\mathsf {ILL}$ , it is convenient to identify the axiomatic extensions of $\mathsf {ILL}$ with the IL, the DT, and the PC. For the DT and the PC we have the following:

Proposition 10.3 [39, Proposition 3.15].

An axiomatic extension of $\mathsf {ILL}$ has the deduction theorem iff there exists some $k \in \mathbb {Z}^+$ such that the theorems of $\vdash $ include the formula $(1 \land x)^k \to (1 \land x)^{k+1}$ . In this case, the DT is witnessed by the sets of the form

$$\begin{align*}(x_1, \dots, x_n)\!\Rightarrow_{nm} \!\!(y_1, \dots, y_m)= \{ (1 \land x_1 \land \dots \land x_n)^k \to (y_1 \land \dots \land y_m) \}. \end{align*}$$

Proposition 10.4. Every axiomatic extension $\vdash $ of $\mathsf {ILL}$ has the proof by cases, as witnessed by the sets of the form

Proof This is essentially [19, Example 4.10.4], where the result is stated for the natural expansion $\mathsf {SL}_{\mathsf {aE}}$ of $\mathsf {ILL}$ with bounds.

In order to address the case of the IL, it is convenient to introduce the following shorthand for every formula $\varphi $ of $\mathsf {ILL}$ :

Proposition 10.5. An axiomatic extension $\vdash $ of $\mathsf {ILL}$ has the inconsistency lemma iff there exist some $k \in \mathbb {Z}^+$ and a function $f \colon \mathbb {Z}^+ \to \mathbb {Z}^+$ such that the theorems of $\vdash $ include the formulas

$$\begin{align*}\bot^k \to x \, \, \text{ and } \, \, (1 \land \lnot (x \land 1)^m )^{f(m)} \to \lnot (1 \land x)^k, \end{align*}$$

for every $m \in \mathbb {Z}^+$ . In this case, the IL is witnessed by the sets of the form

Proof We will often use the fact that $\vdash $ is algebraized by $\mathsf {K}_\vdash $ , as witnessed by the sets and . Similarly, we will repeatedly appeal to the fact that for every ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ and $a, b \in A$ ,

$$\begin{align*}a \leqslant b \, \, \Longleftrightarrow \, \, 1 \leqslant a \to b \end{align*}$$

and

$$\begin{align*}\text{if } a \leqslant 1 \text{, then } a^{n+1} \leqslant a^n\text{, for every }n \in \mathbb{Z}^+. \end{align*}$$

The first property follows from Condition (29) and the assumption that $\langle A; \cdot , 1 \rangle $ is a monoid. The second holds because the operation $\cdot $ is order preserving in both coordinates and, therefore, the assumption that $a \leqslant 1$ guarantees that $a^{n+1} = a^n \cdot a \leqslant a^n \cdot 1 = a^n$ . These facts will be used in the proof without further notice.

We begin by proving the implication from left to right in the statement. Accordingly, suppose that $\vdash $ has the IL. We rely on the next observations:

Claim 10.6. The formula $\bot $ is inconsistent in $\vdash $ .

Proof of the Claim

First, we will prove that

(30) $$ \begin{align} \bot \vdash \varphi \to \psi\text{, for every pair }\varphi\text{ and }\psi\text{ of formulas in which no variable occurs.} \end{align} $$

Accordingly, consider two such formulas $\varphi $ and $\psi $ . It suffices to show that

$$\begin{align*}\mathsf{K}_\vdash \vDash \bot \geqslant 1 \Longrightarrow \varphi \to \psi \geqslant 1. \end{align*}$$

To this end, consider an algebra ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ such that $1^{\boldsymbol {A}} \leqslant \bot ^{\boldsymbol {A}}$ . By the definition of $\bot $ , this yields $0^{\boldsymbol {A}} = 1^{\boldsymbol {A}} = 1^{\boldsymbol {A}} \to 1^{\boldsymbol {A}}$ . As

$$\begin{align*}\mathsf{FL}_{\mathsf{e}}\vDash 1 \thickapprox1 \land 1 \thickapprox 1 \lor 1 \thickapprox 1 \cdot 1, \end{align*}$$

this implies that $\{ 1^{\boldsymbol {A}} \}$ is the universe of a subalgebra of ${\boldsymbol {A}}$ . Consequently, $\varphi ^{\boldsymbol {A}}, \psi ^{\boldsymbol {A}} \in \{ 1^{\boldsymbol {A}} \}$ , because $\varphi $ and $\psi $ have no variables. Therefore, $\varphi ^{\boldsymbol {A}} = \psi ^{\boldsymbol {A}}$ . In particular, $\varphi ^{\boldsymbol {A}} \leqslant \psi ^{\boldsymbol {A}}$ , which amounts to $1^{\boldsymbol {A}} \leqslant \varphi ^{\boldsymbol {A}} \to \psi ^{\boldsymbol {A}}$ , as desired. This establishes Condition (30).

Now, recall that the IL guarantees that the set is inconsistent. In particular, $1 \land \bigwedge \! \sim _1\!\!(1) \vdash y$ . Furthermore, from Condition (30) it follows that $\bot \vdash 1 \to (1 \land \bigwedge \!\sim _1\!\!(1))$ . Since $1$ is a theorem of $\vdash $ and $x, x\to y \vdash y$ , this yields that $\bot \vdash 1 \land \bigwedge \!\sim _1\!\!(1)$ . Together with $1 \land \bigwedge \! \sim _1\!\!(1) \vdash y$ , this implies that $\bot \vdash y$ . By substitution invariance, we conclude that $\bot $ is inconsistent.

Claim 10.7. For every ${\boldsymbol {A}} \in \mathsf {K_\vdash }$ and $a \in A$ , we have that $ 1 \leqslant \bigwedge \!\thicksim _1\!\!(a) $ iff there exists some $n \in \mathbb {Z}^+$ such that $(1 \land a)^n \leqslant \bot $ .

Proof of the Claim

Recall from Theorem 6.9 that the semilattice $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is pseudocomplemented. Therefore, $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({a}) = A$ iff the pseudocomplement $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\thicksim _1\!\!(a)})$ of $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({a})$ in $\mathsf {Fi}_\vdash ^\omega ({{\boldsymbol {A}}})$ is included in $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\emptyset })$ , in symbols,

$$\begin{align*}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a}) = A \, \, \Longleftrightarrow \, \, \thicksim_1\!\!(a) \subseteq \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\emptyset}). \end{align*}$$

On the other hand, by applying in succession Claim 10.6 and Proposition 10.1, we obtain

$$\begin{align*}\mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a}) = A \, \, \Longleftrightarrow \, \, \bot \in \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({a}) \, \, \Longleftrightarrow \, \, \lnot (1 \land a)^n \in \mathsf{Fg}^{{\boldsymbol{A}}}_\vdash({\emptyset})\text{, for some }n \in \mathbb{Z}^+. \end{align*}$$

From the two displays above and the fact that $\mathsf {Fg}^{{\boldsymbol {A}}}_\vdash ({\emptyset }) = \{ c \in A : c \geqslant 1 \}$ it follows that

$$\begin{align*}1 \leqslant \bigwedge \!\sim_1 \!\! (a) \, \, \Longleftrightarrow \, \, 1 \leqslant \lnot (1 \land a)^n \text{, for some }n \in \mathbb{Z}^+, \end{align*}$$

where the condition on the right-hand side is equivalent to the demand that there exists some $n \in \mathbb {Z}^n$ such that $(1 \land a)^n \leqslant \bot $ .

In virtue of Claim 10.6 and Corollary 10.2, there exists some $t \in \mathbb {Z}^+$ such that $\emptyset \vdash (1 \land \bot )^{t} \to x$ . Therefore, $\mathsf {K}_\vdash \vDash (1 \land \bot )^t \to x \geqslant 1$ , which amounts to $\mathsf {K}_\vdash \vDash (1 \land \bot )^t \leqslant x$ . By the definition of $\bot $ , we have $\mathsf {K}_\vdash \vDash \bot \leqslant 1$ . As a consequence, $\mathsf {K}_\vdash \vDash \bot ^s \leqslant x$ , for every positive integer $s \geqslant t$ . This, in turn, yields that

(31) $$ \begin{align} \emptyset \vdash \bot^{s} \to x \text{, for every positive integer }s \geqslant t. \end{align} $$

On the other hand, in view of Claim 10.7, we have that

$$\begin{align*}\mathsf{Th}(\mathsf{K_\vdash}) \cup \{(1 \land x)^n \nleqslant \bot \colon n \in \mathbb{Z}^+\} \Vdash_{\mathsf{FOL}} 1 \nleqslant \bigwedge \! \thicksim_1\!\!(x), \end{align*}$$

where $\mathsf {Th}(\mathsf {K_\vdash })$ is the elementary theory of $\mathsf {K}_\vdash $ and $\Vdash _{\mathsf {FOL}}$ is the deducibility relation of first-order logic. By the Compactness Theorem of first-order logic, the previous display implies that there are some positive integers $n_1,\dots ,n_m \in \mathbb {Z}^+$ such that

$$\begin{align*}\mathsf{Th}(\mathsf{K_\vdash}) \cup \{ (1 \land x)^{n_1} \nleqslant \bot, \dots, (1 \land x)^{n_m} \nleqslant \bot \} \Vdash_{\mathsf{FOL}} 1 \nleqslant \bigwedge \! \thicksim_1\!\!(x). \end{align*}$$

Letting , the above display implies

$$\begin{align*}\mathsf{Th}(\mathsf{K_\vdash}) \cup \{ (1 \land x)^{k} \nleqslant \bot \} \Vdash_{\mathsf{FOL}} 1 \nleqslant \bigwedge \! \thicksim_1\!\!(x). \end{align*}$$

This, in turn, amounts to the following:

$$\begin{align*}\mathsf{K}_\vdash \vDash \bigwedge \! \thicksim_1\!\!(x) \geqslant 1 \Longrightarrow (1 \land x)^{k} \leqslant \bot. \end{align*}$$

In view of Claim 10.7, this yields that for every $m \in \mathbb {Z}^+$ ,

$$\begin{align*}\mathsf{K}_\vdash \vDash (1 \land x )^m \leqslant \bot \Longrightarrow (1 \land x)^{k} \leqslant \bot, \end{align*}$$

where the condition above can be equivalently phrased as

$$\begin{align*}\mathsf{K}_\vdash \vDash \lnot (1 \land x )^m \geqslant 1 \Longrightarrow \lnot (1 \land x)^{k} \geqslant 1. \end{align*}$$

Consequently, $\lnot (1 \land x )^m \vdash \lnot (1 \land x)^{k}$ , for every $m \in \mathbb {Z}^+$ . In view of Proposition 10.1, for every $m \in \mathbb {Z}$ there exists some $f(m) \in \mathbb {Z}^+$ such that

$$\begin{align*}\emptyset \vdash (1 \land \lnot (1 \land x )^m)^{f(m)} \to \lnot (1 \land x)^{k}. \end{align*}$$

Lastly, since the definition of k guarantees that $k \geqslant t$ , from Condition (31) it follows that $\emptyset \vdash \bot ^k \to x$ .

Then we turn to prove the implication from right to left in the statement. We will show that the sets of the form

witness the IL for $\vdash $ , i.e., that for every finite $\Gamma \cup \{\varphi _1,\dots ,\varphi _n\} \subseteq Fm(\vdash )$ ,

$$\begin{align*}\Gamma \cup \{\varphi_1,\dots,\varphi_n\} \text{ is inconsistent } \, \, \text{ iff } \, \, \Gamma \vdash \lnot(1 \land \varphi_1 \land \dots \land \varphi_n)^k. \end{align*}$$

Suppose first that $\Gamma \cup \{\varphi _1,\dots ,\varphi _n\}$ is inconsistent. Then $\Gamma , \varphi _1 \land \dots \land \varphi _n \vdash \bot $ . In view of Corollary 10.2, there exists some $m \in \mathbb {Z}^+$ such that $\Gamma \vdash \lnot (1 \land \varphi _1 \land \dots \land \varphi _n)^m$ . As $x \vdash (1 \land x)^{f(m)}$ , this yields $\Gamma \vdash (1 \land \lnot (1 \land \varphi _1 \land \dots \land \varphi _n)^m)^{f(m)}$ . Since by assumption $\emptyset \vdash (1 \land \lnot (1 \land x )^m)^{f(m)} \to \lnot (1 \land x)^{k} $ , with an application of modus ponens, we obtain that $\Gamma \vdash \lnot (1 \land \varphi _1 \land \dots \land \varphi _n)^k$ , as desired.

To prove the converse, suppose that $\Gamma \vdash \lnot (1 \land \varphi _1 \land \dots \land \varphi _n)^k$ . By Corollary 10.2, this implies that $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \} \vdash \bot $ . Furthermore, as $x \vdash x^k$ , we get $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \} \vdash \bot ^k$ . Since the set $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \}$ is finite, there exists a variable x that does not occur in any of its members. As by assumption $\emptyset \vdash \bot ^k \to x$ , by modus ponens we obtain $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \} \vdash x$ . Since, x does not occur in the formulas of $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \}$ , by substitution invariance, we obtain that $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \} \vdash \psi $ for every formula $\psi $ . Hence, we conclude that $\Gamma \cup \{ \varphi _1, \dots , \varphi _n \}$ is inconsistent.

Let $\vdash $ be an axiomatic extension of $\mathsf {ILL}$ . Notice that, if $\varphi $ is a formula of $\mathsf {IPC}$ compatible with $\vdash $ , then the finite set of formulas $\boldsymbol {\varphi }^k$ is interderivable in $\vdash $ with the conjunction $\bigwedge \boldsymbol {\varphi }^k$ , for every $k \in \mathbb {Z}^+$ . Accordingly, from now on we will assume that the expressions of the form $\boldsymbol {\varphi }^k$ stand for formulas $\bigwedge \boldsymbol {\varphi }^k$ of $\vdash $ , as opposed to a sets of formulas of $\vdash $ .

Furthermore, recall that $\mathsf {K}_\vdash $ is a variety, whence it is closed under $\mathbb {H}$ . Consequently, $\mathsf {Spec}_{\mathsf {K}_\vdash }({\boldsymbol {A}})$ coincides with the poset of meet irreducible congruences of ${\boldsymbol {A}}$ , for every ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ . Because of this, when ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ , we will write $\mathsf {Spec}({\boldsymbol {A}})$ as a shorthand for $\mathsf {Spec}_{\mathsf {K}_\vdash }({\boldsymbol {A}})$ . Bearing this in mind, we obtain the desired correspondence theorem:

Theorem 10.8. Let $\Phi = \varphi _1 \land y \leqslant z \, \& \dots \& \, \varphi _m \land y \leqslant z \Longrightarrow y \leqslant z$ be a Sahlqvist quasiequation compatible with an axiomatic extension $\vdash $ of $\mathsf {ILL}$ . Then the theorems of $\vdash $ include the formula $(1 \land \boldsymbol {\varphi _1}^1) \lor \dots \lor (1 \land \boldsymbol {\varphi _m}^1)$ iff $\mathsf {Spec}({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi )$ , for every algebra ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ .

Proof Observe that $\land $ is a conjunction for $\vdash $ and that $\vdash $ has the PC, as witnessed by sets in Proposition 10.4. Therefore, from Remark 7.12 it follows that the theorems of $\vdash $ include the formula $(1 \land \boldsymbol {\varphi _1}^1) \lor \dots \lor (1 \land \boldsymbol {\varphi _m}^1)$ iff the logic $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi )$ . But, since $\vdash $ is algebraized by $\mathsf {K}_\vdash $ , we can apply Corollary 7.17 obtaining that the latter condition is equivalent to the demand that $\mathsf {Spec}({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi )$ , for every ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ .

Example 10.9. Let $\vdash $ be an axiomatic extension of $\mathsf {ILL}$ with the IL. Then there are some $k\in \mathbb {Z}^+$ and a function $f \colon \mathbb {Z}^+ \to \mathbb {Z}^+$ witnessing the property in the statement of Proposition 10.5. We will prove that the following conditions are equivalent for every $n \in \mathbb {Z}^+$ :

1. (i) The logic $\vdash $ has the $\text {BTWL}_n$ .

2. (ii) The theorems of $\vdash $ include the formula

   $$\begin{align*}\bigvee_{1 \leqslant i \leqslant n+1}\bigg( 1 \land \lnot \bigg( 1 \land \bigwedge_{1 \leqslant j < i} x_j \land \lnot(1 \land x_i)^k\bigg)^k \bigg). \end{align*}$$

3. (iii) For every ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ and $\theta \in \mathsf {Spec}({\boldsymbol {A}})$ , there are a positive integer $m \leqslant n$ and maximal elements $\phi _1, \dots , \phi _m$ of $\mathsf {Spec}({\boldsymbol {A}})$ such that every $\eta \in \mathsf {Spec}({\boldsymbol {A}})$ extending $\theta $ is contained in some $\phi _i$ .

First, recall from Example 4.5 that the Sahlqvist quasiequation

$$\begin{align*}\Phi_n = \varphi_1 \land y \leqslant z \, \& \dots \& \, \varphi_{n+1} \land y \leqslant z \Longrightarrow y \leqslant z, \end{align*}$$

corresponding to the $\mathsf {btw}_n$ axiom is defined setting, for every $i \leqslant n+1$ ,

To prove the equivalence between Conditions (i) and (ii), recall that the logic $\vdash $ has the $\text {BTWL}_n$ precisely when it validates the metarules in $\mathsf {R}_\vdash (\Phi _n)$ . As observed in the proof of Theorem 10.8, this happens iff the theorems of $\vdash $ include the formula $(1 \land \boldsymbol {\varphi _1}^1) \lor \dots \lor (1 \land \boldsymbol {\varphi _{n+1}}^1)$ . But the latter coincides with the formula in Condition (ii), because the IL for $\vdash $ is witnessed by the sets of formulas in Proposition 10.5.

Lastly, recall that $\mathsf {Spec}({\boldsymbol {A}}) \cong \mathsf {Spec}_\vdash ({\boldsymbol {A}})$ for every ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ , because $\vdash $ is algebraized by $\mathsf {K}_\vdash $ . Therefore, the implication (i) $\Rightarrow $ (iii) follows from Theorem 8.6. To prove the converse, suppose that Condition (iii) holds. Then it is easy to check that $\mathsf {Spec}({\boldsymbol {A}}) \vDash \mathsf {tr}(\Phi _n)$ for every ${\boldsymbol {A}} \in \mathsf {K}_\vdash $ , where $\mathsf {tr}(\Phi _n)$ is the first-order sentence mentioned in Example 4.13. Consequently, we can apply Corollary 7.17, obtaining that $\vdash $ validates the metarules in $\mathsf {R}_\vdash (\Phi _n)$ , which means that $\vdash $ has the $\text {BTWL}_n$ .

Example 10.10. The following conditions are equivalent for an axiomatic extension $\vdash $ of $\mathsf {ILL}$ : ¹⁸

1. (i) The logic $\vdash $ has the EML.

2. (ii) There exist some $k \in \mathbb {Z}^+$ and a function $f \colon \mathbb {Z}^+ \to \mathbb {Z}^+$ such that the theorems of $\vdash $ include the formulas

   $$\begin{align*}\bot^k \to x, \, \text{ } (1 \land \lnot (x \land 1)^m )^{f(m)} \to \lnot (1 \land x)^k, \, \text{ and } \, (1 \land x) \lor ( 1 \land \lnot (x \land 1)^k), \end{align*}$$

   for every $m \in \mathbb {Z}^+$ .

3. (iii) The logic $\vdash $ is semisimple and has the IL.

In view of Remark 8.2, the logic $\vdash $ has the EML iff it has the IL and validates the metarules in $\mathsf {R}_\vdash (\Phi )$ , where

$$\begin{align*}\Phi = x \land y \leqslant z \, \& \, \lnot x \land y \leqslant z \Longrightarrow y \leqslant z. \end{align*}$$

As observed in the proof of Theorem 10.8, the logic $\vdash $ validates the rules in $\mathsf {R}_\vdash (\Phi )$ precisely when its theorems contain $(1 \land \boldsymbol {x}^1) \lor (1 \land (\boldsymbol {\lnot x})^1)$ . Consequently, Condition (i) can be rephrased as the demand that $\vdash $ has the IL and its theorems include the formula $(1 \land \boldsymbol {x}^1) \lor (1 \land (\boldsymbol {\lnot x})^1)$ .

On the other hand, in view of Proposition 10.5, the demand that the theorems of $\vdash $ contain the first two formulas in Condition (ii) amounts to the assumption that $\vdash $ has the IL. The third formula in Condition (ii) is precisely $(1 \land \boldsymbol {x}^1)\lor (1 \land (\boldsymbol {\lnot x})^1)$ , whence this condition can be equivalently phrased as the requirement that $\vdash $ has the IL and that $\emptyset \vdash (1 \land \boldsymbol {x}^1) \lor (1 \land (\boldsymbol {\lnot x})^1)$ . It follows that Conditions (i) and (ii) are equivalent.

Lastly, the equivalence between Conditions (i) and (iii) follows from Theorem 8.4.