1 Introduction

The recent series of papers Rivieccio and Spinks (2019); Liang and Nascimento (2019); Rivieccio and Spinks (2020); Rivieccio and Jansana (2021) introduced and developed the basic theory of a non-involutive generalization of Nelson constructive logic with strong negation (Nelson 1949). The new logic was dubbed quasi-Nelson logic (Liang and Nascimento 2019), and the corresponding algebraic models quasi-Nelson algebras. The cited papers show how a number of features and results characteristic of Nelson logic and of its algebraic counterpart (the class of Nelson algebras, alias Nelson residuated lattices) smoothly extend to the non-involutive setting. In particular, it is shown in Rivieccio and Spinks (2020) that quasi-Nelson algebras can be characterized as the class of (0, 1)-congruence orderable residuated lattices, mirroring the characterization of Nelson algebras as the (0, 1)-congruence orderable involutive residuated lattices obtained in Spinks et al. (2019). The papers Rivieccio and Spinks (2019, 2020); Rivieccio and Jansana (2021) further develop a twist-structure representation for quasi-Nelson algebras that is a straightforward generalization of the well-known representation for Nelson algebras due to Vakarelov, Fidel and Sendlewski.

An alternative and older generalization of Nelson algebras is the class of N4-lattices which was introduced as the algebraic counterpart of the paraconsistent version of Nelson logic (Almukdad and Nelson 1984; Odintsov 2003, 2004, 2008). In logical terms, paraconsistent Nelson logic is a weakening of Nelson constructive logic that results from rejecting the explosion axiom \( p \rightarrow (\mathop {\sim }p \rightarrow q ) \), whereas quasi-Nelson logic rejects the double negation law \(\mathop {\sim }\mathop {\sim }p \rightarrow p \). In consequence, the algebraic models of quasi-Nelson logic are residuated lattices that are both integral and boundedFootnote 1 but not necessarily involutive, whereas N4-lattices are residuated structures that possess an involutive negation (satisfying \(\mathop {\sim }\mathop {\sim }x \approx x\)) but are in general neither bounded nor integral. As in the case of quasi-Nelson algebras, a number of key results on Nelson algebras have also been extended to their paraconsistent counterpart. In particular, Odintsov (2003, 2004, 2008) obtained a twist-structure representation for N4-lattices, and Spinks and Veroff (2018) showed how paraconsistent Nelson logic can be viewed as a contraction-free relevance logic.

While it is easily shown that Nelson logic is the least logic that includesFootnote 2 both quasi-Nelson and paraconsistent Nelson logic, the above considerations suggest that the latter are mutually incomparable weakenings of the logic originally introduced by Nelson (1949). The question thus arises of whether one could find a common framework encompassing all three logics and, more interestingly, whether in such a setting one might be able to reproduce the characteristic results on quasi-Nelson and paraconsistent Nelson logic mentioned above. The present paper is a first attempt at tackling this question.

Taking an algebraic approach, we shall introduce the class of quasi-N4-lattices (QN4-lattices) as a common generalization of quasi-Nelson algebras and N4-lattices. The definition we propose is such that N4-lattices turn out to be precisely the QN4-lattices satisfying the double negation law, and quasi-Nelson algebras are precisely the QN4-lattices satisfying the explosive law (Proposition 3.8). We will show that QN4-lattices admit a twist-structure representation entirely analogous to the known ones (Theorem 3.3), and using this representation we will obtain a number of results that mirror the ones already established for quasi-Nelson algebras and N4-lattices. In particular, we characterize the congruences and the (logical) filters on QN4-lattices, and we show that this class (forms a variety which) has equationally definable principal congruences, enjoys the strong congruence extension property and is arithmetical (i.e., both congruence-distributive and congruence-permutable). This last result provides a new proof of congruence-permutability that specializes to both N4-lattices (Spinks and Veroff 2018, Thm. 4.24) and quasi-Nelson algebras.

2 QN4-lattices as twist-structures

In this section we see that twist-structures provide a most straightforward means to devise a common generalization of N4-lattices and quasi-Nelson algebras. The construction we are going to introduce (Definition 2.2) is an obvious extension of the twist-structures used in Rivieccio and Spinks (2019, 2020); Rivieccio and Jansana (2021) to represent quasi-Nelson algebras, as well as of Odintsov’s representation of N4-lattices (Odintsov 2004).

Recall that a Brouwerian algebraFootnote 3 is an algebra \( \langle B ; \wedge , \vee , \rightarrow \rangle \) such that \( \langle B ; \wedge ,\vee \rangle \) is a lattice with order \(\le \) and \(\rightarrow \) is the residuum of \(\wedge \), that is, \(a \wedge b \le c \) iff \(a \le b \rightarrow c\), for all \(a,b, c \in B\). The latter property entails that the lattice \( \langle B ; \wedge ,\vee \rangle \) is distributive and has a top element 1 (while the bottom element may not exist), so 1 can be safely added to the algebraic language as a primitive nullary operation.

Definition 2.1

Given a Brouwerian algebra \( \langle B ; \wedge ,\vee , \rightarrow \rangle \), we say that a unary operator \(\Box :B \rightarrow B \) is a nucleus if, for all \(a,b \in B\),

  1. (i)

    \(\Box (a \wedge b) = \Box a \wedge \Box b \).

  2. (ii)

    \(a \le \Box a = \Box \Box a \).

Nuclei defined on (bounded) Brouwerian algebras are considered, for instance, in Macnab (1981). The above properties entail that \(\Box 1 = 1\) and \(\Box (a \rightarrow b) \le \Box a \rightarrow \Box b\) for all \(a,b \in B\) (cf. the proof of item (xiv) of Proposition 2.4 below), suggesting that \(\Box \) may be viewed as a modal operator. We shall refer to an algebra \( \mathbf {B} = \langle B ; \wedge ,\vee , \rightarrow , \Box \rangle \) as to a nuclear Brouwerian algebra.

Definition 2.2

Let \( \mathbf {B} = \langle B ; \wedge _{\mathbf {B} } ,\vee _{\mathbf {B} } , \rightarrow _{\mathbf {B} } , \Box _{\mathbf {B} } \rangle \) be a nuclear Brouwerian algebra. The algebra \( \mathbf {B}^{\bowtie }\! =\! \langle B \times B ; \wedge , \vee , \rightarrow , \mathop {\sim }\rangle \) is defined as follows. For all \(\langle a_1 ,a_2 \rangle , \langle b_1, b_2 \rangle \in B \times B\),

$$\begin{aligned}&\mathop {\sim }\langle a_1 , a_2 \rangle = \langle a_2, \Box _{\mathbf {B} } \, a_1 \rangle \\&\langle a_1 , a_2 \rangle \wedge \langle b_1 , b_2 \rangle = \langle a_1 \wedge _{\mathbf {B} } b_1 , \Box _{\mathbf {B} } (a_2 \vee b_2 )\rangle \\&\langle a_1 , a_2 \rangle \vee \langle b_1 , b_2 \rangle = \langle a_1 \vee _{\mathbf {B} } b_1 , a_2 \wedge _{\mathbf {B} } b_2\rangle \\&\langle a_1 , a_2 \rangle \rightarrow \langle b_1 , b_2 \rangle = \langle a_1 \rightarrow _{\mathbf {B} } b_1 , \Box _{\mathbf {B} } \, a_1 \wedge _{\mathbf {B} } b_2 \rangle . \end{aligned}$$

A quasi-N4 twist-structure \(\mathbf {A} \) over \(\mathbf {B}\) is a subalgebra of \(\mathbf {B}^{\bowtie } \) satisfying the following properties: \(\pi _1[A] = B\) and \(\Box _{\mathbf {B} } \, a_2 = a_2\) for all \(\langle a_1, a_2 \rangle \in A\).

As mentioned earlier, the preceding construction is a straightforward generalization of those employed in Odintsov (2004, 2008); Rivieccio and Spinks (2019, 2020); Rivieccio and Jansana (2021). Indeed, one can readily verify that any N4-lattice or quasi-Nelson algebra can be constructed by suitably restricting the requirements of Definition 2.2 (more on this below). We shall henceforth write \(\mathbf {A} \le \mathbf {B}^{\bowtie } \) to mean that \(\mathbf {A} \) is a quasi-N4 twist-structure over a nuclear Brouwerian algebra \(\mathbf {B}\). In order to simplify the notation, from now on we shall also overload the symbols \(\wedge , \vee , \rightarrow \) to denote operations on \(\mathbf {B} \) as well as on \(\mathbf {B}^{\bowtie } \) (the context will clarify whether these apply to elements of B or to ordered pairs in \(B \times B\)).

Notice that the set \(S : = \{ \langle a_1, a_2 \rangle \in B \times B : \Box a_2 = a_2 \}\) is closed under all the operations of \(\mathbf {B}^{\bowtie } \), and is therefore the universe of (the largest) twist-structure over \(\mathbf {B} \). Indeed, if \(\langle a_1, a_2 \rangle \in S \), then \(\mathop {\sim }\langle a_1 , a_2 \rangle = \langle a_2, \Box a_1 \rangle \in S\) because \(\Box \Box a_1 = \Box a_1 \), by Definition 2.1.ii. The same reasoning shows that S is closed under \(\wedge \). Regarding \(\vee \), it suffices to observe that \(a_2 \wedge b_2 = \Box a_2 \wedge \Box b_2 = \Box (a_2 \wedge b_2)\) for all \(\langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle \in S\) (the last equality holding true by Definition 2.1.i). A similar reasoning shows that S is closed under \(\rightarrow \), for we have \( \Box a_1 \wedge b_2 = \Box a_1 \wedge \Box b_2 = \Box (a_1 \wedge b_2)\).

It is clear that, on every twist-structure \(\mathbf {A} \le \mathbf {B}^{\bowtie } \), the operation \(\vee \) determines a semilattice structure (which is actually a lattice having \(\wedge \) as meet: see the next proposition). We shall use the symbol \(\le \) for this lattice order (overloaded to denote also the lattice order of the underlying Brouwerian algebra). It is easy to check that, for all \(\langle a_1 ,a_2 \rangle , \langle b_1, b_2 \rangle \in A\), one has \(\langle a_1 ,a_2 \rangle \le \langle b_1, b_2 \rangle \) iff (\(a_1 \le b_1\) and \(b_2 \le a_2\)).

From now on, given a twist-structure \(\mathbf {A} \) (or more generally any algebra \(\mathbf {A} \) having an operation \(\rightarrow \) ) and elements \(a,b \in A\), we shall abbreviate \(|a | : = a \rightarrow a\), and define the relations \(\mathop {\preceq }\) and \(\equiv \) as follows. We let \(a \mathop {\preceq }b \) iff \( a \rightarrow b = |a \rightarrow b |\), and \(\equiv {:=} \preceq \cap \mathrel {(\preceq )^{-1}}\). Thus, one has \(a \equiv b\) iff (\(a \mathop {\preceq }b\) and \(b \mathop {\preceq }a\)).

Proposition 2.3

For every \( \mathbf {A} \le \mathbf {B}^{\bowtie } \), the following hold.

  1. (i)

    The reduct \(\langle A; \wedge , \vee \rangle \) is a distributive lattice .

  2. (ii)

    The relation \(\preceq \) is a quasiorder (i.e., reflexive and transitive) on A.

  3. (iii)

    The relation \(\equiv \) is a congruence on the reduct \(\langle A; \wedge , \vee , \rightarrow \rangle \) and the quotient \(B(\mathbf {A} ) = \langle A; \wedge , \vee , \rightarrow \rangle /{\equiv }\) is a Brouwerian algebra. Moreover, the operator \(\nu \) given by \(\nu [a] : = \mathop {\sim }\mathop {\sim }a /{\equiv }\) for all \(a \in A\) is a nucleus in the sense of Definition 2.1, so the algebra \(\langle B(\mathbf {A} ), \nu \rangle \) is a nuclear Brouwerian algebra.

  4. (iv)

    For all \(a, b \in A\), it holds that \(\mathop {\sim }(a \rightarrow b) \equiv \mathop {\sim }\mathop {\sim }(a \wedge \mathop {\sim }b) \).

  5. (v)

    For all \(a, b \in A\), it holds that \(a \le b\) iff \(a \preceq b\) and \(\mathop {\sim }b \preceq \mathop {\sim }a\).

  6. (vi)

    For all \(a, b \in A\),

    1. 1.

      \(\mathop {\sim }(a \vee b) = \mathop {\sim }a \wedge \mathop {\sim }b\)

    2. 2.

      \(\mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }\mathop {\sim }b = \mathop {\sim }\mathop {\sim }(a \wedge b)\)

    3. 3.

      \(\mathop {\sim }a = \mathop {\sim }\mathop {\sim }\mathop {\sim }a\)

    4. 4.

      \(a \le \mathop {\sim }\mathop {\sim }a\).

Proof

In the following proofs, \(\langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle , \langle c_1, c_2 \rangle \) denote generic elements of \(\mathbf {A} = \langle A , \wedge ,\vee , \rightarrow , \mathop {\sim }\rangle \).

(i). It is clear that \(\langle A; \vee \rangle \) is a semilattice, whose order we will denote by \(\le _{\vee }\). Observe that \(\langle a_1, a_2 \rangle \le _{\vee } \langle b_1, b_2 \rangle \) iff \(a_1 \le b_1\) and \(b_2 \le a_2\), where \(\le \) denotes the lattice order of the Brouwerian algebra \(\mathbf {B} \). We proceed to show that \(\wedge \) is the meet relative to \(\le _{\vee }\). To this end, assume \(\langle a_1, a_2 \rangle \le _{\vee } \langle b_1, b_2 \rangle \), i.e., \(a_1 \le b_1\) and \(b_2 \le a_2\). Then we have \(a_1 = a_1 \wedge b_1\) and (recalling that \(a_2 = \Box a_2\)) \(\Box (a_2 \vee b_2 ) = \Box a_2 = a_2\), so \(\langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle = \langle a_1, a_2 \rangle \), as required. Conversely, assuming \(\langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle = \langle a_1, a_2 \rangle \), we have \(a_1 = a_1 \wedge b_1\) (so \(a_1 \le b_1\)) and \(\Box (a_2 \vee b_2 ) = a_2\). Since \(\Box \) is monotone (by Definition 2.1.i) and \(\Box b_2 = b_2\), from \(b_2 \le a_2 \vee b_2\) we have \(b_2 = \Box b_2 \le \Box (a_2 \vee b_2) = a_2\) and so \(b_2 \le a_2\), as required. It remains to check the distributive law. Recalling that the lattice reduct of \(\mathbf {B} \) is distributive, we compute:

$$\begin{aligned}&\langle a_1, a_2 \rangle \wedge ( \langle b_1, b_2 \rangle \vee \langle c_1, c_2 \rangle )\\&\quad = \langle a_1 \wedge (b_1 \vee c_1) , \Box (a_2 \vee (b_2 \wedge c_2) \rangle \\&\quad = \langle (a_1 \wedge b_1) \vee (a_1 \wedge c_1) , \Box ((a_2 \vee b_2) \wedge (a_2 \vee c_2) \rangle \\&\quad = \langle (a_1 \wedge b_1) \vee (a_1 \wedge c_1), \Box (a_2 \vee b_2)\\&\quad \wedge \Box (a_2 \vee c_2) \rangle \qquad \text {by Def.}~{2.1}.\text {i}\\&\quad = \langle a_1 \wedge b_1, \Box (a_2 \vee b_2) \rangle \vee \langle a_1 \wedge c_1, \Box (a_2 \vee c_2) \rangle \\&\quad = (\langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle ) \vee (\langle a_1, a_2 \rangle \wedge \langle c_1, c_2 \rangle ). \end{aligned}$$

(ii). Observe that,for all\(\langle a_1,a_2\rangle \!\in \! A\),one has \( | \langle a_1, a_2 \rangle | = \langle a_1 \rightarrow a_1, \Box a_1 \wedge a_2 \rangle = \langle 1, \Box a_1 \wedge a_2 \rangle \) and therefore \( \langle a_1, a_2 \rangle = | \langle a_1, a_2 \rangle | \) if and only if \(a_1 = 1\) (the latter equivalence holds because \(a_1= 1\) entails \(\Box a_1 \wedge a_2 = \Box 1 \wedge a_2 = 1 \wedge a_2 = a_2\)). Thus, \( \langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle = | \langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle |\) holds if and only if \(a_1 \rightarrow b_1 = 1\), which is equivalent (in a Brouwerian algebra) to \(a_1 \le b_1\). Thus, we have \(\langle a_1, a_2 \rangle \mathop {\preceq }\langle b_1, b_2 \rangle \) iff \(a_1 \le b_1\), which easily entails that the relation \(\mathop {\preceq }\) is reflexive and transitive.

(iii). By the preceding item, we have \( \langle a_1, a_2 \rangle \mathbin \equiv \langle b_1, b_2 \rangle \) if and only if \(a_1 = b_1\). Given the definitions of the operations \(\wedge , \vee \) and \(\rightarrow \), this easily entails that \(\mathbin \equiv \) is a congruence on the reduct \(\langle A; \wedge , \vee , \rightarrow \rangle \). Using these observations, it is easy to show that \(B(\mathbf {A} )\) is isomorphic to \(\mathbf {B} \). It remains to check that \(\nu \) is a nucleus on \(B(\mathbf {A} )\). This easily follows from the observation that \(\mathop {\sim }\mathop {\sim }\langle a_1, a_2 \rangle = \langle \Box a_1,\Box a_2 \rangle = \langle \Box a_1,a_2 \rangle \).

(iv). As observed above, we have \( \langle a_1, a_2 \rangle \mathbin \equiv \langle b_1, b_2 \rangle \) if and only if \(a_1 = b_1\). Thus, it suffices to check that the first components of \( \mathop {\sim }(\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle ) \) and \( \mathop {\sim }\mathop {\sim }(\langle a_1, a_2 \rangle \wedge \mathop {\sim }\langle b_1, b_2 \rangle ) \) are equal. We have \( \mathop {\sim }(\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle ) = \langle \Box a_1\wedge b_2, \Box ( a_1\rightarrow b_1) \rangle \) and \( \mathop {\sim }\mathop {\sim }(\langle a_1, a_2 \rangle \wedge \mathop {\sim }\langle b_1, b_2 \rangle ) = \mathop {\sim }\mathop {\sim }(\langle a_1\wedge b_2 , \Box (a_2 \vee \Box b_1) \rangle = \langle \Box ( a_1\wedge b_2 ) , \Box (a_2 \vee \Box b_1) \rangle \). Since \(\Box \) preserves finite meets and \(\Box b_2 = b_2\), we have \( \Box ( a_1\wedge b_2 ) = \Box a_1\wedge \Box b_2 = \Box a_1\wedge b_2\), as required.

(v). As observed in item (i), we have \(\langle a_1, a_2 \rangle \le \langle b_1, b_2 \rangle \) iff \(a_1 \le b_1 \) and \(b_2 \le a_2\). On the other hand, we noted in item (ii) that \(\langle a_1, a_2 \rangle \mathop {\preceq }\langle b_1, b_2 \rangle \) iff \(a_1 \le b_1\). To conclude the proof, it is sufficient to observe that \(\mathop {\sim }\langle b_1, b_2 \rangle = \langle b_2, \Box b_1\rangle \mathop {\preceq }\langle a_2, \Box a_1\rangle = \mathop {\sim }\langle a_1, a_2 \rangle \) iff \(b_2 \le a_2\).

(vi).1. The firstcomponentsof \(\mathop {\sim }( \langle a_1, a_2 \rangle \vee \langle b_1, b_2 \rangle ) \) and of \(\mathop {\sim }\langle a_1, a_2 \rangle \wedge \mathop {\sim }\langle b_1, b_2 \rangle \) are identical. The second ones are, respectively, \(\Box (a_1 \vee b_1) \) and \(\Box (\Box a_1\vee \Box b_1)\). Observe that Definition2.1.ii entails \(a_1 \vee b_1\le \Box a_1\vee \Box b\). Using Definition2.1.i (monotonicity of \(\Box \)), this gives us \(\Box (a_1 \vee b_1) \le \Box ( \Box a_1\vee \Box b_1) \). On the other hand, from \(a_1, b_1\le a_1\vee b_1\) we have \(\Box a_1,\Box b_1\le \Box (a_1 \vee b_1)\), so \(\Box a_1\vee \Box b_1\le \Box (a_1 \vee b_1)\). Using monotonicity of \(\Box \) and Definition2.1.ii, the latter gives us \(\Box (\Box a_1\vee \Box b_1) \le \Box \Box (a_1 \vee b_1) = \Box (a_1 \vee b_1) \), as required.

(vi).2. As observed earlier, the double negation does not affect second components. The first component of \(\mathop {\sim }\mathop {\sim }(\langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle ) \) is \(\Box (a_1 \wedge b_1)\), and the first component of \(\mathop {\sim }\mathop {\sim }\langle a_1, a_2 \rangle \wedge \mathop {\sim }\mathop {\sim }\langle b_1, b_2 \rangle \) is \(\Box a_1\wedge \Box b\). Thus, the result follows immediately from Definition 2.1.i.

(vi).3. Observe that the assumption \(a_2 = \Box a_2\) gives us \(\mathop {\sim }\mathop {\sim }\mathop {\sim }\langle a_1, a_2 \rangle = \langle \Box a_2, \Box a_1\rangle = \langle a_2, \Box a_1\rangle = \mathop {\sim }\langle a_1, a_2 \rangle \). (vi).4. As above, we only need to check the inequality of the first components, which easily follows from \(x \le \Box x\) (Definition 2.1.ii). \(\square \)

Items(vi)1. to (vi)4. of Proposition 2.3 entail that the \(\{\wedge , \vee , \mathop {\sim }\}\)-reduct of every quasi-N4 twist-structure is a lower quasi-De Morgan lattice in the terminology of Sankappanavar (see Definition 3.1 below), hence our choice of the terms quasi-N4 twist-structure and quasi-N4-lattice. Items (ii) and (v) also illustrate that the implication \(\rightarrow \) does not determine the lattice order on a twist-structure, in the sense that one can have \(a \rightarrow b = | a \rightarrow b |\) even if \(a \not \le b\). To restore the connection between order and implication that is common to many algebras of logic, one can define a second implication by \(x \Rightarrow y := (x \rightarrow y ) \wedge (\mathop {\sim }y \rightarrow \mathop {\sim }x)\). For every \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) and for all \(\langle a_1 ,a_2 \rangle , \langle b_1, b_2 \rangle \in A\), one has:

$$\begin{aligned}&\langle a_1 ,a_2 \rangle \Rightarrow \langle b_1, b_2 \rangle \\&\quad = \langle (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow a_2),\\&\qquad \Box ((\Box a_1 \wedge b_2) \vee (\Box b_2 \wedge \Box a_1)) \rangle \\&\quad = \langle (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow a_2),\\&\qquad \Box ((\Box a_1 \wedge \Box b_2) \vee (\Box b_2 \wedge \Box a_1)) \rangle \\&\quad = \langle (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow a_2), \Box (\Box a_1 \wedge \Box b_2) \rangle \\&\quad = \langle (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow a_2), \Box \Box a_1 \wedge \Box \Box b_2 \rangle \\&\quad = \langle (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow a_2), \Box a_1 \wedge b_2 \rangle . \end{aligned}$$

It is then easy to check that, for all \(a,b \in A\), one has \(a \Rightarrow b = | a \Rightarrow b |\) if and only if \(a \le b\). It follows that an equivalence connective can be defined by \(x \Leftrightarrow y := (x \Rightarrow y ) \wedge ( y \Rightarrow x)\), and one has:

$$\begin{aligned}&\langle a_1 ,a_2 \rangle \Leftrightarrow \langle b_1, b_2 \rangle = \langle (a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2), \\&\quad \Box ((\Box a_1 \wedge b_2) \vee (\Box b_1 \wedge a_2)) \rangle \end{aligned}$$

where \(a_1 \leftrightarrow b_1 := (a_1 \rightarrow b_1) \wedge (b_1 \rightarrow a_1)\). We then have \(a \Leftrightarrow b = | a \Leftrightarrow b |\) if and only if \(a = b\).

The next proposition shows that every quasi-N4 twist-structure satisfies (nearly) all the identities that were used by Odintsov (2008), Def. 8.5.1 to present the class of N4-lattices as a variety (Odintsov 2008, Thm. 8.5.3). The one exception is item (vii), which appears in Odintsov (2008), Def. 8.5.1 as \(|a| \le \mathop {\sim }(a \rightarrow b) \rightarrow a\), the latter being obviously equivalent to our item (vii) in an involutive context. Later on we are going to show (Proposition 3.7) that quasi-N4 twist-structures can also be presented as a variety of abstract algebras.

Proposition 2.4

(cf. Odintsov 2008, Def. 8.5.1) For every \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) and for all \(a,b,c \in A\), the following hold.

  1. (i)

    \(|a| \rightarrow b = b \).

  2. (ii)

    \((a \wedge b) \rightarrow c = a \rightarrow (b \rightarrow c)\).

  3. (iii)

    \(a \rightarrow (b \wedge c) = (a \rightarrow b) \wedge (a \rightarrow c) \).

  4. (iv)

    \((a \vee b) \rightarrow c = (a \rightarrow c) \wedge (b \rightarrow c)\).

  5. (v)

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

  6. (vi)

    \((a \rightarrow b) \wedge (b \rightarrow c) \mathop {\preceq }a \rightarrow c\).

  7. (vii)

    \(|a| \le \mathop {\sim }(a \rightarrow b) \rightarrow \mathop {\sim }\mathop {\sim }a\).

  8. (viii)

    \(|a| \le b \rightarrow (\mathop {\sim }a \rightarrow \mathop {\sim }(b \rightarrow a ))\).

  9. (ix)

    \(|a| \le \mathop {\sim }(b \rightarrow a ) \rightarrow \mathop {\sim }a \).

  10. (x)

    \(a \wedge (a \rightarrow b) \le b \vee \mathop {\sim }(\mathop {\sim }b \rightarrow \mathop {\sim }a)\).

  11. (xi)

    \(a \le |b| \vee \mathop {\sim }(\mathop {\sim }b \rightarrow \mathop {\sim }a)\).

  12. (xii)

    \((a \Leftrightarrow b) \rightarrow a = (a \Leftrightarrow b ) \rightarrow b\).

  13. (xiii)

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

  14. (xiv)

    \(a \rightarrow b \mathop {\preceq }\mathop {\sim }\mathop {\sim }a \rightarrow \mathop {\sim }\mathop {\sim }b \).

  15. (xv)

    \((a \wedge b) \rightarrow a = |(a \wedge b) \rightarrow a|\).

  16. (xvi)

    \(a \rightarrow b \mathop {\preceq }a \rightarrow (b \vee c)\).

Proof

(i). Here and in subsequent items, we denote by \(a= \langle a_1, a_2 \rangle , b= \langle b_1, b_2 \rangle , c= \langle c_1, c_2 \rangle \) generic elements of \(\mathbf {A} \). Observe that \(|\langle a_1, a_2 \rangle | = \langle a_1 \rightarrow a_1 , \Box a_1 \wedge a_2 \rangle = \langle 1, \Box a_1 \wedge a_2 \rangle \). Thus, \(|\langle a_1, a_2 \rangle | \rightarrow \langle b_1, b_2 \rangle = \langle 1 \rightarrow b_1, \Box 1 \wedge b_2 \rangle = \langle b_1, b_2 \rangle \), as required.

(ii). We have \(( \langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle ) \rightarrow \langle c_1, c_2 \rangle = \langle (a_1 \wedge b_1) \rightarrow c_1, \Box (a_1 \wedge b_1) \wedge c_2 \rangle \) and \( \langle a_1, a_2 \rangle \rightarrow (\langle b_1, b_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) = \langle a_1 \rightarrow (b_1 \rightarrow c_1), \Box a_1 \wedge \Box b_1 \wedge c_2 \rangle \). To obtain the desired result, it suffices to observe that every nuclear Brouwerian algebra satisfies \((x \wedge y) \rightarrow z \approx x \rightarrow (y \rightarrow z) \) and \(\Box (x \wedge y) \approx \Box x \wedge \Box y\).

(iii). We have \(\langle a_1, a_2 \rangle \rightarrow (\langle b_1, b_2 \rangle \wedge \langle c_1, c_2 \rangle ) = \langle a_1 \rightarrow (b_1 \wedge c_1), \Box a_1 \wedge \Box (b_2 \vee c_2) \rangle \) and \( (\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle ) \wedge (\langle a_1, a_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) = \langle (a_1 \rightarrow b_1) \wedge (a_1 \rightarrow c_1), \Box ((\Box a_1 \wedge b_2 ) \vee (\Box a_1 \wedge c_2 )) \rangle \). Equality of the first components then follows from the observation that every Brouwerian algebra satisfies \( x \rightarrow (y \wedge z) \approx (x \rightarrow y ) \wedge (x \rightarrow z)\). Regarding the second components, using the identity \(\Box (x \wedge y) \approx \Box x \wedge \Box y\) and distributivity, we have \(\Box a_1 \wedge \Box (b_2 \vee c_2) = \Box ( a_1 \wedge (b_2 \vee c_2) ) = \Box ( (a_1 \wedge b_2) \vee (a_1 \wedge c_2) ) \). Recalling that \(\Box b_2 = b_2\) and \(\Box c_2 = c_2\), we also have \(\Box ((\Box a_1 \wedge b_2 ) \vee (\Box a_1 \wedge c_2 )) = \Box ((\Box a_1 \wedge \Box b_2 ) \vee (\Box a_1 \wedge \Box c_2 )) = \Box (\Box ( a_1 \wedge b_2 ) \vee \Box ( a_1 \wedge c_2 )) \). The desired result then follows from the observation (made in the proof of Proposition 2.3.vi.1) that every nuclear Brouwerian algebra satisfies \(\Box (x \vee y ) \approx \Box (\Box x \vee \Box y)\).

(iv). Let us compute \((\langle a_1, a_2 \rangle \vee \langle b_1, b_2 \rangle ) \rightarrow \langle c_1, c_2 \rangle = \langle (a_1 \vee b_1) \rightarrow c_1, \Box (a_1 \vee b_1) \wedge c_2 \rangle \) and \((\langle a_1, a_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) \wedge (\langle b_1, b_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) = \langle (a_1 \rightarrow c_1) \wedge (b_1 \rightarrow c_1) , \Box ( (\Box a_1 \wedge c_2 ) \vee (\Box b_1 \wedge c_2 ) )\rangle \). The equality of the first components follows from the observation that every Brouwerian algebra satisfies \((x \vee y) \rightarrow z \approx (x \rightarrow z) \wedge (y \rightarrow z)\). Regarding the second components, we have \( \Box (a_1 \vee b_1) \wedge c_2 = \Box (a_1 \vee b_1) \wedge \Box c_2 = \Box ((a_1 \vee b_1) \wedge c_2) = \Box ((a_1 \vee c_2) \wedge (b_1 \vee c_2) )\) and \(\Box ( (\Box a_1 \wedge c_2 ) \vee (\Box b_1 \wedge c_2 ) ) = \Box ( (\Box a_1 \wedge \Box c_2 ) \vee (\Box b_1 \wedge \Box c_2 ) ) = \Box ( \Box ( a_1 \wedge c_2 ) \vee \Box ( b_1 \wedge c_2 ) ) \) The result then follows because, as observed in item (iii) above, every nuclear Brouwerian algebra satisfies \(\Box (x \vee y ) \approx \Box (\Box x \vee \Box y)\).

(v). In order to verify this and the subsequent inequalities, recall that \(\langle a_1, a_2 \rangle \le \langle b_1, b_2 \rangle \) iff (\(a_1 \le b_1 \) and \(b_2 \le a_2\)). Since \(\Box b_1 \wedge a_2 \le a_2\) and \(\langle b_1, b_2 \rangle \rightarrow \langle a_1, a_2 \rangle = \langle b_1 \rightarrow a_1 , \Box b_1 \wedge a_2 \rangle \), the result follows from the observation that every Brouwerian algebra satisfies \(x \le y \rightarrow x\).

(vi). It is sufficient to check the inequality of the first components of the expressions \((\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle ) \wedge (\langle b_1, b_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) \) and \( \langle a_1, a_2 \rangle \rightarrow \langle c_1, c_2 \rangle \). These are, respectively, \((a_1 \rightarrow b_1) \wedge (b_1 \rightarrow c_1)\) and \(a_1 \rightarrow c_1\). The result then follows, for every Brouwerian algebra satisfies \((x \rightarrow y) \wedge (y \rightarrow z ) \le x \rightarrow z\).

(vii). As we have seen earlier, \(|\langle a_1, a_2 \rangle | = \langle 1, \Box a_1 \wedge a_2 \rangle \). To obtain the desired result, it suffices to compute \(\mathop {\sim }(\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle ) \rightarrow \mathop {\sim }\mathop {\sim }\langle a_1, a_2 \rangle = \langle (\Box a_1 \wedge b_1) \rightarrow \Box a_1, \Box (\Box a_1 \wedge b_1) \wedge a_2 \rangle = \langle 1, \Box \Box a_1 \wedge \Box b_1 \wedge a_2 \rangle = \langle 1, \Box a_1 \wedge \Box b_1 \wedge a_2 \rangle \).

(viii). Recall that \(|\langle a_1, a_2 \rangle | = \langle 1, \Box a_1 \wedge a_2 \rangle \). To obtain the desired result, let us compute \(\langle b_1, b_2 \rangle \rightarrow (\mathop {\sim }\langle a_1, a_2 \rangle \rightarrow \mathop {\sim }(\langle b_1, b_2 \rangle \rightarrow \langle a_1, a_2 \rangle )) = \langle b_1 \rightarrow (a_2 \rightarrow (\Box b_1 \wedge a_2)) , \Box b_1 \wedge \Box a_2 \wedge \Box (b_1 \rightarrow a_1) \rangle = \langle 1 , \Box a_1 \wedge \Box a_2 \wedge \Box b_1 \rangle \). The last equality was obtained as follows: one the one hand, using the laws of Brouwerian algebras and the identity \(x \le \Box x\), we have \(b_1 \rightarrow (a_2 \rightarrow (\Box b_1 \wedge a_2)) = (b_1 \wedge a_2) \rightarrow (\Box b_1 \wedge a_2) = 1\). On the other hand, recalling that \(\Box \) preserves finite meets, we have \(\Box b_1 \wedge \Box (b_1 \rightarrow a_1) = \Box (b_1 \wedge (b_1 \rightarrow a_1)) = \Box (b_1 \wedge a_1) = \Box b_1 \wedge \Box a_1 \).

(ix). Recalling that \(\Box a_2 = a_2\), we compute \(\mathop {\sim }(\langle b_1, b_2 \rangle \rightarrow \langle a_1, a_2 \rangle ) \rightarrow \mathop {\sim }\langle a_1, a_2 \rangle = \langle ( \Box b_1 \wedge a_2) \rightarrow a_2, \Box ( \Box b_1 \wedge a_2) \wedge \Box a_1 \rangle = \langle 1, \Box \Box b_1 \wedge \Box a_2 \wedge \Box a_1 \rangle = \langle 1, \Box b_1 \wedge a_2 \wedge \Box a_1 \rangle \). The result then follows.

(x). Let us compute \(\langle a_1, a_2 \rangle \wedge (\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle ) = \langle a_1 \wedge (a_1 \rightarrow b_1), \Box (a_2 \vee (\Box a_1 \wedge b_2) )\rangle = \langle a_1 \wedge b_1, \Box (a_2 \vee (\Box a_1 \wedge b_2) )\rangle \) and \( \langle b_1, b_2 \rangle \vee \mathop {\sim }(\mathop {\sim }\langle b_1, b_2 \rangle \rightarrow \mathop {\sim }\langle a_1, a_2 \rangle ) = \langle b_1 \vee (\Box b_2 \wedge \Box a_1), b_2 \wedge \Box (b_2 \rightarrow a_2 ) \rangle = \langle b_1 \vee (\Box b_2 \wedge \Box a_1), b_2 \wedge a_2 \rangle \). The last equality was obtained using \(\Box b_2 = b_2\) and the observation that \(\Box \) preserves finite meets. Since \(a_1 \wedge b_1 \le b_1 \le b_1 \vee (\Box b_2 \wedge \Box a_1)\) and \(b_2 \wedge a_2 \le a_2 \le \Box a_2 \le \Box (a_2 \vee (\Box a_1 \wedge b_2) )\), the result follows.

(xi). The result easily follows if we compute \(| \langle b_1, b_2 \rangle | \vee \mathop {\sim }(\mathop {\sim }\langle b_1, b_2 \rangle \rightarrow \mathop {\sim }\langle a_1, a_2 \rangle ) = \langle 1 \vee (\Box b_2 \wedge \Box a_1) , \Box b_1 \wedge b_2 \wedge \Box ( b_2 \rightarrow a_2) \rangle = \langle 1 , \Box b_1 \wedge b_2 \wedge a_2 \rangle \), where the last equality holds because \(b_2 \wedge \Box ( b_2 \rightarrow a_2) = \Box b_2 \wedge \Box ( b_2 \rightarrow a_2) = \Box (b_2 \wedge ( b_2 \rightarrow a_2)) = \Box (b_2 \wedge a_2) = \Box b_2 \wedge \Box a_2 = b_2 \wedge a_2\).

(xii). As observed earlier, \(\langle a_1 ,a_2 \rangle \Leftrightarrow \langle b_1, b_2 \rangle = \langle (a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2), \Box ((\Box a_1 \wedge b_2) \vee (\Box b_1 \wedge a_2)) \rangle \). Thus, \( (\langle a_1 ,a_2 \rangle \Leftrightarrow \langle b_1, b_2 \rangle ) \rightarrow \langle a_1, a_2 \rangle = \langle ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \rightarrow a_1, \Box ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \wedge a_2 \rangle \) and, likewise, \( (\langle a_1 ,a_2 \rangle \Leftrightarrow \langle b_1, b_2 \rangle ) \rightarrow \langle b_1, b_2 \rangle = \langle ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \rightarrow b_1, \Box ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \wedge b_2 \rangle \). Note that by item (ii) above we have \(((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \rightarrow a_1 = (a_2 \leftrightarrow b_2) \rightarrow ( (a_1 \leftrightarrow b_1) \rightarrow a_1 )\) and, similarly, \(((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \rightarrow b_1 = (a_2 \leftrightarrow b_2) \rightarrow ( (a_1 \leftrightarrow b_1) \rightarrow b_1 )\). Then the equality of the first components is guaranteed by the identity \((x \leftrightarrow y) \rightarrow x \approx (x \leftrightarrow y ) \rightarrow y\), which holds on every Brouwerian algebra. As to the second components, since \(a_2 = \Box a_2\), we have \(\Box ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \wedge a_2 = \Box ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \wedge \Box a_2 = \Box ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2) \wedge a_2) = \Box ((a_1 \leftrightarrow b_1) \wedge (b_2 \rightarrow a_2) \wedge (a_2 \rightarrow b_2) \wedge a_2) = \Box ((a_1 \leftrightarrow b_1) \wedge (b_2 \rightarrow a_2) \wedge a_2 \wedge b_2) = \Box ((a_1 \leftrightarrow b_1) \wedge a_2 \wedge b_2 \wedge a_2) = \Box ((a_1 \leftrightarrow b_1) \wedge a_2 \wedge b_2) \). A similar reasoning shows that \(\Box ((a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2)) \wedge b_2 = \Box ((a_1 \leftrightarrow b_1) \wedge a_2 \wedge b_2) \), thus concluding our proof.

(xiii). Let us compute \( \langle a_1, a_2 \rangle \rightarrow (\langle b_1, b_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) = \langle a_1 \rightarrow ( b_1 \rightarrow c_1) , \Box a_1 \wedge \Box b_2 \wedge c_2 \rangle \) and \( (\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle ) \rightarrow (\langle a_1, a_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) = \langle (a_1 \rightarrow b_1) \rightarrow (a_1 \rightarrow c_1 ) , \Box (a_1 \rightarrow b_1) \wedge \Box a_1 \wedge c_2 \rangle \). Equality of the first components is thus a consequence of the identity \(x \rightarrow (y \rightarrow z) \approx (x \rightarrow y) \rightarrow (x \rightarrow z) \), which is valid on every Brouwerian algebra. Regarding the second components, since the \(\Box \) operation preserves finite meets, we have \(\Box (a_1 \rightarrow b_1) \wedge \Box a_1 \wedge c_2 = \Box ((a_1 \rightarrow b_1) \wedge a_1) \wedge c_2 =\Box (a_1 \wedge b_1) \wedge c_2 =\Box a_1 \wedge \Box b_1 \wedge c_2 \), as required.

(xiv). We only need to take care of the first components of \(\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle \) and \(\mathop {\sim }\mathop {\sim }\langle a_1, a_2 \rangle \rightarrow \mathop {\sim }\mathop {\sim }\langle b_1, b_2 \rangle \). These are, respectively, \(a_1 \rightarrow b_1 \) and \(\Box a_1 \rightarrow \Box b_1\). Since \(x \le \Box x\) is valid on every nuclear Brouwerian algebra, to show that \(a_1 \rightarrow b_1 \le \Box a_1 \rightarrow \Box b_1\), it suffices to check that \(\Box (a_1 \rightarrow b_1) \le \Box a_1 \rightarrow \Box b_1\). By residuation, we have \(\Box (a_1 \rightarrow b_1) \le \Box a_1 \rightarrow \Box b_1\) iff \(\Box a_1 \wedge \Box (a_1 \rightarrow b_1) \le \Box b_1\). Since \(\Box a_1 \wedge \Box (a_1 \rightarrow b_1) = \Box (a_1 \wedge (a_1 \rightarrow b_1)) = \Box (a_1 \wedge b_1) = \Box a_1 \wedge \Box b_1 \le \Box b_1\), the result follows.

(xv). Recalling item (ii), we have \(( \langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle ) \rightarrow \langle a_1, a_2 \rangle = \langle (a_1 \wedge b_1) \rightarrow a_1, \Box (a_1 \wedge b_1) \wedge a_2 \rangle = \langle 1, \Box (a_1 \wedge b_1) \wedge a_2 \rangle \) and \(| \langle 1, \Box (a_1 \wedge b_1) \wedge a_2 \rangle | = \langle 1 \rightarrow 1, \Box 1 \wedge \Box (a_1 \wedge b_1) \wedge a_2 \rangle = \langle 1, \Box (a_1 \wedge b_1) \wedge a_2 \rangle \), as required.

(xvi). As observed earlier (item (ii) of Proposition 2.3), it suffices to check that \(a_1 \rightarrow b_1 \le a \rightarrow (b_1 \vee c_1)\), which obviously holds in a Brouwerian algebra. \(\square \)

The next proposition provides a recipe for producing concrete examples of quasi-N4 twist-structures.

Let \(\mathbf {B}\) be a nuclear Brouwerian algebra, and let \(\nabla , \Delta \subseteq B\). We shall say that \(\nabla \) is a dense filter if \(\nabla \) is a lattice filter of \(\langle B; \wedge , \vee \rangle \) and, for all \(a,b \in B\), one has \(\Box a \vee (a \rightarrow b) \in \nabla \). We shall say that \(\Delta \) is a \(\Box \)-ideal if \(\Delta \) is a (non-empty) lattice ideal of \(\langle B; \wedge , \vee \rangle \) and \(\Box a \in \Delta \) whenever \(a \in \Delta \). Let \(\mathbf {B}^{\bowtie }\) be the algebra introduced in Definition 2.2, and let \(\nabla , \Delta \subseteq B\) be, respectively, a dense filter and a \(\Box \)-ideal of \(\mathbf {B}\). Consider the set:

$$\begin{aligned} Tw \langle B, \nabla , \Delta \rangle := & {} \{ \langle a_1, a_2 \rangle \in B \times B :\\ a_2= & {} \Box a_2, \, a_1 \vee a_2 \in \nabla , \, a_1 \wedge a_2 \in \Delta \}. \end{aligned}$$

Proposition 2.5

The set \(Tw \langle B, \nabla , \Delta \rangle \) is closed under all the operations of \(\mathbf {B}^{\bowtie }\), and is therefore the universe of a twist-structure over \(\mathbf {B}\).

Proof

The case of negation is easy. Assume \(\langle a_1, a_2 \rangle \in Tw \langle B, \nabla , \Delta \rangle \), so \(a_2 = \Box a_2 \), \(a_1 \vee a_2 \in \nabla \) and \(a_1 \wedge a_2 \in \Delta \). To show that \(\mathop {\sim }\langle a_1, a_2 \rangle = \langle a_2, \Box a_1 \rangle \in A\), we need to check that \(\Box a_1 = \Box \Box a_1 \), \(a_2 \vee \Box a_1 \in \nabla \) and \(a_2 \wedge \Box a_1 \in \Delta \). The first condition follows from Definition 2.1.ii, which also entails \(a_1 \vee a_2 \le a_2 \vee \Box a_1 \). Then \(a_2 \vee \Box a_1 \in \nabla \), because \(\nabla \) is increasing. The last condition follows from Definition 2.1.i and the fact that \(\Delta \) is \(\Box \)-closed: we have that \(a_1 \wedge a_2 \in \Delta \) entails \(\Box (a_1 \wedge a_2) = \Box a_1 \wedge \Box a_2 = \Box a_1 \wedge a_2 \in \Delta \).

Letting \(\langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle \in A\), we check that A is closed under conjunction. Since \(\langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle = \langle a_1 \wedge b_1, \Box (a_2 \vee b_2) \rangle \), we need to show that \(\Box \Box (a_2 \vee b_2) = \Box (a_2 \vee b_2) \), which is immediate, that \((a_1 \wedge b_1) \vee \Box (a_2 \vee b_2) \in \nabla \) and \(a_1 \wedge b_1 \wedge \Box (a_2 \vee b_2) \in \Delta \). Regarding \((a_1 \wedge b_1) \vee \Box (a_2 \vee b_2) \in \nabla \), observe that, by distributivity, we have \( (a_1 \wedge b_1) \vee \Box (a_2 \vee b_2) = (a_1 \vee \Box (a_2 \vee b_2)) \wedge (b_1 \vee \Box (a_2 \vee b_2))\). Since \(\nabla \) is increasing, it is thus sufficient to show that \((a_1 \vee a_2 \vee b_2) \wedge ( b_1 \vee a_2 \vee b_2) \in \nabla \). By assumption, \(a_1 \vee a_2 , b_1 \vee b_2 \in \nabla \), so \(a_1 \vee a_2 \vee b_2, b \vee a_2 \vee b_2 \in \nabla \), because \(\nabla \) is increasing. Since \(\nabla \) is closed under finite meets, we conclude \((a \vee a_2 \vee b_2) \wedge ( b \vee a_2 \vee b_2) \in \nabla \), as claimed. Regarding \(a_1\wedge b_1\wedge \Box (a_2 \vee b_2) \in \Delta \), observe that, using items (ii) and (i) of Definition 2.1, we have \(a_1\wedge b_1\wedge \Box (a_2 \vee b_2) \le \Box (a_1\wedge b_1 ) \wedge \Box (a_2 \vee b_2) = \Box (a_1\wedge b_1\wedge (a_2 \vee b_2))\). Since \(\Delta \) is decreasing, it is thus sufficient to show that \(\Box (a_1\wedge b_1\wedge (a_2 \vee b_2)) \in \Delta \). By distributivity, we have \(\Box (a_1\wedge b_1\wedge (a_2 \vee b_2)) = \Box ( (a_1\wedge b_1\wedge a_2) \vee (a_1\wedge b_1\wedge b_2) )\). Since \(\Delta \) is decreasing, the assumption \(a_1\wedge b_1\in \Delta \) entails \(a_1\wedge b_1\wedge a_2, a_1\wedge b_1\wedge b_2 \in \Delta \). Then \( (a_1\wedge b_1\wedge a_2) \vee (a_1\wedge b_1\wedge b_2) \in \Delta \), because \(\Delta \) is closed under finite joins. Finally, we use the property of being \(\Box \)-closed to conclude \( \Box ( (a_1\wedge b_1\wedge a_2) \vee (a_1\wedge b_1\wedge b_2) ) \in \Delta \), as claimed.

The case of disjunction is more straightforward. We need to show that \(\Box (a_2 \wedge b_2) = a_2 \wedge b_2 \), that \(a_1\vee b_1\vee (a_2 \wedge b_2) \in \nabla \) and \((a_1\vee b_1) \wedge a_2 \wedge b_2 \in \Delta \). The first claim follows from Definition 2.1.i, for the assumptions \(\Box a_2 = a_2\) and \(\Box b_2 = b_2\) imply \(\Box (a_2 \wedge b_2) = \Box a_2 \wedge \Box b_2 = a_2 \wedge b_2\). As to \(a_1\vee b_1\vee (a_2 \wedge b_2) \in \nabla \), by distributivity we have \(a_1\vee b_1\vee (a_2 \wedge b_2) = (a_1\vee b_1\vee a_2) \wedge (a_1\vee b_1\vee b_2)\), so the result can be established as in the case of conjunction. Likewise, to obtain \((a_1\vee b) \wedge a_2 \wedge b_2 \in \Delta \) we can use distributivity to have \((a_1\vee b) \wedge a_2 \wedge b_2 = (a_1\wedge a_2 \wedge b_2) \vee (b_1\wedge a_2 \wedge b_2)\) and reason as before.

Finally, to check that A is closed under \(\rightarrow \), we need to show that \(\Box (\Box a_1 \wedge b_2) = \Box a_1 \wedge b_2\), \((a_1 \rightarrow b_1) \vee (\Box a_1 \wedge b_2) \in \nabla \), and \((a_1 \rightarrow b_1) \wedge \Box a_1 \wedge b_2 \in \Delta \). Using Definition 2.1 and the assumption that \(\Box b_2 = b_2\), we have \(\Box (\Box a_1 \wedge b_2) = \Box \Box a_1\wedge \Box b_2 = \Box a_1 \wedge b_2\). To show that \((a_1 \rightarrow b_1) \vee (\Box a_1 \wedge b_2) = ((a_1\rightarrow b_1) \vee \Box a_1) \wedge ((a_1\rightarrow b_1) \vee b_2) \in \nabla \), observe that \((a_1\rightarrow b_1) \vee \Box a_1 \in \nabla \) because \(\nabla \) is dense, and, by the properties of the implication (in particular, the inequality \(x \le y \rightarrow x\)), we have \(b_1\vee b_2 \le (a_1\rightarrow b_1) \vee b_2\). Since \(\nabla \) is increasing, the assumption that \( b_1\vee b_2 \in \nabla \) gives us the required result. Lastly, to show that \((a_1 \rightarrow b_1) \wedge \Box a_1 \wedge b_2 \in \Delta \), recall that, by assumption, \(b_1\wedge b_2 \in \Delta \). Thus, \(b_1\wedge b_2 \wedge a_1\in \Delta \), because \(\Delta \) is decreasing. Since \(\Delta \) is \(\Box \)-closed, we thus have \(\Box (b_1\wedge b_2 \wedge a_1) \in \Delta \). To finish the proof, it is sufficient to observe that \((a_1 \rightarrow b_1) \wedge \Box a_1 \wedge b_2 \le \Box (a_1\rightarrow b) \wedge \Box a_1\wedge \Box b_2 = \Box ((a_1\rightarrow b_1) \wedge a_1\wedge b_2) = \Box (b_1\wedge a_1\wedge b_2) \), where the last equality holds because \(x \wedge (x \rightarrow y) = x \wedge y \) holds on every Brouwerian algebra. \(\square \)

Example 2.6

Let \(\mathbf {B} = \langle B, \wedge , \vee ,\rightarrow \Box \rangle \) be a nuclear Brouwerian algebra whose lattice reduct is the three-element Heyting algebra with universe \(B = \{0, a, 1 \}\). The nucleus on B is defined by \(\Box 0 = 0\) and \(\Box a = \Box 1 = 1\). The largest quasi-N4 twist-structure over \(\mathbf {B}^{\bowtie } \) is the six-element algebra \(\mathbf {A} _6\) depicted in Fig. 1, which is constructed as \(Tw \langle B, B, B \rangle \) according to Proposition 2.5. By letting \(\nabla = \{a, 1 \}\) and \(\Delta = B\), one obtains the five-element subalgebra \(\mathbf {A} _5\) with universe \(A_5 = A_6 - \{ \langle 0, 0 \rangle \}\). Likewise, the four-element chain \(\mathbf {A} _4\), corresponding to the choice \(\nabla = \{1 \}\) and \(\Delta = B\), has universe \(A_4 = A_5 - \{ \langle a, 0 \rangle \}\). Note that all these algebras are neither quasi-Nelson algebras nor N4-lattices.

Fig. 1
figure 1

Quasi-N4-lattices as twist-structures

3 The variety of quasi-N4-lattices

In this section we introduce the abstract class of quasi-N4-lattices (Definition 3.2) and proceed to show that each quasi-N4-lattice can be viewed as a twist-structure of the type introduced above (Theorem 3.3). We then use this result to prove that quasi-N4-lattices form a variety (Proposition 3.7) and to establish a number of other results about filters and congruences on these algebras. We are going take the properties in Proposition 2.3 as our official definition for quasi-N4-lattices. As mentioned earlier, just as the implication-free reduct of every N4-lattice forms an algebra that is known in the literature as a De Morgan lattice, so the implication-free reducts of quasi-N4-lattices from structures that have been studied before under the name of quasi-De Morgan latticesFootnote 4.

Definition 3.1

(cf. Sankappanavar (1987)) A semi-De Morgan lattice is an algebra \( \langle A; \wedge , \vee , \mathop {\sim }\rangle \) of type \(\langle 2,2,1 \rangle \) such that \(\langle A; \wedge , \vee \rangle \) is a distributive lattice and the following identities are satisfied:

  1. (SDM1)

    \(\mathop {\sim }(x \vee y) \approx \mathop {\sim }x \wedge \mathop {\sim }y\).

  2. (SDM2)

    \(\mathop {\sim }\mathop {\sim }(x \wedge y) \approx \mathop {\sim }\mathop {\sim }x \wedge \mathop {\sim }\mathop {\sim }y\).

  3. (SDM3)

    \(\mathop {\sim }x \approx \mathop {\sim }\mathop {\sim }\mathop {\sim }x\).

A De Morgan lattice is a semi-De Mogan lattice that is involutive, i.e., one that satisfies \(x \approx \mathop {\sim }\mathop {\sim }x\). A (lower) quasi-De Morgan lattice is a semi-De Morgan lattice additionally satisfying \( x \le \mathop {\sim }\mathop {\sim }x\) (here, \(\alpha \le \beta \) is a shorthand for the identity \(\alpha \approx \alpha \wedge \beta \)).

Definition 3.2

A quasi-N4-lattice (QN4-lattice) is an algebra \(\mathbf {A} = \langle A; \wedge , \vee , \rightarrow , \mathop {\sim }\rangle \) of type \(\langle 2, 2, 2, 1 \rangle \) satisfying the following properties:

  1. (QN4a)

    The reduct \(\langle A; \wedge , \vee \rangle \) is a distributive lattice (with order \(\le \)).

  2. (QN4b)

    The relation \(\equiv {:=} \preceq \cap \mathrel {(\preceq )^{-1}}\) is a congruence on the reduct \(\langle A; \wedge , \vee , \rightarrow \rangle \) and the quotient \(B(\mathbf {A} ) = \langle A; \wedge , \vee , \rightarrow \rangle /{\equiv }\) is a Brouwerian algebra. Moreover, the operator \(\Box \) given by \(\Box [a] : = \mathop {\sim }\mathop {\sim }a /{\equiv }\) for all \(a \in A\) is a nucleus, so the algebra \(\langle B(\mathbf {A} ), \Box \rangle \) is a nuclear Brouwerian algebra.

  3. (QN4c)

    For all \(a, b \in A\), it holds that \(\mathop {\sim }(a \rightarrow b) \equiv \mathop {\sim }\mathop {\sim }(a \wedge \mathop {\sim }b)\).

  4. (QN4d)

    For all \(a, b \in A\), it holds that \(a \le b\) iff \(a \preceq b\) and \(\mathop {\sim }b \preceq \mathop {\sim }a\).

  5. (QN4e)

    For all \(a, b \in A\),

    1. (QN4e.1)

      \(\mathop {\sim }(a \vee b) = \mathop {\sim }a \wedge \mathop {\sim }b\)

    2. (QN4e.2)

      \(\mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }\mathop {\sim }b = \mathop {\sim }\mathop {\sim }(a \wedge b)\)

    3. (QN4e.3)

      \(\mathop {\sim }a = \mathop {\sim }\mathop {\sim }\mathop {\sim }a\)

    4. (QN4e.4)

      \(a \le \mathop {\sim }\mathop {\sim }a\)

The previous definitions entail that the \(\{ \rightarrow \}\)-free reduct of a quasi-N4-lattice is a lower quasi-De Morgan lattice (cf. Proposition 3.4). Obviously Definition 3.2 generalizes the one introduced by Odintsov for N4-lattices Odintsov (2004) as well as the definition of quasi-Nelson algebras first introduced in Rivieccio and Spinks (2019); see Proposition 3.8 below for a more precise statement of the relations among these classes of algebras.

Theorem 3.3

Every quasi-N4-lattice \(\mathbf {A} = \langle A; \wedge , \vee , \rightarrow , \mathop {\sim }\rangle \) is isomorphic to a twist-structure over \(\langle B(\mathbf {A} ), \Box \rangle \) through the map \(\iota :A \rightarrow A /{\equiv } \times A /{\equiv }\) given by \(\iota (a) : = \langle a /{\equiv }, \mathop {\sim }a /{\equiv } \rangle \) for all \(a \in A\).

Proof

Item (QN4b) in Definition 3.2 guarantees that \(\langle B(\mathbf {A} ), \Box \rangle ^{\bowtie }\) is a nuclear Brouwerian algebra, so one can apply Definition 2.2 to obtain the algebra \(\langle B(\mathbf {A} ), \Box \rangle ^{\bowtie }\). Item (QN4d) ensures that the map \(\iota \) is injective. Also observe that the requirement \(\pi _1[\iota (A)] = A /{\equiv }\) from Definition 2.2 is trivially satisfied. We shall denote by [a] the equivalence class of each \(a \in A\) modulo the relation \(\mathbin \equiv \). Thus, \(\iota (a) = \langle [a], [\mathop {\sim }a ] \rangle \) for all \(a \in A\); notice that, by (QN4e.3), we have \(\Box [\mathop {\sim }a ] = [\mathop {\sim }\mathop {\sim }\mathop {\sim }a ] = [\mathop {\sim }a]\), as required by Definition 2.2. Let us check that \(\iota \) preserves the algebraic operations. The case of negation is straightforward: for all \(a \in A\), we have \(\iota (\mathop {\sim }a) = \langle [\mathop {\sim }a ], [\mathop {\sim }\mathop {\sim }a] \rangle = \langle [\mathop {\sim }a ], \Box [a] \rangle = \mathop {\sim }\langle [a], [\mathop {\sim }a ] \rangle = \mathop {\sim }\iota (a) \). Regarding the meet, we have:

$$\begin{aligned} \iota (a \wedge b)&= \langle [a \wedge b], [\mathop {\sim }(a \wedge b) ]\rangle \\&= \langle [a \wedge b], [\mathop {\sim }\mathop {\sim }\mathop {\sim }( a \wedge b) ] \rangle&\text {by (QN4e.3)} \\&= \langle [a \wedge b], [\mathop {\sim }(\mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }\mathop {\sim }b) ] \rangle&\text {by (QN4e.2)} \\&= \langle [a \wedge b], [\mathop {\sim }\mathop {\sim }(\mathop {\sim }a \vee \mathop {\sim }b) ] \rangle&\text {by (QN4e.1)} \\&= \langle [a \wedge b], \Box [\mathop {\sim }a \vee \mathop {\sim }b ] \rangle \\&= \langle [a] \wedge [b], \Box ([\mathop {\sim }a ] \vee [\mathop {\sim }b ]) \rangle \\&= \langle [a], [\mathop {\sim }a ] \rangle \wedge \langle [b], [\mathop {\sim }b ] \rangle \\&= \iota (a) \wedge \iota (b). \end{aligned}$$

Regarding the join:

$$\begin{aligned} \iota (a \vee b)&= \langle [a \vee b], [\mathop {\sim }(a \vee b) ]\rangle \\&= \langle [a \wedge b], [\mathop {\sim }a \wedge \mathop {\sim }b ]\rangle&\text {by (QN4e.1)} \\&= \langle [a] \vee [b], [\mathop {\sim }a ] \wedge [\mathop {\sim }b ] \rangle \\&= \langle [a], [\mathop {\sim }a ] \rangle \vee \langle [b], [\mathop {\sim }b ] \rangle \\&= \iota (a) \vee \iota (b). \end{aligned}$$

Lastly, the implication:

$$\begin{aligned} \iota (a \rightarrow b)&= \langle [a \rightarrow b], [\mathop {\sim }(a \rightarrow b) ]\rangle \\&= \langle [a \rightarrow b], [\mathop {\sim }\mathop {\sim }(a \wedge \mathop {\sim }b) ] \rangle&\text {by (QN4c)} \\&= \langle [a \rightarrow b], [ \mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }\mathop {\sim }\mathop {\sim }b ]) \rangle&\text {by (QN4e.2)} \\&= \langle [a \rightarrow b], [ \mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }b ]) \rangle&\text {by (QN4e.3)} \\&= \langle [a] \rightarrow [b], \Box [ a ] \wedge [\mathop {\sim }b ]) \rangle \\&= \langle [a], [\mathop {\sim }a ] \rangle \rightarrow \langle [b], [\mathop {\sim }b ] \rangle \\&= \iota (a) \rightarrow \iota (b). \end{aligned}$$

\(\square \)

Relying on Theorem 3.3, we will from now on, whenever convenient, identify an arbitrary quasi-N4-lattice with a twist-structure \( \mathbf {A} \le \mathbf {B}^{\bowtie }\). We state the following result as a first consequence of this observation.

Proposition 3.4

Let \(\mathbf {A} = \langle A; \wedge , \vee , \rightarrow , \mathop {\sim }\rangle \) be a quasi-N4-lattice.

  1. (i)

    \(\langle A; \wedge , \vee , \mathop {\sim }\rangle \) is a lower quasi-De Morgan lattice.

  2. (ii)

    \(\langle A; \wedge , \vee , \mathop {\sim }\rangle \) is a De Morgan lattice if and only if \(\mathbf {A} \) is an N4-lattice (cf. Proposition 3.8).

Remark 3.5

Spinks and Veroff (2018, Thm. 2.1) have shown that, in the setting of N4-lattices, the weak implication is term definable using the strong one and the conjunction. This result has some logical import, for it allows one to view Nelson’s paraconsistent logic as a contraction-free relevance logic. Thanks to the twist representation, we can show that the same term does the job in the non-involutive setting of quasi-N4-lattices as well (see Proposition 3.6). Indeed, defining:

$$\begin{aligned} x \Rightarrow _{e} y := (x \wedge (y \Rightarrow y) ) \Rightarrow y \end{aligned}$$

the weak implication can be introduced as follows:

$$\begin{aligned} x \rightarrow y := ( x \wedge ((x \Rightarrow _e y ) \Rightarrow (x \Rightarrow _e y ))) \Rightarrow (x \Rightarrow _e y). \end{aligned}$$

This suggests that quasi-N4-lattices could be axiomatized in the language \(\{\wedge , \vee , *, \Rightarrow , \mathop {\sim }\}\), and we speculate whether such a presentation might be obtained by a suitable adaptation of the axiom system for the relevance logic RW, as in the case of Nelson’s paraconsistent logic (Spinks and Veroff 2018, Thm. 2.1).

Let us also observe that, on a quasi-Nelson algebra \(\mathbf {A} \) (cf. Proposition 3.8), the term \(x \Rightarrow x\) is constant and is interpreted as the top element 1 of the lattice order. Hence, one has, for all \(a,b \in A\), \(a \Rightarrow _{e} b = a \Rightarrow b\) and

$$\begin{aligned} a \rightarrow b= & {} ( a \wedge ((a \Rightarrow _e b ) \Rightarrow (a \Rightarrow _e b ))) \Rightarrow (a \Rightarrow _e b)\\= & {} (a \wedge 1) \Rightarrow (a \Rightarrow b) = a \Rightarrow (a \Rightarrow b), \end{aligned}$$

thus recovering the usual definition of the weak implication from the strong for Nelson algebras, as was to be expected.

Proposition 3.6

Every quasi-N4-lattice satisfies the following identity:

$$\begin{aligned} x \rightarrow y = ( x \wedge ((x \Rightarrow _e y ) \Rightarrow (x \Rightarrow _e y ))) \Rightarrow (x \Rightarrow _e y). \end{aligned}$$

Proof

Letting \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) and \(a= \langle a_1, a_2 \rangle , b= \langle b_1, b_2 \rangle \), let us compute the sub-terms of \( ( a \wedge ((a \Rightarrow _e b ) \Rightarrow (a \Rightarrow _e b ))) \Rightarrow (a \Rightarrow _e b) \). We have:

$$\begin{aligned} a \Rightarrow _e b&=( \langle a_1, a_2 \rangle \wedge \langle 1, \Box b_1 \wedge b_2) \rangle \Rightarrow \langle b_1, b_2 \rangle \\&= \langle a_1, \Box ( a_2 \vee (\Box b_1 \wedge b_2)) \rangle \Rightarrow \langle b_1, b_2 \rangle \\&= \langle (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow \Box ( a_2 \vee (\Box b_1 \wedge b_2)), \Box a_1 \wedge b_2 \rangle \\&= \langle (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow \Box ( a_2 \vee \Box b_1), \Box a_1 \wedge b_2 \rangle \end{aligned}$$

where the last equality holds because:

$$\begin{aligned}&b_2 \rightarrow \Box ( a_2 \vee (\Box b_1 \wedge b_2))\\&\quad = b_2 \rightarrow \Box ( (a_2 \vee \Box b_1) \wedge (a_1 \vee b_2)) \\&\quad = b_2 \rightarrow (\Box (a_2 \vee \Box b_1) \wedge \Box (a_1 \vee b_2)) \\&\quad = (b_2 \rightarrow \Box (a_2 \vee \Box b_1)) \wedge ( b_2 \rightarrow \Box (a_1 \vee b_2)) \\&\quad = (b_2 \rightarrow \Box (a_2 \vee \Box b_1)) \wedge 1 \\&\quad = b_2 \rightarrow \Box (a_2 \vee \Box b_1). \end{aligned}$$

Thus, we have:

$$\begin{aligned}&(a \Rightarrow _e b ) \Rightarrow (a \Rightarrow _e b )\\&\quad = \langle 1, \Box ( (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow \Box ( a_2 \vee \Box b_1)) \wedge \Box a_1 \wedge b_2 \rangle \\&\quad = \langle 1, \Box ( a_1 \wedge b_1 \wedge b_2). \rangle \end{aligned}$$

where the last equality is justified by the following computations:

$$\begin{aligned}&\Box ( (a_1 \rightarrow b_1) \wedge (b_2 \rightarrow \Box ( a_2 \vee \Box b_1)) \wedge \Box a_1 \wedge b_2\\&\quad = \Box (a_1 \wedge (a_1 \rightarrow b_1)) \wedge b_2 \wedge \Box ( a_2 \vee \Box b_1)) \\&\quad = \Box (a_1 \wedge b_1) \wedge b_2 \wedge \Box ( a_2 \vee \Box b_1)) \\&\quad = \Box ( a_1 \wedge b_1 \wedge ( a_2 \vee \Box b_1) ) \wedge \Box b_2 \\&\quad = \Box ( a_1 \wedge b_1 \wedge b_2). \end{aligned}$$

Hence, \(a \wedge (a \Rightarrow _e b ) = \langle a_1, \Box (a_2 \vee \Box ( a_1 \wedge b_1 \wedge b_2)) \rangle \). It is now easy to check that the second component of \(( a \wedge ((a \Rightarrow _e b ) \Rightarrow (a \Rightarrow _e b ))) \Rightarrow (a \Rightarrow _e b)\) is \( \Box a_1 \wedge \Box a_1 \wedge b_2 = \Box a_1 \wedge b_2 \), as required. The first component is

$$\begin{aligned}&(a_1 \rightarrow ((a_1 \rightarrow b_1) \wedge (b_2 \rightarrow \Box ( a_2 \vee \Box b_1)))) \wedge \\&\quad ((\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee \Box ( a_1 \wedge b_1 \wedge b_2))). \end{aligned}$$

The first member of the conjunction can be rewritten as follows:

$$\begin{aligned}&a_1 \rightarrow ((a_1 \rightarrow b_1) \wedge (b_2 \rightarrow \Box ( a_2 \vee \Box b_1)))\\&\quad = (a_1 \!\rightarrow (a_1 \!\rightarrow b_1)) \wedge (a_1\! \rightarrow (b_2 \!\rightarrow \Box ( a_2 \vee \Box b_1))) \\&\quad = (a_1 \rightarrow b_1) \wedge (a_1 \rightarrow (b_2 \rightarrow \Box ( a_2 \vee \Box b_1))) \\&\quad = a_1 \rightarrow ( b_1 \wedge (b_2 \rightarrow \Box ( a_2 \vee \Box b_1))) \\&\quad = a_1 \rightarrow b_1, \end{aligned}$$

the last equality being justified by the following inequalities: \(b_1 \le b_2 \rightarrow (a_2 \vee b_1) \le b_2 \rightarrow \Box ( a_2 \vee \Box b_1)\). As to the second member of the conjunction, observe that

$$\begin{aligned}&\Box (a_2 \vee \Box ( a_1 \wedge b_1 \wedge b_2))\\&\quad = \Box (a_2 \vee (\Box a_1 \wedge \Box b_1 \wedge \Box b_2)) \\&\quad = \Box (a_2 \vee (\Box a_1 \wedge \Box b_1 \wedge \Box b_2)) \\&\quad = \Box (a_2 \vee (\Box a_1 \wedge \Box b_1 \wedge b_2)) \\&\quad = \Box ( (a_2 \vee \Box a_1) \wedge (a_2 \vee \Box b_1) \wedge (a_2 \vee b_2)) \\&\quad = \Box (a_2 \vee \Box a_1) \wedge \Box (a_2 \vee \Box b_1) \wedge \Box (a_2 \vee b_2). \end{aligned}$$

Thus, we have:

$$\begin{aligned}&(\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee \Box ( a_1 \wedge b_1 \wedge b_2)) \\&= (\Box a_1 \wedge b_2 ) \rightarrow (\Box (a_2 \vee \Box a_1) \\&\quad \wedge \Box (a_2 \vee \Box b_1) \wedge \Box (a_2 \vee b_2)) \\&= ((\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee \Box a_1))\\&\wedge ((\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee \Box b_1) )\\&\wedge ((\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee b_2)) \\&= 1 \wedge ((\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee \Box b_1) ) \wedge 1 \\&= (\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee \Box b_1). \end{aligned}$$

To conclude the proof, it therefore suffices to verify the inequality:

$$\begin{aligned} \qquad \quad \qquad a_1 \rightarrow b_1 \le (\Box a_1 \wedge b_2 ) \rightarrow \Box (a_2 \vee \Box b_1) \end{aligned}$$

which is equivalent, by residuation, to the following one:

$$\begin{aligned} \qquad \quad \qquad \Box a_1 \wedge b_2 \wedge (a_1 \rightarrow b_1) \le \Box (a_2 \vee \Box b_1). \end{aligned}$$

In turn, the latter holds because of the following (in)equalities:

$$\begin{aligned} \Box a_1 \wedge b_2 \wedge (a_1 \rightarrow b_1)&\le \Box a_1 \wedge \Box b_2 \wedge \Box (a_1 \rightarrow b_1) \\&= \Box (a_1 \wedge b_2 \wedge (a_1 \rightarrow b_1)) \\&= \Box (a_1 \wedge b_2 \wedge b_1) \\&\le \Box b_1 \\&\le \Box (a_2 \vee \Box b_1). \end{aligned}$$

\(\square \)

In the next proposition we see that the (Odintsov-style) non-equational presentation for QN4-lattices given in Definition 3.2 can be replaced with an equational one, entailing that QN4-lattices form a variety of algebras.

Proposition 3.7

Items (QN4b) and (QN4d) in Definition 3.2 can be equivalently replaced by the following identities:

  1. (i)

    \(|x| \rightarrow y \approx y \).

  2. (ii)

    \((x \wedge y) \rightarrow x \approx |(x \wedge y) \rightarrow x|\).

  3. (iii)

    \((x \wedge y) \rightarrow z \approx x \rightarrow (y \rightarrow z) \).

  4. (iv)

    \((x \Leftrightarrow y) \rightarrow x \approx (x \Leftrightarrow y ) \rightarrow y\).

  5. (v)

    \((x \vee y) \rightarrow z \approx (x \rightarrow z) \wedge (y \rightarrow z) \)

  6. (vi)

    \(x \rightarrow (y \wedge z) \approx (x \rightarrow y) \wedge (x \rightarrow z)\).

  7. (vii)

    \((x \rightarrow y) \wedge (y \rightarrow z) \mathop {\preceq }x \rightarrow z\).

  8. (viii)

    \(x \rightarrow y \mathop {\preceq }x \rightarrow (y \vee z)\).

  9. (ix)

    \(x \rightarrow (y \rightarrow z) \approx (x \rightarrow y) \rightarrow (x \rightarrow z) \).

  10. (x)

    \(x \rightarrow y \mathop {\preceq }\mathop {\sim }\mathop {\sim }x \rightarrow \mathop {\sim }\mathop {\sim }y \).

Hence, the class of quasi-N4-lattices is a variety.

Proof

We have seen in Proposition 2.4 that every quasi-N4-lattice \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) satisfies items (i) to (x).

Conversely, let \(\mathbf {A} = \langle A; \wedge , \vee , \rightarrow , \mathop {\sim }\rangle \) be an algebra satisfying items (i)–(x) above, as well as (QN4a), (QN4c) and (QN4e) from Definition 3.2. Let us check (QN4b).

To show that \(\mathbin \equiv \) is an equivalence relation, it suffices to observe that \(\mathop {\preceq }\) is reflexive and transitive. Reflexivity follows immediately from item (i); to check transitivity, assume \(a \mathop {\preceq }b\) and \(b \mathop {\preceq }c\). Observe that items (iii) and (i) entail that \((|c| \wedge d ) \rightarrow e = d \rightarrow e \) for all \(c,d,e \in A\). Then our assumptions imply \(((a \rightarrow b) \wedge (b \rightarrow c) ) \rightarrow (a \rightarrow c) = (|a \rightarrow b| \wedge |b \rightarrow c| ) \rightarrow (a \rightarrow c) = a \rightarrow c\) which, by (vii), gives us \( a \rightarrow c = |((a \rightarrow b) \wedge (b \rightarrow c) ) \rightarrow (a \rightarrow c)|\). Thus, by (i), we have \( (a \rightarrow c) \rightarrow (a \rightarrow c) = |((a \rightarrow b) \wedge (b \rightarrow c) ) \rightarrow (a \rightarrow c)| \rightarrow (a \rightarrow c) = a \rightarrow c\). Hence, \(a \mathop {\preceq }c\), as claimed.

We proceed in a similar way to check that \(\mathbin \equiv \) is compatible with the lattice operations and the implication.

Assuming \(a \mathop {\preceq }b\) and letting \(c \in A\), we use (iii) to obtain \((a \wedge c) \rightarrow (b \wedge c) = c \rightarrow (a \rightarrow (b \wedge c) = c \rightarrow ((a \rightarrow b ) \wedge (a \rightarrow c)) = (c \rightarrow (a \rightarrow b )) \wedge ( c \rightarrow (a \rightarrow c)) = (c \rightarrow (a \rightarrow b )) \wedge ( (c \wedge a) \rightarrow c)\). Observe that \( (c \wedge a) \rightarrow c = |( c \wedge a) \rightarrow c|\) by item (ii). Likewise, using the assumption \(a \mathop {\preceq }b\) together with items (iii) and (ii), we have \(c \rightarrow (a \rightarrow b ) = c \rightarrow ((a \rightarrow b ) \rightarrow (a \rightarrow b ) ) = ((a \rightarrow b ) \wedge c ) \rightarrow (a \rightarrow b) = |c \rightarrow (a \rightarrow b )|\). Thus, \(((a \wedge c) \rightarrow (b \wedge c) ) \rightarrow ((a \wedge c) \rightarrow (b \wedge c) ) = ((c \rightarrow (a \rightarrow b )) \wedge ( (c \wedge a) \rightarrow c)) \rightarrow ((a \wedge c) \rightarrow (b \wedge c) ) = (|c \rightarrow (a \rightarrow b )| \wedge | (c \wedge a) \rightarrow c|) \rightarrow ((a \wedge c) \rightarrow (b \wedge c) ) = (a \wedge c) \rightarrow (b \wedge c) \). Hence, \(a \wedge c \mathop {\preceq }b \wedge c\). Using this, it is easy to show that \(\mathop {\preceq }\) is compatible with the meet.

A similar reasoning shows that \(a \mathop {\preceq }b\) entails \(a \vee c \mathop {\preceq }b \vee c \). Using (v) and (iii), we have \( (a \vee c) \rightarrow (b \vee c) = (a \rightarrow (b \vee c))) \wedge (c \rightarrow (b \vee c)) \). From the assumption \(a \mathop {\preceq }b\) and item (viii), we have \(a \rightarrow (b \vee c) = |a \rightarrow (b \vee c)|\). Indeed, using also (i), we have \( a \rightarrow (b \vee c) = |a \rightarrow b | \rightarrow (a \rightarrow (b \vee c)) = (a \rightarrow b ) \rightarrow (a \rightarrow (b \vee c)) = |(a \rightarrow b ) \rightarrow (a \rightarrow (b \vee c)) | = ||a \rightarrow b | \rightarrow (a \rightarrow (b \vee c)) | = |a \rightarrow (b \vee c)| \). Observe that \( c \le b \vee c \) entails \(c \rightarrow (b \vee c) = |c \rightarrow (b \vee c)|\). This holds because, using (ii), from \(c = c \wedge (b \vee c)\) we can obtain \(c \rightarrow (b \vee c) = (c \wedge (b \vee c)) \rightarrow (b \vee c) = |(c \wedge (b \vee c)) \rightarrow (b \vee c) | = |c \rightarrow (b \vee c) | \). We then have \( (a \vee c) \rightarrow (b \vee c) = (|a \rightarrow (b \vee c))| \wedge |c \rightarrow (b \vee c)|) \rightarrow ((a \vee c) \rightarrow (b \vee c)) = (a \rightarrow (b \vee c))) \wedge (c \rightarrow (b \vee c)) \rightarrow ((a \vee c) \rightarrow (b \vee c)) = ((a \vee c) \rightarrow (b \vee c)) \rightarrow ((a \vee c) \rightarrow (b \vee c)) \), as required. Using this, it is easy to verify that \(\mathbin \equiv \) is compatible with the join.

To show that \(\mathbin \equiv \) is compatible with the implication, we will check that \(a \mathop {\preceq }b\) entails \(c \rightarrow a \mathop {\preceq }c \rightarrow b \) and \(b \rightarrow c \mathop {\preceq }a \rightarrow c \) for all \(c \in A\). Regarding the former claim, using (ix) we have \((c \rightarrow a) \rightarrow (c \rightarrow b) = c \rightarrow (a \rightarrow b) \). By (i), (iii) and (ii), we have \(c \rightarrow (a \rightarrow b) = |a \rightarrow b| \rightarrow (c \rightarrow (a \rightarrow b)) = (a \rightarrow b) \rightarrow (c \rightarrow (a \rightarrow b)) = ((a \rightarrow b) \wedge c) \rightarrow (a \rightarrow b)) = ( c \wedge (a \rightarrow b)) \rightarrow (a \rightarrow b) = |( c \wedge (a \rightarrow b)) \rightarrow (a \rightarrow b)| = |c \rightarrow (a \rightarrow b)|\). Hence, \(c \rightarrow a \mathop {\preceq }c \rightarrow b \).

To show that \(b \rightarrow c \mathop {\preceq }a \rightarrow c \), observe that \(b \mathop {\preceq }(b \rightarrow c) \rightarrow c \) holds because, by (ii), we have \(b \rightarrow ((b \rightarrow c) \rightarrow c) = (b \rightarrow c) \rightarrow (b \rightarrow c) \). Then, from the assumption \(a \mathop {\preceq }b\) and the transitivity of \(\mathop {\preceq }\), we obtain \( a \mathop {\preceq }(b \rightarrow c) \rightarrow c\). By (iii), we have \(a \rightarrow ((b \rightarrow c) \rightarrow c) = (b \rightarrow c) \rightarrow (a \rightarrow c)\), so the result easily follows.

We proceed to show that the quotient \(\mathbf {A} / {\mathbin \equiv }\) is a Brouwerian algebra. Since \(\langle A, \wedge , \vee \rangle \) is a distributive lattice, so is the corresponding reduct of \(\mathbf {A} / {\mathbin \equiv }\). Thus, it suffices to check the residuation law, i.e., that for all \(a,b,c \in A\), one has \([a] \wedge [b] \le [c]\) if and only if \([a] \le [b] \rightarrow [c]\), where \([a], [b], [c] \in \mathbf {A} / {\mathbin \equiv }\). Assume \([a] \wedge [b] \le [c]\), i.e., \([a \wedge b \wedge c] = [a \wedge b]\). The assumption gives us, in particular \(a \wedge b \mathop {\preceq }a \wedge b \wedge c\). Since \(a \wedge b \wedge c \mathop {\preceq }c \) holds by (ii), by the transitivity of \(\mathop {\preceq }\), we have \(a \wedge b \mathop {\preceq }c\). Thus, \((a \rightarrow b) \rightarrow c = |(a \rightarrow b) \rightarrow c |\). Since \((a \rightarrow b) \rightarrow c = a \rightarrow (b \rightarrow c)\) holds by (iii), it follows that \(a \rightarrow (b \rightarrow c) = |a \rightarrow (b \rightarrow c)|\), i.e., \(a \mathop {\preceq }b \rightarrow c\). Since \(a \mathop {\preceq }a\), using the compatibility of \(\mathop {\preceq }\) with the meet, we conclude \(a \wedge a = a \mathop {\preceq }a \wedge (b \rightarrow c) \). Since \(a \wedge (b \rightarrow c) \mathop {\preceq }a\) holds by (ii), we obtain \([a \wedge (b \rightarrow c)] = [a]\), as required. Conversely, assume \([a \wedge (b \rightarrow c)] = [a]\). Since \(a \wedge b \wedge c \mathop {\preceq }a \wedge b\) holds by (ii), it suffices to show that \(a \wedge b \mathop {\preceq }a \wedge b \wedge c\). In fact, showing \(a \wedge b \mathop {\preceq }c\) is enough, for we can use \(a \wedge b \mathop {\preceq }a \wedge b\) and the compatibility of \(\mathop {\preceq }\) with the meet to obtain \(a \wedge b \wedge a \wedge b = a \wedge b \mathop {\preceq }a \wedge b \wedge c\). From the assumption \([a \wedge (b \rightarrow c)] = [a]\) and (iii), we have \(a \mathop {\preceq }a \wedge (b \rightarrow c) \mathop {\preceq }b \rightarrow c\). Hence, \(a \mathop {\preceq }b \rightarrow c\). Using (iii), we have \( |a \rightarrow (b \rightarrow c) | = a \rightarrow (b \rightarrow c) = (a \wedge b) \rightarrow c\). Hence, the required result easily follows.

Let us check that \( \Box [a ] : = [\mathop {\sim }\mathop {\sim }a ] \) is a nucleus operator. To begin with, notice that \(\Box \) is well defined on \(\mathbf {A} / {\mathbin \equiv }\) because \(a \mathbin \equiv b \) entails \(\mathop {\sim }\mathop {\sim }a \mathbin \equiv \mathop {\sim }\mathop {\sim }b \) by (x). Further, by (QN4e.2), we have \(\Box ([a] \wedge [b]) = \Box [a \wedge b] = [\mathop {\sim }\mathop {\sim }(a \wedge b) ] = [\mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }\mathop {\sim }b]= [\mathop {\sim }\mathop {\sim }a] \wedge [\mathop {\sim }\mathop {\sim }b] = \Box [a] \wedge \Box [b]\). Thus, \(\Box \) preserves finite meets. By (QN4e.4), we have \([a] \wedge \Box [a ] = [a] \wedge [\mathop {\sim }\mathop {\sim }a ] = [a \wedge \mathop {\sim }\mathop {\sim }a ] = [a]\), so \([a] \le \Box [a]\). Lastly by (QN4e.3) we have \(\Box \Box [a ] = [\mathop {\sim }\mathop {\sim }\mathop {\sim }\mathop {\sim }a ] = [\mathop {\sim }\mathop {\sim }a] = \Box [a]\).

To show that (QN4d) is satisfied, assume \(a \le b\). Then \(a = a \wedge b\), so (ii) gives us \(a \rightarrow b = (a \wedge b) \rightarrow b = |(a \wedge b) \rightarrow b|\). Then, by (i), we have \((a \rightarrow b) \rightarrow (a \rightarrow b) = |a \rightarrow b | = |(a \wedge b) \rightarrow b| \rightarrow (a \rightarrow b) = a \rightarrow b\). Hence, \(a \mathop {\preceq }b\). Observe that, by (QN4e.1), \(a \vee b = b \) entails \(\mathop {\sim }(a \vee b) = \mathop {\sim }a \wedge \mathop {\sim }b = \mathop {\sim }b \), i.e., \(\mathop {\sim }b \le \mathop {\sim }a\). Then we can apply the preceding reasoning to obtain \(\mathop {\sim }b \mathop {\preceq }\mathop {\sim }a \). Conversely, assume \(a \mathop {\preceq }b\) and \(\mathop {\sim }b \mathop {\preceq }\mathop {\sim }a \). Recall that \((|c| \wedge d ) \rightarrow e = d \rightarrow e \) for all \(c,d,e \in A\). This holds because, by (iii) and (i), we have \((|c| \wedge d ) \rightarrow e = |c| \rightarrow (d \rightarrow e) = d \rightarrow e\). Now, we can instantiate (iv) as follows: \(((a \vee b) \Leftrightarrow b) \rightarrow (a \vee b) = ((a \vee b) \Leftrightarrow b ) \rightarrow b\). Using (QN4e.1) followed by items (v) and (vi), we have \( (a \vee b) \Leftrightarrow b = ((a \vee b) \rightarrow b) \wedge (\mathop {\sim }b \rightarrow \mathop {\sim }(a \vee b)) \wedge (b \rightarrow (a \vee b)) \wedge (\mathop {\sim }(a \vee b) \rightarrow \mathop {\sim }a) = ((a \vee b) \rightarrow b) \wedge (\mathop {\sim }b \rightarrow (\mathop {\sim }a \wedge \mathop {\sim }b)) \wedge (b \rightarrow (a \vee b)) \wedge ( (\mathop {\sim }a \wedge \mathop {\sim }b) \rightarrow \mathop {\sim }a) = (a \rightarrow b) \wedge (b \rightarrow b) \wedge (\mathop {\sim }b \rightarrow \mathop {\sim }a) \wedge (\mathop {\sim }b \rightarrow \mathop {\sim }b) \wedge (b \rightarrow (a \vee b)) \wedge ( (\mathop {\sim }a \wedge \mathop {\sim }b) \rightarrow \mathop {\sim }a)\). We have \(a \rightarrow b = |a \rightarrow b |\) and \(\mathop {\sim }b \rightarrow \mathop {\sim }a = |\mathop {\sim }b \rightarrow \mathop {\sim }a|\) by assumption; moreover, (i) entails \(b \rightarrow b = |b \rightarrow b |\) and, likewise \(\mathop {\sim }b \rightarrow \mathop {\sim }b = | \mathop {\sim }b \rightarrow \mathop {\sim }b |\). We have just shown that \(b \le a \vee b\) entails \(b \mathop {\preceq }a \vee b\). Lastly, (ii) entails \((\mathop {\sim }a \wedge \mathop {\sim }b) \rightarrow \mathop {\sim }a = |(\mathop {\sim }a \wedge \mathop {\sim }b) \rightarrow \mathop {\sim }a|\). Joining these observations, we have \(((a \vee b) \Leftrightarrow b) \rightarrow (a \vee b) = (|a \rightarrow b| \wedge |b \rightarrow b| \wedge |\mathop {\sim }b \rightarrow \mathop {\sim }a| \wedge |\mathop {\sim }b \rightarrow \mathop {\sim }b| \wedge |b \rightarrow (a \vee b)| \wedge | (\mathop {\sim }a \wedge \mathop {\sim }b) \rightarrow \mathop {\sim }a|) \rightarrow (a \vee b) = a \vee b = ((a \vee b) \Leftrightarrow b ) \rightarrow b = b\). Hence, \(a \le b\). \(\square \)

It is well known that the lattice reduct of a N4-lattice may be unbounded or bounded (in which case both bounds exist). We see in the next proposition that the situation is different in the non-involutive case. When the bounds exist, we shall denote by (resp.) 0 and 1 the bottom and top element of the lattice reduct of a quasi-N4-lattice.

Proposition 3.8

Let \(\mathbf {A} \) be a quasi-N4-lattice.

  1. (i)

    \(\mathbf {A} \) is a quasi-Nelson algebra iff \(\mathbf {A} \vDash x \wedge \mathop {\sim }x \mathop {\preceq }y \) iff \(\mathbf {A} \vDash \mathop {\sim }|x| \approx 0\).

  2. (ii)

    \(\mathbf {A} \vDash |x| \approx |y| \) iff \(\mathbf {A} \vDash |x | \approx 1\).

  3. (iii)

    \(\mathbf {A} \) is an N4-lattice iff \(\mathbf {A} \vDash \mathop {\sim }\mathop {\sim }x \le x\).

Proof

(i). Using the twist representation established in Rivieccio and Spinks (2019), it is easy to check that every quasi-Nelson algebra as introduced in Rivieccio and Spinks (2019), Def. 4.1 satisfies both \( x \wedge \mathop {\sim }x \mathop {\preceq }y \) and \(\mathop {\sim }|x| \approx 0\). To show that a quasi-N4-lattice \(\mathbf {A} \) satisfying \( x \wedge \mathop {\sim }x \mathop {\preceq }y\) is a quasi-Nelson algebra according to (Rivieccio and Spinks 2019, Def. 4.1), it suffices to verify that the lattice reduct of \(\mathbf {A} \) is bounded. Assuming \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) and letting \(a= \langle a_1, a_2 \rangle , b= \langle b_1, b_2 \rangle \in A\), let us compute \( \langle a_1, a_2 \rangle \wedge \mathop {\sim }\langle a_1, a_2 \rangle = \langle a_1 \wedge a_2 , \Box (\Box a_1 \vee a_2 ) \rangle = \langle a_1 \wedge a_2 , \Box ( a_1 \vee a_2 ) \rangle \). The last equality holds because \(\Box a_2 = a_2 \) and, as observed earlier, \(\mathbf {B}\) satisfies \(\Box (x \vee y) \approx \Box (\Box x \vee \Box y)\). We then have \( \langle a_1, a_2 \rangle \wedge \mathop {\sim }\langle a_1, a_2 \rangle = \langle a_1 \wedge a_2 , \Box ( a_1 \vee a_2 ) \rangle \mathop {\preceq }\langle b_1 \wedge b_2 , \Box ( b_1 \vee b_2 ) \rangle = \langle b_1, b_2 \rangle \wedge \mathop {\sim }\langle b_1, b_2 \rangle \) for all \( \langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle \in A\). Hence, \(a_1 \wedge a_2 \le b_1 \wedge b_2\) (so, by symmetry, \(a_1 \wedge a_2 = b_1 \wedge b_2\)). We claim that \(a_1 \wedge a_2\) is the bottom element of the lattice order of \(\mathbf {B}\). To see this, let \(c_1 \in B\) be an arbitrary element of B. By the requirement \(\pi _1[A] = B\), there is \(c_2 \in B\) such that \(\langle c_1, c_2 \rangle \in A\). We then have \(a_1 \wedge a_2 = c_1 \wedge c_2 \le c_1\). That is, \(a_1 \wedge a_2\) is the bottom element of the lattice order of \(\mathbf {B}\). Thus, letting \(a_1 \wedge a_2 : = 0\), we have, for all \( \langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle \in A\), that \(| \langle a_1, a_2 \rangle | = \langle 1 , 0 \rangle = |\langle b_1, b_2 \rangle |\). Thus, \(\langle 1 , 0 \rangle \) is the top element of the lattice order of \(\mathbf {A} \), and \(\mathop {\sim }\langle 1, 0 \rangle = \langle 0, \Box 1 \rangle = \langle 0, 1 \rangle \) is the bottom element, as required. To conclude the proof, assuming \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) as before, suppose \(\mathbf {A} \vDash \mathop {\sim }|x| \approx 0\). Then, for every element \(\langle a_1, a_2 \rangle \in A\), we have \(\mathop {\sim }|\langle a_1, a_2 \rangle | = \langle \Box a_1 \wedge a_2, \Box 1 \rangle = \langle \Box a_1 \wedge a_2, 1 \rangle = \langle 0, 1 \rangle \), that is, \(\Box a_1 \wedge a_2 = 0\). The latter entails \( a_1 \wedge a_2 = 0\) because \(a_1 \wedge a_2 \le \Box a_1 \wedge a_2 \). This immediately implies \( \mathbf {A} \vDash x \wedge \mathop {\sim }x \mathop {\preceq }y\), which as we have seen is equivalent to \(\mathbf {A} \) being a quasi-Nelson algebra.

(ii). The leftward implication is clear. As to the rightward one, given arbitrary elements \(\langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle \in A\), assume \(|\langle a_1, a_2 \rangle | = \langle 1, \Box a_1 \wedge a_2 \rangle = \langle 1, \Box b_1 \wedge b_2 \rangle = |\langle b_1, b_2 \rangle | \). We may thus let \(c_2 : = \Box a_1 \wedge a_2\). Since every quasi-N4-lattice satisfies \(\langle a_1, a_2 \rangle \le |\langle a_1, a_2 \rangle | = \langle 1, c_2 \rangle \), this entails that \(|\langle 1, c_2 \rangle | \) is the top element of the lattice order of \(\mathbf {A} \). Observe that \(c_2\) need not be the minimum on \(\mathbf {B}\), but it is the minimum of those elements of B that are fixed under the \(\Box \) operation. Indeed, observe that \(c_2 = \Box c_2 \) and that, for all \(\langle d_1, d_2 \rangle \in A\), from \(\langle d_1, d_2 \rangle \le \langle 1, c_2 \rangle \) we have \(c_2 \le d_2\).

(iii). The rightward implication is clear. As to the leftward one, assume \(\mathbf {A} \vDash \mathop {\sim }\mathop {\sim }x \le x\) and let \(a_1 \in B\). Then there is \(a_2 \in B\) such that \(\langle a_1, a_2 \rangle \in A\), and \(\mathop {\sim }\mathop {\sim }\langle a_1 , a_2 \rangle = \langle \Box a_1, a_2 \rangle \le \langle a_1, a_2 \rangle \). This means that \(\mathbf {B}\) satisfies \(\Box x \le x \) (and, hence, \(\Box x \approx x\)). Thus, \(\Box \) is the identity map on B, which entails that Definition 2.2 reduces to Odintsov’s definition of twist-structures for N4-lattices. \(\square \)

Proposition 3.8 entails that a quasi-N4-lattice is a Nelson algebra if and only if both items (i) and (iii) hold. Also observe that (i) implies (ii). In fact, a quasi-N4-lattice \(\mathbf {A} \) may have a top element without necessarily having a bottom element, but not the other way round: if 0 is the bottom element, then \(\mathop {\sim }0\) is necessarily the top element. Indeed, since the negation is order-reversing, from \(0 \le \mathop {\sim }a \) and \(a \le \mathop {\sim }\mathop {\sim }a\) we have \(a \le \mathop {\sim }\mathop {\sim }a \le \mathop {\sim }0\), for all \(a \in A\). Thus, \(\mathop {\sim }0 = 1\).

Let \({{\mathsf {Q}}}{{\mathsf {N}}}\), \({{\mathsf {N}}}{{\mathsf {4}}}\), and \(\mathsf {QN4}\) denote the varieties of quasi-Nelson algebras, N4-lattices and QN4-lattices, respectively. Let us also denote by \({\mathbb {V}}({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}})\) the variety generated by \({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}\). Having observed that \({\mathbb {V}}({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}) \subseteq \mathsf {QN4}\), one may wonder whether this inclusion is strict. This is indeed the case. In fact, it is easy to verify that the following identity

$$\begin{aligned}&((x \wedge \mathop {\sim }x) \rightarrow y ) \vee (\mathop {\sim }\mathop {\sim }z \rightarrow z ) \nonumber \\&\quad \approx |((x \wedge \mathop {\sim }x) \rightarrow y ) \vee (\mathop {\sim }\mathop {\sim }z \rightarrow z )| \end{aligned}$$
(1)

is verified by all members of \({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}\). However, in the algebra \(\mathbf {A} _4\) depicted in Fig. 1, we have, for instance:

$$\begin{aligned}&((\langle a,1 \rangle \wedge \mathop {\sim }\langle a,1 \rangle ) \rightarrow \langle 0 ,1 \rangle ) \vee (\mathop {\sim }\mathop {\sim }\langle a,1 \rangle \rightarrow \langle a,1 \rangle ) \\&\quad = \langle a, 1 \rangle \ne \langle 1, 1 \rangle = |\langle a, 1 \rangle |. \end{aligned}$$

Hence, \(\mathbf {A} _4 \notin {\mathbb {V}}({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}) \). Later we are going to see (Theorem 4.7) that adding the identity (1) to \(\mathsf {QN4}\) is indeed enough to axiomatize \({\mathbb {V}}({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}) \).

4 Congruence properties

4.1 Filters and congruences

In this subsection we introduce a notion of filter for QN4-lattices that will allow us to establish an isomorphism between the lattice of filters on an arbitrary QN4-lattice \(\mathbf {A} \) and the lattice of congruences on \(\mathbf {A} \) (Theorem 4.4). We are also going to show that the lattice of congruences on each QN4-lattice \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) is isomorphic to the lattice of congruences on the (nuclear) Brouwerian algebra \(\mathbf {B}\) (Corollary 4.6)

Recall that a filter of a Brouwerian algebra \(\mathbf {B}\) is a set \(F \subseteq B\) that is non-empty, increasing and closed under finite meets. An equivalent definition is to require F to be non-empty and closed under modus ponens, meaning that \(a, a \rightarrow b \in F\) entail \(b \in F\) for all \(a,b \in B\). The (po)set of all filters of a Brouwerian algebra \(\mathbf {B}\) will be denoted by \(Fi(\mathbf {B})\).

Given a quasi-N4-lattice \(\mathbf {A} \) and \(F \subseteq A\), we shall say that F is an (implicative) filter if (i) \(|a| \in F\) for all \(a \in A\), and (ii) F is closed under modus ponens (\(\rightarrow \)-mp): if \(a, a \rightarrow b \in A\), then \(b \in F\), for all \(a,b \in A\). Observe that every implicative filter F satisfies the following property: If \(a \in F\) and \(a \mathop {\preceq }b\), then (\(a \rightarrow b \in F\), hence) \(b \in F\). The (po)set of all filters of a quasi-N4-lattice \(\mathbf {A} \) will be denoted by \(Fi(\mathbf {A})\).

Every implicative filter F of a quasi-N4-lattice \(\mathbf {A} = \langle A; \wedge , \vee , \rightarrow , \mathop {\sim }\rangle \) is a lattice filter of the lattice reduct \( \langle A; \wedge , \vee \rangle \), while the converse need not hold in general. Let us check this on a twist-structure \( \mathbf {A} \le \mathbf {B}^{\bowtie }\). Assume \(\langle a_1, a_2 \rangle \in F\) and \(\langle a_1, a_2 \rangle \le \langle b_1, b_2 \rangle \) for some \(\langle b_1, b_2 \rangle \in A\). Then \(a_1 \le b_1\), which entails \(\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle = \langle 1, \Box a_1 \wedge b_2 \rangle \). Observe that \(|\langle 1, \Box a_1 \wedge b_2 \rangle | = \langle 1, \Box 1 \wedge \Box a_1 \wedge b_2 \rangle = \langle 1, \Box a_1 \wedge b_2 \rangle \in F\). Thus, by (\(\rightarrow \)-mp), we have \(\langle b_1, b_2 \rangle \in F\), as required. Now assume \(\langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle \in F\). Observe that \(\langle a_1, a_2 \rangle \rightarrow ( \langle b_1, b_2 \rangle \rightarrow (\langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle )) = \langle a_1 \rightarrow (b_1 \rightarrow (a_1 \wedge b_1)), \Box a_1 \wedge \Box b_1 \wedge \Box (a_2 \vee b_2) \rangle = \langle 1, \Box a_1 \wedge \Box b_1 \wedge \Box (a_2 \vee b_2) \rangle \in F\). Then we can apply (\(\rightarrow \)-mp) to obtain \(\langle a_1, a_2 \rangle \wedge \langle b_1, b_2 \rangle \in F\), as required. (To see that a lattice filter need not be an implicative filter, observe that the singleton filter \(\{\langle 1,0 \rangle \}\) on any of the algebras depicted in Fig. 1 does not satisfy the first requirement for being an implicative filter, because \(|\langle 1, 1 \rangle | = \langle 1, 1 \rangle \notin \{\langle 1,0 \rangle \}\)).

Proposition 4.1

Let \( \mathbf {A} \le \mathbf {B}^{\bowtie }\), \(F_1 \subseteq B\) and \(F \subseteq A\).

  1. (i)

    If \(F_1 \in Fi(\mathbf {B})\), then \((F_1 \times B) \cap A \in Fi(\mathbf {A} )\).

  2. (ii)

    If \(F \in Fi(\mathbf {A} )\), then \(F = (\pi _1[F] \times B) \cap A\), where \(\pi _1[F] \in Fi(\mathbf {B})\).

Proof

(i). Let \(F : = (F_1 \times B) \cap A\). Recall that, for all \(\langle a_1, a_2 \rangle \in A\), we have \(| \langle a_1, a_2 \rangle | = \langle 1, \Box a_1 \wedge a_2 \rangle \). Since \(1 \in F_1\), we have \(\langle 1, b_2 \rangle \in F_1 \times B\) for every \(b_2 \in B\). Thus, for all \(\langle a_1, a_2 \rangle \in A\), we have \(| \langle a_1, a_2 \rangle | \in F\). Now assume \(\langle a_1, a_2 \rangle , \langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle \in (F_1 \times B) \cap A\). We have \(a_1, a_1 \rightarrow b_1 \in F_1\). Since \(F_1\) is an implicative filter, we have \(b_1 \in F_1\). Hence, \(\langle b_1, b_2 \rangle \in F_1 \times B\), giving us the desired result.

(ii). It is clear that \(F \subseteq (\pi _1[F] \times A_2) \cap A\). For the converse inclusion, assume \(\langle a_1, a_2 \rangle \in A\) is such that \(\langle a_1, a_2 \rangle \in \pi _1[F] \times A\). Then there is \(b_2 \in A\) with \(\langle a_1, b_2 \rangle \in F\). Since \(\langle a_1, b_2 \rangle \rightarrow \langle a_1, a_2 \rangle = \langle 1, \Box a_1 \wedge a_2 \rangle = | \langle a_1, a_2 \rangle | \in F\), by (\(\rightarrow \)-mp) we have \(\langle a_1, a_2 \rangle \in F\), as required. Next, let us check that \(\pi _1[F]\) is a filter. It is clear that \(\pi _1[F]\) is non-empty. Now suppose \(a_1, a_1 \rightarrow _1 b_1 \in \pi _1[F]\). Then there is an element \(a_2 \in A\) such that \(\langle a_1, a_2 \rangle \in F\). Also, by the requirement \(\pi _1[A] = A\), the assumption \(b_1 \in A\) entails that there is an element \(b_2 \in A\) with \(\langle b_1, b_2 \rangle \in A\). Observe that \( \langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle = \langle a_1 \rightarrow b_1, \Box a_1 \wedge b_2 \rangle \in (\pi _1[F] \times A) \cap A = F\). Then we can use (\(\rightarrow \)-mp) to conclude \(\langle b_1, b_2 \rangle \in F\), and so \(b_1 \in \pi _1[F]\). Thus, \(\pi _1[F]\) is an implicative filter (hence, a lattice filter) of \(\mathbf {B}\). \(\square \)

Theorem 4.2

For every QN4-lattice \( \mathbf {A} \le \mathbf {B}^{\bowtie }\), the first-coordinate projection map \(\pi _1 \) is a complete lattice isomorphism between \(Fi(\mathbf {A} )\) and \(Fi(\mathbf {B})\).

Proof

It is clear that the map \(\pi _1\) is order-preserving. To show that it is also order-reflecting, assume \(\pi _1[F] \subseteq \pi _1 [G]\) for some \(F, G \in Fi(\mathbf {A} )\). Then, using Proposition 4.1.ii, we have \(F = (\pi _1[F] \times A_-) \cap A \subseteq (\pi _1[G] \times A_-) \cap A = G \). Hence, \(F =G\). Thus, \(\pi _1\) is an order embedding. Moreover, \(\pi _1\) is surjective. Indeed, let \(F_1 \in Fi(\mathbf {B})\). Then, by Proposition 4.1.i, we have \(F := (F_1 \times A) \cap A \in Fi(\mathbf {A} )\), and \(F_1 = \pi _1 [F]\). \(\square \)

It is easy to verify that the isomorphism mentioned in Theorem 4.2 preserves the property of being a prime filter (defined in the usual way); also observe that the theorem implies that each QN4-lattice \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) has a least implicative filter \(F_0 = (\{1 \} \times B) \cap A \), which can also be described as \(F_0 = \{|a | : a \in A \}\).

Given a QN4-lattice \(\mathbf {A} \) and a congruence \(\theta \in \mathrm {Con}(\mathbf {A} ) \), we define \( F_{\theta } : = \{ a \in A : \langle a, |a| \rangle \in \theta \} \). Conversely, for each \(F \in Fi(\mathbf {A} )\), we let \( \theta _{F} : = \{ \langle a, b \rangle \in A \times A : a \rightarrow b, b \rightarrow a, \mathop {\sim }a \rightarrow \mathop {\sim }b , \mathop {\sim }b \rightarrow \mathop {\sim }a \in F \} \).

Lemma 4.3

Let \(\mathbf {A} \) be a quasi-N4-lattice, let \(\theta \in \mathrm {Con}(\mathbf {A} ) \), \(F \in Fi(\mathbf {A} )\), and \(a,b \in A\). Then,

  1. (i)

    If \(\langle a, |b| \rangle \in \theta \), then \(\langle a, |a | \rangle \in \theta \).

  2. (ii)

    \(F_{\theta } \in Fi(\mathbf {A} )\).

  3. (iii)

    \(\theta _{F} \in \mathrm {Con}(\mathbf {A} ) \).

  4. (iv)

    \( F_{\theta _{F}} = F\).

  5. (v)

    \(\theta _{F_{\theta }} = \theta \).

Proof

(i). Let us assume \( \mathbf {A} \le \mathbf {B}^{\bowtie }\). Then \(\langle a, |b| \rangle \in \theta \) and Proposition 2.4.i entail \(\langle a \rightarrow a , |b| \rightarrow a \rangle = \langle a \rightarrow a , a \rangle = \langle |a|, a \rangle \in \theta \).

(ii). For all \(a \in A\), we have \(|a| = ||a ||\), so (by reflexivity of \(\theta \)) we obtain \(|a | \in F_{\theta }\). To show that \(F_{\theta }\) is closed under (\(\rightarrow \)-mp), assume \(a, a \rightarrow b \in F_{\theta }\), i.e., \(\langle a, |a| \rangle , \langle a \rightarrow b, |a \rightarrow b | \rangle \in \theta \). Then \(\langle a \wedge (a \rightarrow b), |a| \wedge |a \rightarrow b | \rangle \in \theta \). It is easy to check (on a twist-structure) that \( ||a| \wedge |a \rightarrow b || = |a| \wedge |a \rightarrow b | \). Then, by item (i) above, we have \(\langle a \wedge (a \rightarrow b), |a \wedge (a \rightarrow b)| \rangle \in \theta \), so \(\langle (a \wedge (a \rightarrow b)) \rightarrow b, |a \wedge (a \rightarrow b)| \rightarrow b \rangle = \langle (a \wedge (a \rightarrow b)) \rightarrow b, b \rangle \in \theta \). Letting \(a = \langle a_1, a_2 \rangle , b = \langle b_1, b_2 \rangle \), let us compute \( (a \wedge (a \rightarrow b)) \rightarrow b = (\langle a_1, a_2 \rangle \wedge (\langle a_1, a_2 \rangle \rightarrow \langle b_1, b_2 \rangle )) \rightarrow \langle b_1, b_2 \rangle = \langle (a_1 \wedge (a_1 \rightarrow b_1)) \rightarrow b_1, \Box (a_1 \wedge (a_1 \rightarrow b_1)) \wedge b_2 \rangle = \langle (a_1 \wedge b_1) \rightarrow b_1, \Box (a_1 \wedge b_1) \wedge b_2 \rangle = \langle 1, \Box a_1 \wedge \Box b_1 \wedge b_2 \rangle \). Thus, \(|(a \wedge (a \rightarrow b)) \rightarrow b | = (a \wedge (a \rightarrow b)) \rightarrow b \). Thus, by item (i) above, from \( \langle (a \wedge (a \rightarrow b)) \rightarrow b, b \rangle = \langle |(a \wedge (a \rightarrow b)) \rightarrow b |, b \rangle \in \theta \) we obtain \(\langle b, |b | \in \theta \). Hence, \(b \in F_{\theta }\), as required.

(iii). Let us assume \( \mathbf {A} \le \mathbf {B}^{\bowtie }\). Let \(\langle a,b \rangle \in \theta _{F}\), that is, \(a \rightarrow b, b \rightarrow a, \mathop {\sim }a \rightarrow \mathop {\sim }b , \mathop {\sim }b \rightarrow \mathop {\sim }a \in F\). Observe that \(a \rightarrow b \mathop {\preceq }\mathop {\sim }\mathop {\sim }a \rightarrow \mathop {\sim }\mathop {\sim }b\). Indeed, letting \(a = \langle a_1, a_2 \rangle , b = \langle b_1, b_2 \rangle \), we have \( \mathop {\sim }\mathop {\sim }\langle a_1, a_2 \rangle \rightarrow \mathop {\sim }\mathop {\sim }\langle b_1, b_2 \rangle = \langle \Box a_1 \rightarrow \Box b_1, \Box a_1 \wedge b_2 \rangle \). The result then follows because \(a_1 \rightarrow b_1 \le \Box (a_1 \rightarrow b_1) \le \Box a_1 \rightarrow \Box b_1\). Then from \(a \rightarrow b, b \rightarrow a \in F\) we obtain \(\mathop {\sim }\mathop {\sim }a \rightarrow \mathop {\sim }\mathop {\sim }b, \mathop {\sim }\mathop {\sim }b \rightarrow \mathop {\sim }\mathop {\sim }a \in F\). Hence, \(\langle \mathop {\sim }a, \mathop {\sim }b \rangle \in \theta _{F}\).

To check that \( \theta _{F}\) is compatible with the lattice operations, it is sufficient to verify that \(\langle a \wedge c, b \wedge c \rangle , \langle a \vee c, b \vee c \rangle \in \theta _{F}\) for all \(c \in A\). Using items (ii) and (iii) of Proposition 2.4, we have \((a \wedge c ) \rightarrow (b \wedge c) = ((a \wedge c) \rightarrow b) \wedge ((a \wedge c) \rightarrow c) = ((c \wedge a) \rightarrow b) \wedge ((a \wedge c) \rightarrow c) = (c \rightarrow (a \rightarrow b)) \wedge ((a \wedge c) \rightarrow c) \). It is easy to check that \((a \wedge c) \rightarrow c = |(a \wedge c) \rightarrow c|\), hence \((a \wedge c) \rightarrow c \in F\). Since \(a \rightarrow b \mathop {\preceq }c \rightarrow (a \rightarrow b)\), the assumption \(a \rightarrow b \in F\) gives us \( c \rightarrow (a \rightarrow b) \in F\). Since F is closed under finite meets, we obtain \((c \rightarrow (a \rightarrow b)) \wedge ((a \wedge c) \rightarrow c) = (a \wedge c ) \rightarrow (b \wedge c) \in F \), as required. A similar reasoning shows that \((b \wedge c ) \rightarrow (a \wedge c) \in F\). To show that \(\mathop {\sim }(a \wedge c ) \rightarrow \mathop {\sim }(b \wedge c) \in F\), it is sufficient to observe that \(\mathop {\sim }a \rightarrow \mathop {\sim }b \mathop {\preceq }\mathop {\sim }(a \wedge c ) \rightarrow \mathop {\sim }(b \wedge c) \). To see that the latter holds, letting \(a = \langle a_1, a_2 \rangle , b = \langle b_1, b_2 \rangle , c = \langle c_1, c_2 \rangle \), we compute \(\mathop {\sim }\langle a_1, a_2 \rangle \rightarrow \mathop {\sim }\langle b_1, b_2 \rangle = \langle a_2 \rightarrow b_2, a_2 \wedge \Box b_1 \rangle \) and \(\mathop {\sim }(\langle a_1, a_2 \rangle \wedge \langle c_1, c_2 \rangle ) \rightarrow \mathop {\sim }(\langle b_1, b_2 \rangle \wedge \langle c_1, c_2 \rangle ) = \langle \Box (a_2 \vee c_2) \rightarrow \Box (b_2 \vee c_2) , \Box (a_2 \vee c_2) \wedge \Box ( b_1 \wedge c_1) \rangle \). It suffices to check that \(a_2 \rightarrow b_2 \le \Box (a_2 \vee c_2) \rightarrow \Box (b_2 \vee c_2)\), which does hold because, using the properties of the implication of Brouwerian algebras, we have \(a_2 \rightarrow b_2 \le (a_2 \rightarrow (b_2 \vee c_2)) \wedge 1 = (a_2 \rightarrow (b_2 \vee c_2)) \wedge (c_2 \rightarrow (b_2 \vee c_2)) = (a_2 \vee c_2 ) \rightarrow (b_2 \vee c_2) \le \Box ((a_2 \vee c_2 ) \rightarrow (b_2 \vee c_2) ) \le \Box (a_2 \vee c_2 ) \rightarrow \Box (b_2 \vee c_2) \). A similar reasoning allows us to conclude that \(\mathop {\sim }(b \wedge c ) \rightarrow \mathop {\sim }(a \wedge c) \in F\).

We proceed to check that \( \langle a \vee c, b \vee c \rangle \in \theta _{F}\). To show that \( (a \vee c ) \rightarrow (b \vee c) \in F\), recall that \( (a \vee c ) \rightarrow (b \vee c) = (a \rightarrow (b \vee c)) \wedge (c \rightarrow (b \vee c))\) holds by item (iv) of Proposition 2.4. From \(a \rightarrow b \in F\) and \(a \rightarrow b \mathop {\preceq }a \rightarrow (b \vee c)\), we conclude \(a \rightarrow (b \vee c) \in F\). That \(c \rightarrow (b \vee c)\) follows from the observation that \(c \rightarrow (b \vee c) = |c \rightarrow (b \vee c)|\). Then the desired result follows because F is closed under finite meets. A similar reasoning establishes \( (b \vee c ) \rightarrow (a \vee c) \in F\). To show \( \mathop {\sim }(a \vee c ) \rightarrow \mathop {\sim }(b \vee c) \in F\), it suffices to observe that \( \mathop {\sim }(a \vee c ) \rightarrow \mathop {\sim }(b \vee c) = (\mathop {\sim }a \wedge \mathop {\sim }c) \rightarrow (\mathop {\sim }b \wedge \mathop {\sim }c)\) holds by (QN4e.1) in Definition 3.2. Then the result follows from the above proof that \(\theta _{F}\) is compatible with the meet, and similarly we obtain \( \mathop {\sim }(b \vee c ) \rightarrow \mathop {\sim }(a \vee c) \in F\).

Lastly, let us check that \( \theta _{F}\) is compatible with the implication. We do this in two steps, showing that \( \langle a, b \rangle \in \theta _{F}\) entails \( \langle a \rightarrow c, b \rightarrow c \rangle \in \theta _{F}\) and \( \langle c \rightarrow a, c \rightarrow b \rangle \in \theta _{F}\) for all \(c \in A\). To see that \((a \rightarrow c) \rightarrow (b \rightarrow c) \in F\), observe that \((b \rightarrow a ) \wedge (a \rightarrow c) \mathop {\preceq }b \rightarrow c\) holds by item (vi) of Proposition 2.4. Using also item (ii) of Proposition 2.4, we thus have \(((b \rightarrow a ) \wedge (a \rightarrow c) ) \rightarrow (b \rightarrow c) = (b \rightarrow a ) \rightarrow ( (a \rightarrow c) ) \rightarrow (b \rightarrow c)) = | (b \rightarrow a ) \rightarrow ( (a \rightarrow c) ) \rightarrow (b \rightarrow c)) | \). Hence, \(b \rightarrow a \mathop {\preceq }(a \rightarrow c) ) \rightarrow (b \rightarrow c)\). Thus, from \(b \rightarrow a \in F\) we obtain \((a \rightarrow c) ) \rightarrow (b \rightarrow c) \in F\), as required. A similar reasoning shows that \(a \rightarrow b \in F\) entails \((b \rightarrow c) ) \rightarrow (a \rightarrow c) \in F\). To see that \(\mathop {\sim }(a \rightarrow c) \rightarrow \mathop {\sim }(b \rightarrow c) \in F\), recall that we have shown earlier that \( \langle a, b \rangle \in \theta _{F}\) entails \( \langle \mathop {\sim }a, \mathop {\sim }b \rangle \in \theta _{F}\), and therefore also \( \langle \mathop {\sim }\mathop {\sim }a, \mathop {\sim }\mathop {\sim }b \rangle \in \theta _{F}\). By compatibility of \( \theta _{F}\) with the meet, we have \( \langle \mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }c, \mathop {\sim }\mathop {\sim }b \wedge \mathop {\sim }c \rangle \in \theta _{F}\). Thus, in particular, \((\mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }c) \rightarrow (\mathop {\sim }\mathop {\sim }b \wedge \mathop {\sim }c) \in F\). To conclude the proof, it suffices to observe that \( (\mathop {\sim }\mathop {\sim }a \wedge \mathop {\sim }c) \rightarrow (\mathop {\sim }\mathop {\sim }b \wedge \mathop {\sim }c) \mathop {\preceq }\mathop {\sim }(a \rightarrow c) \rightarrow \mathop {\sim }(b \rightarrow c) \). This is a consequence of (QN4c), (QN4e.2) and (QN4e.3) in Definition 3.2, and can be easily verified on a twist-structure: indeed, we have \( (\mathop {\sim }\mathop {\sim }\langle a_1, a_2 \rangle \wedge \mathop {\sim }\langle c_1, c_2 \rangle ) \rightarrow (\mathop {\sim }\mathop {\sim }\langle b_1, b_2 \rangle \wedge \mathop {\sim }\langle c_1, c_2 \rangle ) = \langle (\Box a_1 \wedge c_2 ) \rightarrow (\Box b_1 \wedge c_2) , \Box (\Box a_1 \wedge c_2 ) \wedge \Box (b_2 \vee \Box c_1 ) \rangle \) and \(\mathop {\sim }(\langle a_1, a_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) \rightarrow \mathop {\sim }(\langle b_1, b_2 \rangle \rightarrow \langle c_1, c_2 \rangle ) = \langle (\Box a_1 \wedge c_2 ) \rightarrow (\Box b_1 \wedge c_2 ), \Box (\Box a_1 \wedge c_2 ) \wedge \Box (\Box b_1 \rightarrow \Box c_1) \rangle \). A similar reasoning shows \(\mathop {\sim }(b \rightarrow c) \rightarrow \mathop {\sim }(a \rightarrow c) \in F\). We have established that \( \langle a, b \rangle \in \theta _{F}\) entails \( \langle a \rightarrow c, b \rightarrow c \rangle \in \theta _{F}\). We proceed to show that \( \langle c \rightarrow a, c \rightarrow b \rangle \in \theta _{F}\). It suffices to check that \((c \rightarrow a ) \rightarrow (c \rightarrow b) \in F\) and \(\mathop {\sim }(c \rightarrow a) \rightarrow \mathop {\sim }(c \rightarrow b) \in F\). The former is straightforward: just observe that \(a \rightarrow b \mathop {\preceq }c \rightarrow (a \rightarrow b) \mathop {\preceq }(c \rightarrow a ) \rightarrow (c \rightarrow b) \). As to the latter, we reason as before and recall that \( (\mathop {\sim }\mathop {\sim }c \wedge \mathop {\sim }a) \rightarrow (\mathop {\sim }\mathop {\sim }c \wedge \mathop {\sim }b) \mathop {\preceq }\mathop {\sim }(c \rightarrow a) \rightarrow \mathop {\sim }(c \rightarrow b) \). To conclude the proof, it suffices to observe that, as shown earlier, \( \langle a, b \rangle \in \theta _{F}\) entails \( \langle \mathop {\sim }a, \mathop {\sim }b \rangle \in \theta _{F}\) and this latter gives us \( \langle \mathop {\sim }\mathop {\sim }c \wedge \mathop {\sim }a, \mathop {\sim }\mathop {\sim }c \wedge \mathop {\sim }b \rangle \in \theta _{F}\).

(iv). Applying the definitions, we have \(a \in F_{\theta _{F}}\) iff \(\langle a, |a| \rangle \in \theta _{F}\) iff \( a \rightarrow |a|, |a| \rightarrow a, \mathop {\sim }a \rightarrow \mathop {\sim }|a| , \mathop {\sim }|a| \rightarrow \mathop {\sim }a \in F\). Since \(|a | \rightarrow a = a \), we have \(F_{\theta _{F}} \subseteq F\). To check the converse inclusion, assume \(a \in F\), and observe that \(b \rightarrow |b| = |b \rightarrow |b||\), so \(b \rightarrow |b| \in F\) for all \(b \in A\). Hence, \( a \rightarrow |a|, |a| \rightarrow a \in F\). To conclude the proof, it suffices to note that \(a \mathop {\preceq }\mathop {\sim }a \rightarrow \mathop {\sim }|a|\) and \( \mathop {\sim }|a| \rightarrow \mathop {\sim }a = | \mathop {\sim }|a| \rightarrow \mathop {\sim }a |\). The latter follows from item (ix) of Proposition 2.4, and the former can be easily checked on a twist-structure. Indeed, we have \( \mathop {\sim }\langle a_1, a_2 \rangle \rightarrow \mathop {\sim }|\langle a_1, a_2 \rangle | = \langle a_2 \rightarrow (\Box a_1 \wedge a_2) , \Box a_2 \wedge 1 \rangle =\langle a_2 \rightarrow \Box a_1, \Box a_2 \wedge 1 \rangle \), so the result follows from the observation that \(a_1 \le \Box a_1 \le a_2 \rightarrow \Box a_1\).

(v). Assume \(\langle a,b \rangle \in \theta _{F_{\theta }}\). Applying the definitions, we have \(\langle a,b \rangle \in \theta _{F_{\theta }}\) iff \(a \rightarrow b, b \rightarrow a, \mathop {\sim }a \rightarrow \mathop {\sim }b , \mathop {\sim }b \rightarrow \mathop {\sim }a \in F_{\theta }\) iff \(\langle a \rightarrow b, |a \rightarrow b| \rangle , \langle b \rightarrow a, |b \rightarrow a| \rangle , \langle \mathop {\sim }a \rightarrow \mathop {\sim }b, |\mathop {\sim }a \rightarrow \mathop {\sim }b| \rangle , \langle \mathop {\sim }b \rightarrow \mathop {\sim }a, |\mathop {\sim }b \rightarrow \mathop {\sim }a| \rangle \in \theta \). Then we have \(\langle (a \rightarrow b) \wedge (\mathop {\sim }b \rightarrow \mathop {\sim }a) \wedge (\mathop {\sim }a \rightarrow \mathop {\sim }b) \wedge ( b \rightarrow a), |a \rightarrow b| \wedge |\mathop {\sim }b \rightarrow \mathop {\sim }a| \wedge |\mathop {\sim }a \rightarrow \mathop {\sim }b| \wedge |b \rightarrow a|\rangle = \langle a \Leftrightarrow b, |a \rightarrow b| \wedge |\mathop {\sim }b \rightarrow \mathop {\sim }a| \wedge |\mathop {\sim }a \rightarrow \mathop {\sim }b| \wedge |b \rightarrow a|\rangle \in \theta \). From the latter, we obtain \(\langle (a \Leftrightarrow b) \rightarrow a, (|a \rightarrow b| \wedge |\mathop {\sim }b \rightarrow \mathop {\sim }a| \wedge |\mathop {\sim }a \rightarrow \mathop {\sim }b| \wedge |b \rightarrow a| ) \rightarrow a \rangle = \langle (a \Leftrightarrow b) \rightarrow a, a \rangle \in \theta \). The last equality holds because, using items (i) and (ii) of Proposition 2.4, we have \((|c| \wedge |d|) \rightarrow e = |c | \rightarrow (|d| \rightarrow e ) = |c | \rightarrow e = e \) for all \(c,d,e \in \mathbf {A} \). In a similar way we obtain \( \langle (a \Leftrightarrow b) \rightarrow b, b \rangle \in \theta \). By item (xii) of Proposition 2.4, we have \((a \Leftrightarrow b) \rightarrow a = (a \Leftrightarrow b) \rightarrow b\). Hence, \(\langle (a \Leftrightarrow b) \rightarrow a, (a \Leftrightarrow b) \rightarrow b \rangle \in \theta \), which gives us \(\langle a, b \rangle \in \theta \). Thus, \(\theta _{F_{\theta }} \subseteq \theta \). The converse inclusion is easier. Assuming \(\langle a, b \rangle \in \theta \), we have \(\langle a \rightarrow b, b \rightarrow b \rangle \in \theta \), which gives us \(\langle (a \rightarrow b) \rightarrow (a \rightarrow b), (b \rightarrow b) \rightarrow (a \rightarrow b) \rangle = \langle |a \rightarrow b|, a \rightarrow b \rangle \in \theta \), as required. In a similar way we have \( \langle |b \rightarrow a|, b \rightarrow a \rangle \in \theta \). To obtain \( \langle |\mathop {\sim }a \rightarrow \mathop {\sim }b|, \mathop {\sim }a \rightarrow \mathop {\sim }b \rangle , \langle |\mathop {\sim }b \rightarrow \mathop {\sim }a|, \mathop {\sim }b \rightarrow \mathop {\sim }a \rangle \in \theta \) one can also reason in a similar way: it suffices to observe that \(\langle a, b \rangle \in \theta \) entails \(\langle \mathop {\sim }a, \mathop {\sim }b \rangle \in \theta \). \(\square \)

Theorem 4.4

The maps given by \(\theta \mapsto F_{\theta }\) and \(F \mapsto \theta _{F}\) establish an isomorphism between the complete lattices \(Fi(\mathbf {A} )\) and \(\text {Con}(\mathbf {A} )\).

Proof

Both maps are clearly order-preserving. Lemma 4.5 entails they are also order-reflecting (hence injective) and inverses of one another. \(\square \)

Lemma 4.5

Let \( \mathbf {B} = \langle B , \wedge ,\vee , \rightarrow , \Box \rangle \) be a nuclear Brouwerian algebra. Then \(\mathrm {Con}(\mathbf {B}) = \mathrm {Con}(\langle B , \wedge ,\vee , \rightarrow \rangle )\).

Proof

Let \(\theta \in \mathrm {Con}(\langle B , \wedge ,\vee , \rightarrow \rangle ) \), and assume \(\langle a,b \rangle \in \theta \). Then \(\langle a \rightarrow b , b \rightarrow b \rangle = \langle a \rightarrow b, 1 \rangle \in \theta \). Since \(a \rightarrow b \le \Box (a \rightarrow b) \le \Box a \rightarrow \Box b\), from \(\langle a \rightarrow b, 1 \rangle \in \theta \) we obtain \( \langle (a \rightarrow b) \vee (\Box a \rightarrow \Box b), 1 \vee (\Box a \rightarrow \Box b) \rangle = \langle \Box a \rightarrow \Box b, 1 \rangle \in \theta \). From the latter, we have \(\langle \Box a \wedge (\Box a \rightarrow \Box b), \Box a \wedge 1 \rangle = \langle \Box a \wedge \Box b, \Box a \rangle \in \theta \). A similar reasoning establishes \( \langle \Box a \wedge \Box b, \Box b \rangle \in \theta \), so \( \langle \Box a, \Box b \rangle \in \theta \). Hence, \(\theta \in \mathrm {Con}(\mathbf {B}) \), as required. \(\square \)

Corollary 4.6

Let \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) be a quasi-N4-lattice, where \( \mathbf {B} = \langle B , \wedge ,\vee , \rightarrow , \Box \rangle \). Then \(\mathrm {Con}(\mathbf {A} ) \cong \mathrm {Con}(\mathbf {B}) = \mathrm {Con}(\langle B , \wedge ,\vee , \rightarrow \rangle ) \).

Proof

The equality \(\mathrm {Con}(\mathbf {B}) = \mathrm {Con}(\langle B , \wedge ,\vee , \rightarrow \rangle )\) has been established in Lemma 4.5. The required result will be obtained by composing the following isomorphisms. It is well known that the lattice filters \(Fi(\mathbf {B})\) of a Brouwerian algebra form a complete lattice that is isomorphic to \(\mathrm {Con}(\langle B , \wedge ,\vee , \rightarrow \rangle )\). In turn, by Theorem 4.2, we have \(Fi(\mathbf {B}) \cong Fi(\mathbf {A} ) \), and Theorem 4.4 gives us \( Fi(\mathbf {A} ) \cong \text {Con}(\mathbf {A} ) \). \(\square \)

It may be interesting to illustrate the correspondence that we obtain by composing the isomorphisms mentioned in the proof of Corollary 4.6. Every \(\eta \in \mathrm {Con}(\mathbf {B})\) determines a congruence \(\eta _{\mathbf {A} } \in \mathrm {Con}(\mathbf {A} )\) given by:

$$\begin{aligned} \eta _{\mathbf {A} } : = \{ \langle \langle a_1, a_2 \rangle , \langle b_1, b_2 \rangle \rangle {\in } A {\times } A : \langle a_1, b_1 \rangle , \langle a_2, b_2 \rangle {\in } \eta \}. \end{aligned}$$

Conversely, for \(\theta \in \mathrm {Con}(\mathbf {A} )\), we have \(\theta _{\mathbf {B}} \in \mathrm {Con}(\mathbf {B})\) given by:

$$\begin{aligned} \theta _{\mathbf {B}} := & {} \{ \langle a, b \rangle \in B \times B : \text { there is } c \in B \text { s.t. } \langle a \leftrightarrow b, c \rangle \in A \\&\text { and }\quad \langle \langle a \leftrightarrow b, c \rangle , |\langle a \leftrightarrow b, c \rangle | \rangle \in \theta \}. \end{aligned}$$

The previous results allow us to justify an observation announced at the end of the preceding section.

Theorem 4.7

\({\mathbb {V}}({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}) \) is axiomatized relative to \(\mathsf {QN4}\) by the identity (1):

$$\begin{aligned}&((x \wedge \mathop {\sim }x) \rightarrow y ) \vee (\mathop {\sim }\mathop {\sim }z \rightarrow z ) \approx \\&\quad |((x \wedge \mathop {\sim }x) \rightarrow y ) \vee (\mathop {\sim }\mathop {\sim }z \rightarrow z )|. \end{aligned}$$

Proof

Let \({\mathsf {K}}\) be the subvariety of \(\mathsf {QN4}\) axiomatized by the identity (1). We have observed earlier that \({\mathbb {V}}({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}) \subseteq {\mathsf {K}}\). To verify the converse inclusion, we are going to show that every subdirectly irreducible member of \({\mathsf {K}}\) belongs to \({{\mathsf {Q}}}{{\mathsf {N}}}\cup {{\mathsf {N}}}{{\mathsf {4}}}\). Let then \(\mathbf {A} \le \mathbf {B}^{\bowtie }\) be a subdirectly irreducible QN4-lattice in \({\mathsf {K}}\). By Corollary 4.6 (see also item (ii) of Corollary 4.13), the \(\Box \)-free reduct of \(\mathbf {B}\) is a subdirectly irreducible Brouwerian algebra. Then \(\mathbf {B}\) has a unique co-atom (see, e.g., Galatos et al. 2007, Thm. 1.23) which entails that the least lattice filter \(\{ 1 \}\) on \(\mathbf {B}\) is prime. Using Theorem 4.2, it is easy to see that \(F = (\{ 1 \} \times B) \cap A \), which is the least filter on \(\mathbf {A} \), is also prime. By (1), for all elements \(a,b,c \in A\), we have \( ((a \wedge \mathop {\sim }a) \rightarrow b ) \vee (\mathop {\sim }\mathop {\sim }c \rightarrow c ) \in F \). Since F is prime, this means that either \( (a \wedge \mathop {\sim }a) \rightarrow b \in F\) or \(\mathop {\sim }\mathop {\sim }c \rightarrow c \in F\). Recalling Proposition 3.8, we have in the former case \(\mathbf {A} \in {{\mathsf {Q}}}{{\mathsf {N}}}\), and in the latter \(\mathbf {A} \in {{\mathsf {N}}}{{\mathsf {4}}}\), as required. \(\square \)

4.2 EDPC, CEP and congruence-permutability

We shall now proceed to show that the variety of QN4-lattices possesses a ternary deduction term and a quaternary deductive term in the sense of Blok and Pigozzi (1994), as well as a Maltsev term witnessing congruence-permutability. This entails that quasi-N4-lattices have equationally definable principal congruences (EDPC) and a strong version of the congruence extension property (CEP).

Let:

$$\begin{aligned} (q(x,y,z)) := (x \Leftrightarrow y) \rightarrow z. \end{aligned}$$

Lemma 4.8

Let \(\mathbf {A} \) be a quasi-N4-lattice and \(a,b,c,d \in A\).

  1. (i)

    \(q(a,a,b)= b\).

  2. (ii)

    \(q(a,b,a)= q(a,b,b)\).

  3. (iii)

    \( q(a,b,\mathop {\sim }c) = q(a,b, \mathop {\sim }q(a,b,c))\).

  4. (iv)

    \( q(a,b, c \rightarrow d) = q(a,b, q(a,b,c) \rightarrow q(a,b,d))\).

  5. (v)

    \( q(a,b, c \wedge d) = q(a,b, q(a,b,c) \wedge q(a,b,d))\).

  6. (vi)

    \( q(a,b, c \vee d) = q(a,b, q(a,b,c) \vee q(a,b,d))\).

  7. (vii)

    \(q(a,b,q(c,d,e))= q(c,d,q(a,b,e))\).

Proof

(i). Throughout the proof, we will assume \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) and work with generic elements \(a= \langle a_1, a_2 \rangle , b= \langle b_1, b_2 \rangle \) etc. Recall that \( \langle a_1 ,a_2 \rangle \Leftrightarrow \langle b_1, b_2 \rangle = \langle (a_1 \leftrightarrow b_1) \wedge (a_2 \leftrightarrow b_2), \Box ((\Box a_1 \wedge b_2) \vee (\Box b_1 \wedge a_2)) \rangle \). Thus, \( \langle a_1 ,a_2 \rangle \Leftrightarrow \langle a_1, a_2 \rangle = \langle (a_1 \leftrightarrow a_1) \wedge (a_2 \leftrightarrow a_2), \Box ((\Box a_1 \wedge a_2) \vee (\Box a_1 \wedge a_2)) \rangle = \langle 1, \Box a_1 \wedge a_2 \rangle =| \langle 1, \Box a_1 \wedge a_2 \rangle |\). Then the result follows from item (i) of Proposition 2.4.

(ii). This is item (xii) of Proposition 2.4.

(iii). From now on, to simplify the notation, let us abbreviate \(\alpha _1 : = a_1 \leftrightarrow b_1\) and \(\alpha _2 : = a_2 \leftrightarrow b_2\) Taking into account item (i), we have \( q( \langle a_1 ,a_2 \rangle , \langle b_1, b_2 \rangle ,\mathop {\sim }\langle c_1, c_2 \rangle ) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow c_2, \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box c_1 \rangle \) and \(\mathop {\sim }q( \langle a_1 ,a_2 \rangle , \langle b_1, b_2 \rangle ,\langle c_1, c_2 \rangle ) = \langle \Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2, \Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \rangle \). Thus, \( q(a,b, \mathop {\sim }q(a,b,c)) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow (\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2), \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \rangle \). We must therefore show that

$$\begin{aligned} (\alpha _1 \wedge \alpha _2) \rightarrow c_2 = (\alpha _1 \wedge \alpha _2) \rightarrow (\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) \end{aligned}$$

and

$$\begin{aligned}&\Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box c_1\\&\quad = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1). \end{aligned}$$

Regarding the first components, observe that \( \alpha _1 \wedge \alpha _2 \le \Box (\alpha _1 \wedge \alpha _2) = \Box \alpha _1 \wedge \Box \alpha _2 \). Thus, using item (iii) of Proposition 2.4, we have \( (\alpha _1 \wedge \alpha _2) \rightarrow (\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) = ((\alpha _1 \wedge \alpha _2) \rightarrow (\Box \alpha _1 \wedge \Box \alpha _2)) \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow c_2) = 1 \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow c_2) = (\alpha _1 \wedge \alpha _2) \rightarrow c_2 \), which entails the required result. The second components are straightforward. Indeed, recalling that \(x \wedge (x \rightarrow y) \approx x \wedge y\) holds on every Brouwerian algebra, we have \( \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) = \Box ( \alpha _1 \wedge \alpha _2 \wedge (\alpha _1 \wedge \alpha _2) \rightarrow c_1 ) = \Box ( \alpha _1 \wedge \alpha _2 \wedge c_1 ) = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box c_1 \).

(iv). Let us compute \( q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle \rightarrow \langle d_1 ,d_2 \rangle ) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \rightarrow d_1), \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box c_1 \wedge d_2 \rangle \) and \( q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle ) \rightarrow q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle d_1 ,d_2 \rangle ) = \langle (\alpha _1) \wedge \alpha _2) \rightarrow c_1, \Box \alpha _1 \wedge \Box \alpha _2 \wedge c_1 \rangle \rightarrow \langle (\alpha _1 \wedge \alpha _2) \rightarrow d_1, \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2 \rangle = \langle ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \rightarrow ((\alpha _1 \wedge \alpha _2) \rightarrow d_1), \Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2 \rangle \). Hence,

$$\begin{aligned}&q(\langle a_1 ,a_2 \rangle , \langle b_1 , b_2 \rangle , q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle ) \\&\quad \rightarrow q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle d_1 ,d_2 \rangle )) \end{aligned}$$

reduces to \(\langle (\alpha _1 \wedge \alpha _2) \rightarrow (((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \rightarrow (\alpha _1 \wedge \alpha _2) \rightarrow d_1)), \Box \alpha _1 \wedge \Box \alpha _2 \wedge (\Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2) \rangle \). We thus need to check that \( (\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \rightarrow d_1) = (\alpha _1 \wedge \alpha _2) \rightarrow (((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \rightarrow (\alpha _1 \wedge \alpha _2) \rightarrow d_1)) \) and \( \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box c_1 \wedge d_2 = \Box \alpha _1 \wedge \Box \alpha _2 \wedge (\Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2) \). The first equality is a consequence of the identity \(x \rightarrow (y \rightarrow z) \approx x \rightarrow ((x \rightarrow y ) \rightarrow (x \rightarrow z))\), which holds on every Brouwerian algebra. Regarding the second equality, we have \( \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2 = \Box (\alpha _1 \wedge \alpha _2) \wedge \Box ((\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge d_2 = \Box (\alpha _1 \wedge \alpha _2 \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow c_1)) \wedge d_2 = \Box (\alpha _1 \wedge \alpha _2 \wedge c_1) \wedge d_2 = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box c_1 \wedge d_2 \).

(v). Let us compute \( q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle \wedge \langle d_1 ,d_2 \rangle ) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \wedge d_1) , \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box (c_2 \vee d_2) \rangle \) and \( q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle ) \wedge q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle d_1 ,d_2 \rangle ) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow c_1 , \Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2 \rangle \wedge \langle (\alpha _1 \wedge \alpha _2) \rightarrow d_1 , \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2 \rangle = \langle ( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow d_1) , \Box ((\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) \vee (\Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2)) \rangle \).

Hence,

$$\begin{aligned}&q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle ) \\&\quad \wedge q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle d_1 ,d_2 \rangle )) \end{aligned}$$

reduces to \(\langle (\alpha _1 \wedge \alpha _2) \rightarrow ( ( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)), \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ((\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) \vee (\Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2)) \rangle \), and we need to check that

$$\begin{aligned}&(\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \wedge d_1) = (\alpha _1 \wedge \alpha _2) \\&\quad \rightarrow ( ( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)) \end{aligned}$$

and

$$\begin{aligned}&\Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box (c_2 \vee d_2) = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \\&\quad \Box ((\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) \vee (\Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2)). \end{aligned}$$

The former equality follows from the identity \(x \rightarrow (y \wedge z) \approx x \rightarrow ((x \rightarrow y) \wedge (x \rightarrow z))\), which is valid on every Brouwerian algebra. As to the latter, recalling that \(\Box c_2 = c_2 \) and \(\Box d_2 = d_2\), we have \( \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ((\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) \vee (\Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2)) = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box (\Box ( \alpha _1 \wedge \alpha _2 \wedge c_2) \vee \Box ( \alpha _1 \wedge \alpha _2 \wedge d_2) ) = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ( ( \alpha _1 \wedge \alpha _2 \wedge c_2) \vee ( \alpha _1 \wedge \alpha _2 \wedge d_2) ) = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box ( \alpha _1 \wedge \alpha _2 \wedge (c_2 \vee d_2) ) = \Box (\alpha _1 \wedge \alpha _2 \wedge \alpha _1 \wedge \alpha _2 \wedge (c_2 \vee d_2) ) = \Box (\alpha _1 \wedge \alpha _2 \wedge (c_2 \vee d_2) ) = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box (c_2 \vee d_2), \) as required.

(vi). Let us compute \( q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle \vee \langle d_1 ,d_2 \rangle ) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \vee d_1) , \Box \alpha _1 \wedge \Box \alpha _2 \wedge (c_2 \wedge d_2) \rangle \) and \( q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle ) \vee q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle d_1 ,d_2 \rangle ) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow c_1 , \Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2 \rangle \vee \langle (\alpha _1 \wedge \alpha _2) \rightarrow d_1 , \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2 \rangle = \langle ( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1) , (\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) \wedge (\Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2) \rangle \). Hence, \(q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle c_1 ,c_2 \rangle ) \vee q(\langle a_1 ,a_2 \rangle , \langle b_1 ,b_2 \rangle , \langle d_1 ,d_2 \rangle )) = \langle (\alpha _1 \wedge \alpha _2) \rightarrow (( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)), \Box \alpha _1 \wedge \Box \alpha _2 \wedge (\Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2) \wedge (\Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2) \rangle \). We thus need to check that

$$\begin{aligned}&(\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \vee d_1) = (\alpha _1 \wedge \alpha _2) \\&\quad \rightarrow (( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)) \end{aligned}$$

and \( \Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2 \wedge d_2 = \Box \alpha _1 \wedge \Box \alpha _2 \wedge \Box \alpha _1 \wedge \Box \alpha _2 \wedge c_2 \wedge \Box \alpha _1 \wedge \Box \alpha _2 \wedge d_2 \). The latter equality is clear; as to the former, observe that \( c_1 \vee d_1 \le ( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1) \) entails \( (\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \vee d_1) \le (\alpha _1 \wedge \alpha _2) \rightarrow (( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)) \). The converse inequality \( (\alpha _1 \wedge \alpha _2) \rightarrow (( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)) \le (\alpha _1 \wedge \alpha _2) \rightarrow (c_1 \vee d_1) \) is equivalent, by residuation, to \( (\alpha _1 \wedge \alpha _2) \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow (( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1))) \le c_1 \vee d_1\). Note that \( (\alpha _1 \wedge \alpha _2) \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow (( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1))) = \alpha _1 \wedge \alpha _2 \wedge (( (\alpha _1 \wedge \alpha _2) \rightarrow c_1) \vee ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)) = (\alpha _1 \wedge \alpha _2 \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow c_1)) \vee (\alpha _1 \wedge \alpha _2 \wedge ((\alpha _1 \wedge \alpha _2) \rightarrow d_1)) = (\alpha _1 \wedge \alpha _2 \wedge c_1) \vee (\alpha _1 \wedge \alpha _2 \wedge d_1) = (\alpha _1 \wedge \alpha _2) \wedge (c_1 \vee d_2) \le c_1 \vee d_1 \). Hence, the required result follows.

(vii). We need to show \( (a \Leftrightarrow b) \rightarrow ((c \Leftrightarrow d) \rightarrow e) = (c \Leftrightarrow d) \rightarrow ((a \Leftrightarrow b) \rightarrow e) \), which is an easy consequence of item (ii) of Proposition 2.4. \(\square \)

Lemma 4.8 allows us to apply (Blok and Pigozzi 1994, Thm. 2.3, Cor. 2.4) to obtain the following result, which generalizes the one established about N4-lattices in Spinks and Veroff (2018, Thm. 4.26).

Theorem 4.9

q(xyz) is a commutative ternary deduction term in the sense of Blok and Pigozzi (1994). Therefore, the variety of quasi-N4-lattices has equationally definable principal congruences and the strong congruence extension property (Blok and Pigozzi 1994, Thm. 2.12).

By Theorem 4.9, for every quasi-N4-lattice \(\mathbf {A} \), the principal congruence generated by elements \(a, b \in A\) is given by \(\theta (a,b) = \{ \langle c, d \rangle : (a \Leftrightarrow b) \rightarrow c = (a \Leftrightarrow b) \rightarrow d \}\).

Theorem 4.10

The variety of quasi-N4-lattices is congruence-permutable with Maltsev term:

$$\begin{aligned}&p(x,y,z) := (((x \Rightarrow y ) \wedge |z | ) \Rightarrow z) \wedge \\&\quad (((z \Rightarrow y ) \wedge |x | ) \Rightarrow x). \end{aligned}$$

Proof

We need to show that every quasi-N4-lattice \(\mathbf {A} \) satisfies \( p(x,x,y) \approx y \) and \( p(x,y,y) \approx x \). To see this, let \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) and \(a= \langle a_1, a_2 \rangle , b= \langle b_1, b_2 \rangle \in A\). We claim that \( (a \Rightarrow a ) \wedge |b|) \Rightarrow b = b \) and \( b \le (b \Rightarrow a ) \wedge |a|) \Rightarrow a \), which entails \(p(a,a,b) = ((a \Rightarrow a ) \wedge |b|) \Rightarrow b) \wedge ((b \Rightarrow a ) \wedge |a|) \Rightarrow a) = b \wedge ((b \Rightarrow a ) \wedge |a|) \Rightarrow a) = b\) and, by the same token, \(p(a,b,b) = a\).

Let us compute: \( ((\langle a_1, a_2 \rangle \Rightarrow \langle a_1, a_2 \rangle ) \wedge |\langle b_1, b_2 \rangle | ) \Rightarrow \langle b_1, b_2 \rangle = \langle 1, \Box (\Box a_1 \wedge a_2 \rangle ) \vee (\Box b_1 \wedge b_2) \rangle \Rightarrow \langle b_1, b_2 \rangle = \langle (1 \rightarrow b_1) \wedge (b_2 \rightarrow \Box ((\Box a_1 \wedge a_2 \rangle ) \vee (\Box b_1 \wedge b_2))), \Box 1 \wedge b_2 \rangle = \langle b_1 \wedge (b_2 \rightarrow \Box ((\Box a_1 \wedge a_2 \rangle ) \vee (\Box b_1 \wedge b_2))), b_2 \rangle = \langle b_1, b_2 \rangle \). The last equality holds because of the following (in)equalities: \(b_1 \le \Box b_1 \le b_2 \rightarrow \Box b_1 = (b_2 \rightarrow \Box b_1) \wedge 1 = (b_2 \rightarrow \Box b_1) \wedge (b_2 \rightarrow b_2) = b_2 \rightarrow (\Box b_1 \wedge b_2) \le b_2 \rightarrow ((\Box a_1 \wedge a_2 \rangle ) \vee (\Box b_1 \wedge b_2)) \le b_2 \rightarrow \Box ((\Box a_1 \wedge a_2 \rangle ) \vee (\Box b_1 \wedge b_2))\)

Now let us compute: \( ((\langle b_1, b_2 \rangle \Rightarrow \langle a_1, a_2 \rangle ) \wedge |\langle a_1, a_2 \rangle | ) \Rightarrow \langle a_1, a_2 \rangle = \langle (b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2) \wedge 1 , \Box ( (\Box b_1 \wedge a_2 ) \vee (\Box a_1 \wedge a_2) ) \rangle \Rightarrow \langle a_1, a_2 \rangle = \langle (((b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2)) \rightarrow a_1) \wedge (a_2 \rightarrow \Box ( (\Box b_1 \wedge a_2 ) \vee (\Box a_1 \wedge a_2) ), \Box ((b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2)) \wedge \Box a_2 \rangle \). Observe that \(b_1 \le (((b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2)) \rightarrow a_1) \wedge (a_2 \rightarrow \Box ( (\Box b_1 \wedge a_2 ) \vee (\Box a_1 \wedge a_2) )\) because of the following (in)equalities: \( b_1 \le (b_1 \rightarrow a_1) \rightarrow a_1 \le (a_2 \rightarrow b_2) \rightarrow ((b_1 \rightarrow a_1) \rightarrow a_1) = ((b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2)) \rightarrow a_1 \) and \( b_1 \le \Box b_1 \le a_2 \rightarrow \Box b_1 = (a_2 \rightarrow \Box b_1) \wedge 1 = (a_2 \rightarrow \Box b_1) \wedge (a_2 \rightarrow a_2 ) = a_2 \rightarrow (\Box b_1 \wedge a_2 ) \le a_2 \rightarrow \Box (\Box b_1 \wedge a_2 ) \le a_2 \rightarrow \Box ( (\Box b_1 \wedge a_2 ) \vee (\Box a_1 \wedge a_2)) \). Furthermore, recalling that \(\Box b_2 = b_2\), we have \(\Box ((b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2)) \wedge \Box a_2 \le b_2\) because \( \Box ((b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2)) \wedge \Box a_2 = \Box ((b_1 \rightarrow a_1) \wedge (a_2 \rightarrow b_2) \wedge a_2) = \Box ((b_1 \rightarrow a_1) \wedge a_2 \wedge b_2) \le \Box (a_2 \wedge b_2) \le \Box b_2 = b_2 \). Thus, \(p(a,a,b) = b\), as claimed. \(\square \)

As a variety of enriched lattices, quasi-N4-lattices are obviously congruence-distributive. Thus, the preceding theorem extends the result of Spinks and Veroff (2018, Cor. 4.25) to the non-involutive setting.

Corollary 4.11

The variety of quasi-N4-lattices is arithmetical.

It is known (Spinks and Veroff 2018, Lemma 4.28) that a variety having a ternary deduction term and a Maltsev term must also possess a quaternary deductive term in the sense of Blok et al. (1984, Def. 1.1). Thus, Theorems 4.9 and 4.10 give us the following result, extending (Spinks and Veroff 2018, Thm. 4.29).

Corollary 4.12

The variety of quasi-N4-lattices has a quaternary deductive term

$$\begin{aligned} \quad \qquad t (x,y,z,w) : = p( q(x,y,z), q(x,y,w), w), \end{aligned}$$

where, as before, \(p(x,y,z) = (((x \Rightarrow y ) \wedge |z | ) \Rightarrow z) \wedge (((z \Rightarrow y ) \wedge |x | ) \Rightarrow x)\) and \(q(x,y,z) = (x \Leftrightarrow y) \rightarrow z\).

Corollary 4.13

Let \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) be a quasi-N4-lattice, where \( \mathbf {B} = \langle B , \wedge ,\vee , \rightarrow , \Box \rangle \). The following are equivalent:

  1. (i)

    \(\mathbf {A} \) is directly indecomposable (resp., subdirectly irreducible, simple).

  2. (ii)

    \( \langle B , \wedge ,\vee , \rightarrow \rangle \) is a directly indecomposable (resp., subdirectly irreducible, simple) Brouwerian algebra.

Proof

For subdirectly irreducible and simple algebras, the result is an immediate consequence of Corollary 4.6. For directly indecomposable algebras, it suffices to further observe that both Brouwerian algebras (see, e.g., (Galatos et al. 2007, p. 94)) and quasi-N4-lattices (by Theorem 4.10) are congruence-permutable. \(\square \)

Recall that, according to Spinks et al. (2019), an algebra \(\mathbf {A} \) having constants 0 and 1 is (0, 1)-congruence orderable if and only if, for all \(a,b \in A\), it holds that

$$\begin{aligned} \theta (0, a) = \theta (0, b) \text { and } \theta (1, a) = \theta (1, b) \quad \text {implies}\quad a = b, \end{aligned}$$

where \(\theta (a, b)\) denotes the principal congruence generated by \(\{a,b\}\) in \(\mathbf {A} \). As mentioned earlier, it was shown in Spinks et al. (2019) and Rivieccio and Spinks (2020) that Nelson and quasi-Nelson algebras coincide with, respectively, the class of (0, 1)-congruence orderable involutive residuated lattices and the class of (0, 1)-congruence orderable residuated lattices. Although an arbitrary (quasi-)N4-lattice \(\mathbf {A} \) need not have any definable algebraic constant, it can be shown that \(\mathbf {A} \) satisfies a property that reminds one closely of (0, 1)-congruence orderability, and could lead to a generalization of the latter that might be applicable outside the setting of pointed algebras (cf. Problem 8.1 in Spinks et al. (2019)). We prove this in item (iii) of the next proposition.

Proposition 4.14

Let \(\mathbf {A} \) be a quasi-N4-lattice and \(a,b, c \in A\).

  1. (i)

    \(a \Leftrightarrow |a| = a\).

  2. (ii)

    \(\theta (a, |a|) = \{ \langle b, c \rangle \in A \times A : a \rightarrow b = a \rightarrow c \}\).

  3. (iii)

    \(a = b\) iff (\(\theta (a, |a|) = \theta (b, |b|) \) and \(\theta (\mathop {\sim }a, | \mathop {\sim }a|) = \theta (\mathop {\sim }b, | \mathop {\sim }b |) \)).

Proof

(i). Let \( \mathbf {A} \le \mathbf {B}^{\bowtie }\) and \(a= \langle a_1, a_2 \rangle , b= \langle b_1, b_2 \rangle \in A\). Let us compute \(\langle a_1, a_2 \rangle \Leftrightarrow |\langle a_1, a_2 \rangle | = \langle (a_1 \leftrightarrow 1) \wedge (a_2 \leftrightarrow (\Box a_1 \wedge a_2)), \Box (\Box a_1 \wedge \Box a_1 \wedge a_2) \vee (\Box 1 \wedge a_2)) \rangle = \langle a_1 \wedge (a_2 \rightarrow (\Box a_1 \wedge a_2)) \wedge ((\Box a_1 \wedge a_2) \rightarrow a_2), \Box ((\Box a_1 \wedge a_2) \vee a_2 ) \rangle = \langle a_1 \wedge (a_2 \rightarrow \Box a_1) \wedge (a_2 \rightarrow a_2) \wedge 1, \Box a_2 \rangle = \langle a_1 \wedge 1, \Box a_2 \rangle = \langle a_1 , a_2 \rangle \).

(ii). By Theorem 4.9, we have \(\langle b, c \rangle \in \theta (a, |a|) \) iff \((a \Leftrightarrow |a|) \rightarrow b = (a \Leftrightarrow |a|) \rightarrow c\), and by item (i) above we have \((a \Leftrightarrow |a|) \rightarrow b = a \rightarrow b\) and \( (a \Leftrightarrow |a|) \rightarrow c =a \rightarrow c\).

(iii). To verify the only non-trivial implication, assume we have \(\theta (a, |a|) \!= \theta (b, |b|) \) and \(\theta (\mathop {\sim }a, | \mathop {\sim }a|) \!= \theta (\mathop {\sim }b, | \mathop {\sim }b |) \). Thus, \(\langle b, |b| \rangle \in \theta (a, |a|)\), which by item (ii) above means \(a \rightarrow b = a \rightarrow |b|\). By item (xiii) of Proposition 2.4, we have \(a \rightarrow |b| = a \rightarrow (b \rightarrow b) = |a \rightarrow b |\). Hence, \(a \mathop {\preceq }b\), and a similar reasoning gives us \(b \mathop {\preceq }a\). Thus, \(a \mathbin \equiv b\). Applying the same reasoning to the assumption \(\theta (\mathop {\sim }a, | \mathop {\sim }a|) = \theta (\mathop {\sim }b, | \mathop {\sim }b |) \), from \(\langle \mathop {\sim }b, | \mathop {\sim }b| \rangle \in \theta (\mathop {\sim }a, |\mathop {\sim }a|)\) we obtain \(\mathop {\sim }a \rightarrow \mathop {\sim }b = \mathop {\sim }a \rightarrow |\mathop {\sim }b |\), so \(\mathop {\sim }a \mathop {\preceq }\mathop {\sim }b\), and similarly we have \(\mathop {\sim }b \mathop {\preceq }\mathop {\sim }a \). Then \(\mathop {\sim }a \mathbin \equiv \mathop {\sim }b\), and we can invoke item (QN4d) of Definition 3.2 to conclude \(a = b\). \(\square \)

5 Future work

The aim of the present work has been to initiate the study of a potentially interesting new class of algebras related to well-known non-classical logics. Future research may explore several directions, and time will tell to which extent such a research will turn out to be fruitful. We mention below a few topics on quasi-N4-lattices that, from our current standpoint, appear to deserve further investigation.

In the first place, given the connection of the algebraic structures considered here with Nelson logics, there is the question of introducing a logical calculus corresponding to quasi-N4-lattices. We believe that quasi-N4-lattices are likely to turn out to be the equivalent algebraic semantics of an algebraizable logic (in Blok and Pigozzi’s (1989) sense), and we conjecture that the same translations that witness the algebraizability of paraconsistent Nelson logic (see, e.g., (Rivieccio 2011, Thm. 2.6)) will work for the logic of quasi-N4-lattices as well. A related question is whether one might be able to present an alternative view of quasi-N4-lattices as algebras of relevance logics and introduce a corresponding logical calculus accordingly, generalizing the result of Spinks and Veroff (2018) on N4-lattices and paraconsistent Nelson logic; Remark 3.5 suggests that this may indeed be a feasible project.

From a structural point of view the representation stated in Theorem 3.3, though quite useful in practice, appears less satisfactory than the corresponding known results on Nelson algebras and N4-lattices. This is because Theorem 3.3 does not tell us how a given quasi-N4-lattice sits inside the full product algebra into which it is embedded. In the case of Nelson algebras and N4-lattices, the missing information is provided by what Odintsov called invariants, which in our case would be the sets \(\nabla \) and \(\Delta \) mentioned in Proposition 2.5. The latter, however, only tells us that every triple \( \langle B, \nabla , \Delta \rangle \) uniquely determines a quasi-N4-lattice: it is an open question whether every quasi-N4-lattice may be obtained in this way as a twist-structure from a triple \( \langle B, \nabla , \Delta \rangle \).

A last topic that deserves to be mentioned is the investigation of sub(quasi)varieties of quasi-N4-lattices, an enterprise in which the twist-structure representation may prove to be a very helpful tool (especially in its improved version, which includes the above-mentioned invariants); see, e.g., the analogous case of subvarieties of quasi-Nelson algebras in Rivieccio and Jansana (2021, Sect. 3.1). In particular, a recent paper Rivieccio et al. (2020) has drawn attention to the role played by the so-called prelinearity identity in the context of quasi-Nelson algebras, and to the connection of the latter with well-known algebras of fuzzy logics (on the role of prelinearity within the theory of N4-lattices we refer the reader to Aguzzoli et al. (2017)). Preliminary results indicate that a similar investigation may prove to be equally fruitful, and perhaps even more insightful, in the wider setting of quasi-N4-lattices.