2.1 Universal algebra

We write $f:A\twoheadrightarrow B$ if f is a surjective homomorphism between A and B and we say that B is homomorphic image of A. We denote by $B\preceq A$ that B is a subalgebra of A and by $\prod _{i\in I}A_i$ the product of the family of algebras $\{A_i\}_{i\in I}$ . If I is finite, we also write $A_0\times \cdots \times A_n$ for the product $\prod _{i\in I} A_i$ . For every $i\in I$ we also have a projection function $\pi _i: \prod _{i\in I} A_i \rightarrow A_i $ such that $\pi _i : \alpha \mapsto \alpha (i)$ . It is easy to show that every such projection function is a surjective homomorphism. We introduce the following closure maps.

Definition 2.1. Let $\mathcal {K}$ be a set of algebras of the same similarity-type, we then define the following:

$$ \begin{align*} & A\in I(\mathcal{K}) \text{ iff } A \text{ is isomorphic to some algebra in } \mathcal{K} \\ & A\in S(\mathcal{K}) \text{ iff } A \text{ is a subalgebra of some algebra in } \mathcal{K} \\ & A\in H(\mathcal{K}) \text{ iff } A \text{ is homomorphic image of some algebra in } \mathcal{K}\\ & A\in P(\mathcal{K}) \text{ iff } A \text{ is product of a nonempty family of algebras in } \mathcal{K}. \end{align*} $$

The following proposition provides a characterisation of how the previous maps interact with one another.

A variety is defined as a class of algebras $\mathcal {V}$ of the same similarity type which is closed under homomorphic images, subalgebras and products. If $\mathcal {K}$ is an arbitrary class of algebras of the same similarity type, then we write $\mathcal {V}(\mathcal {K})$ for the variety generated by $\mathcal {K}$ , i.e., for the smallest class of algebras containing $\mathcal {K}$ which is closed under subalgebras, homomorphic images and products. An important theorem by Birkhoff establishes that varieties are exactly the classes of algebras which are definable by equations [Reference Burris and Sankappanavar7, Theorem 11.9].

Finally, we recall the following important theorems, which provide an internal characterisation of algebraic varieties. The first theorem, due to Tarski, characterizes the variety generated by a set of algebras in terms of the closure maps defined above. The second theorem is an important result by Birkhoff which shows that subdirectly irreducible algebras play an important role as generators of varieties. We use $\mathcal {V}_{SI}$ to denote the collection of subdirectly irreducible algebras of a variety $\mathcal {V}$ . For a proof of these results see [Reference Burris and Sankappanavar7, Theorems 9.5 and 9.7].

2.2 Heyting algebras

A Heyting algebra is a bounded lattice H such that for every $a,b\in H$ there is some element $a\rightarrow b\in H$ such that for all $c\in H$ we have that $c\leq a\rightarrow b \Leftrightarrow c\land a\leq b $ . Given an element $a\in H$ of a Heyting algebra, we define its pseudocomplement $\neg a$ as $\neg a := a \rightarrow 0$ . In case for all $a\in H$ it is the case that $a \land \neg a = 0$ and $a \lor \neg a = 1$ we say that H is a Boolean algebra. It is well known that a Heyting algebra H is subdirectly irreducible iff H has a second greatest element $s_H$ .

A power-set algebra is a Boolean algebra $B=(\wp (X),\cup ,\cap ,\setminus, \emptyset, X)$ , where the universe is a power-set, the algebraic operations of join and meet are the set-theoretic operations of union and intersection and complementation is the set-theoretic complement. We recall that every finite Boolean algebra B is isomorphic to a power-set algebra, i.e., $B\cong \wp (X)$ for some finite set X, see e.g., [Reference Davey and Priestley16, Chapter 5]. Thus it follows that finite Boolean algebras are always equivalent up to isomorphism to $\wp (n)$ for some $n\in \mathbb {N}$ . It is easy to show that if $n\leq m$ , then $\wp (n)\preceq \wp (m)$ . Then, by identifying every $\wp (n)$ by $2^n$ , it follows that finite Boolean algebras form an ordered chain of subalgebras:

$$ \begin{align*} 2^0\space\preceq\space 2^1\space\preceq\space 2^2\space\preceq\space 2^3\space\preceq\space 2^4\space\preceq\cdots \end{align*} $$

2.3 Intermediate logics

Intermediate logics are a well-studied class of logics with many applications in mathematics and computer science. Fix a countable set $\mathtt {AT}$ of atomic propositional formulas, we define the set of propositional formulas $\mathcal {L}_P$ inductively as follows.

Definition 2.5. The language $\mathcal {L}_P$ is defined as follows, where $p\in \mathtt {AT}$ :

$$ \begin{align*} \varphi ::= p \mid \top \mid \bot \mid \varphi\land\varphi \mid \varphi \lor \varphi \mid \varphi \rightarrow \varphi. \end{align*} $$

Negation is defined as $\neg \varphi :=\varphi \rightarrow \bot $ . If $\varphi $ is a formula, then we write $\varphi (\overline {x})$ or $\varphi (x_0,\dots ,x_n)$ to specify that the atomic formulas in $\varphi $ are among those of $\overline {x}$ or respectively of $x_0,\dots ,x_n$ . A substitution is a function $\eta : \mathtt {AT} \rightarrow \mathcal {L}_P$ which naturally lifts by induction to formulas by setting, for every connective $\odot $ , the map $(\psi \odot \chi ) \mapsto \eta (\psi )\odot \eta (\chi ) $ . If $\varphi $ is a formula and q occurs in $\varphi $ , we write for the formula obtained by the substitution $\eta : q\mapsto p $ . Similarly, if $\overline {q}=q_0,\dots ,q_n$ are variables in $\varphi $ , then we write for the formula obtained by the substitution $\eta : q_i \mapsto p_i $ for all $i\leq n$ .

We denote by $\mathtt {IPC}$ the intuitionistic propositional calculus and by $\mathtt {CPC}$ the classical propositional calculus. Now, given a propositional language $\mathcal {L}_P$ , we say that a set of formulas $L\subseteq \mathcal {L}_P$ is a superintuitionistic logic if $\mathtt {IPC}\subseteq L$ and in addition L is closed under modus ponens and uniform substitution. An intermediate logic is a superintuitionistic logic L which is also consistent, namely $\bot \notin L$ . We thus identify every logical system with the sets of its theorems.

It can be proven that $\mathtt {CPC}$ is the maximal intermediate logic and that intermediate logics are all the logics L such that $\mathtt {IPC} \subseteq L \subseteq \mathtt {CPC}$ . We denote by $L + \varphi $ the closure under substitution and modus ponens of the set of formulas $L \cup \{\varphi \}$ and by $L + \Gamma $ the closure under substitution and modus ponens of the set of formulas $L \cup \Gamma $ . If L is an intermediate logic and $\varphi \in L$ then we write $\vdash _L \varphi $ or $L\vdash \varphi $ . Moreover, if $\varphi $ can be obtained by closing the set $L \cup \Gamma $ under modus ponens, then we write $\Gamma \vdash _L \varphi $ and we say that $\varphi $ is derivable from $\Gamma $ in L. It is a well-know fact [Reference Chagrov and Zakharyaschev8, Chapter 4.1] that intermediate logics form a bounded lattice $ \Lambda (\mathtt {IPC}) $ with $\mathtt {IPC} = \bot $ and $\mathtt {CPC} = \top $ and where meet and join are defined as follows

$$ \begin{align*} L_0 \land L_1 \space &=\space L_0 \cap L_1, \\ L_0 \lor L_1 \space &=\space L_0 + L_1. \end{align*} $$

We list here some intermediate logics that will be useful for us in this article:

$$ \begin{align*} \begin{array}{l @{} l} \mathtt{KC} &\hspace{2pt} = \space \mathtt{IPC} \space + \space \neg p \lor \neg\neg p, \\ \mathtt{KP} &\hspace{2pt} = \space \mathtt{IPC} \space + \space (\neg p \rightarrow q\lor r) \rightarrow (\neg p \rightarrow q) \lor (\neg p \rightarrow r), \\ \mathtt{ND} &\hspace{2pt} =\space \mathtt{IPC} \space + \space \{ (\neg p \rightarrow \bigvee_{i\leq k} \neg q_i )\rightarrow \bigvee_{i\leq k}(\neg p \rightarrow \neg q_i) : k\geq 2 \}. \end{array} \end{align*} $$

The logic ND was introduced by Maksimova in [Reference Maksimova34]. The logic $\mathtt {KP}$ was introduced by Kreisel and Putnam in [Reference Kreisel and Putnam33]. The logic KC is also know as the logic of the weak excluded middle and was introduced by Jankov in [Reference Jankov30]. While the previous logics are defined in axiomatic terms, one can also define logics by specifying the class of structures they correspond to. The logic $\mathtt {ML}$ is the logic of so-called Medvedev frames and it was introduced by Medvedev in [Reference Medvedev36]. A relational structure $\mathcal {F}$ is a Medvedev frame if $\mathcal {F}\cong (\wp ^+(W),\supseteq )$ , where W is a finite set and $\wp ^+(W)=\{X\subseteq W : X\neq \emptyset \}$ . A Medvedev model is then defined as a relational model over a Medvedev frame. Let $\mathcal {C}$ be the class of all Medvedev frames, then we have that $ \mathtt {ML}= \{\varphi \in \mathcal {L}_P : \mathcal {C} \Vdash \varphi \}$ , i.e., $\mathtt {ML}$ is the set of formulas valid in all Medvedev frames (here we assume the reader’s familiarity with the standard Kripke semantics of intuitionistic logic).

We will now briefly recall the algebraic semantics of intermediate logics.

Given an algebraic model $M=(H,V)$ , we define by induction the interpretation of any formula $\varphi \in \mathcal {L}_P$ .

Definition 2.7 (Interpretation of Arbitrary Formulas)

Given an algebraic model M and a formula $\varphi \in \mathcal {L}$ , its interpretation

is defined as follows:

When the valuation V is clear from the context, we simply write for the interpretation of $\varphi $ in H under V. We say that a formula $\varphi $ is true under $ V $ in H or true in the model $ M=(H, V) $ and write $M\vDash \varphi $ if . We say that $\varphi $ is valid in H and write $H\vDash \varphi $ if $\varphi $ is true in every algebraic model $M=(H,V)$ over H. Given a class of Heyting algebras $\mathcal {C}$ , we say that $\varphi $ is valid in $ \mathcal {C} $ and write $\mathcal {C}\vDash \varphi $ if $\varphi $ is valid in every Heyting algebra $H\in \mathcal {C}$ . Finally, we say that $\varphi $ is a validity if $\varphi $ is valid in any Heyting algebra H.

We denote by HA the collection of all Heyting algebras. Let $ \Lambda (\mathrm{HA}) $ be the lattice of varieties of Heyting algebras and $ \Lambda (\mathtt {IPC}) $ the lattice of intermediate logics, we then define the two maps $Var: \Lambda (\mathtt {IPC}) \rightarrow \Lambda (\mathrm{HA}) $ and $Log: \Lambda (\mathrm{HA}) \rightarrow \Lambda (\mathtt {IPC}) $ as follows:

$$ \begin{align*} &Var: L\mapsto \{H\in \mathrm{HA} : H\vDash L \};\\ &Log: \mathcal{V} \mapsto \{\varphi\in \mathcal{L}_P : \mathcal{V}\vDash \varphi \}. \end{align*} $$

That the two former functions are well defined follows from $Var(L)$ being a variety of Heyting algebras and $Log(\mathcal {V})$ being an intermediate logic. Also, one can prove that both these maps are order-reversing homomorphisms. We say that a variety of Heyting algebras $\mathcal {V}$ is defined by a set of formulas $\Gamma $ if $\mathcal {V}=Var(\Gamma )$ and we say $\mathcal {V}$ is definable if there exists one such $\Gamma $ . We say that an intermediate logic L is algebraically complete with respect to a class of Heyting algebras $\mathcal {C}$ if $L=Log(\mathcal {C})$ .

Theorem 2.8 (Definability Theorem)

Every variety of Heyting algebras $\mathcal {V}$ is defined by its validities, i.e., for every Heyting algebra H,

$$ \begin{align*} H\in \mathcal{V} \Leftrightarrow H\vDash Log(\mathcal{V}). \end{align*} $$

Theorem 2.9 (Algebraic Completeness)

Every intermediate logic L is complete with respect to its corresponding variety of Heyting algebras, i.e., for every $\varphi \in \mathcal {L}_P$ ,

$$ \begin{align*} \varphi\in L \Leftrightarrow Var(L)\vDash \varphi. \end{align*} $$

We refer the reader to [Reference Chagrov and Zakharyaschev8, Section 7] for a full proof of the aforementioned two results and the related constructions. Here let us only remark that the first of these two results is an immediate application of the fact that varieties and equational classes coincide. The second result relies essentially on the free-algebra construction, namely on the Lindenbaum–Tarski algebra of intermediate logics. These results together give us the following theorem.

Here, the isomorphisms between $\Lambda (\mathtt {IPC}) $ and $\Lambda (\mathrm{HA}) $ are the two maps $Log$ and $Var$ . We sometimes refer to the previous theorem as a duality result concerning $\Lambda (\mathtt {IPC}) $ and $\Lambda (\mathrm{HA}) $ . Notice that we are implicitly excluding from the lattice $ \Lambda (\mathrm{HA}) $ the trivial variety generated by a singleton set, for it dually corresponds to the inconsistent logic containing all the formulas of $\mathcal {L}_P$ .

2.4 Inquisitive semantics

Inquisitive logic is a formalism extending the repertoire of (classical) propositional logic with questions, in order to study their logical relations. The term question in this context refers to the expressions whose semantics is not completely determined by their truth-conditions (i.e., which evaluations make it true), as it is the case for questions in natural language. And in fact the idea to define the semantics for this logic is to shift from a semantics based on truth-conditions to a semantics based on information (e.g., what pieces of information allow to resolve the question or entail the formula).

In this section we recall the basic definitions of inquisitive logic, which follow the intuition presented above. For an extended exposition on the logic and the idea underlying it we refer to [Reference Ciardelli11, Reference Ciardelli, Groenendijk and Roelofsen13].

Though sometimes inquisitive logic is introduced in a signature containing special question-forming operators—most notably the inquisitive disjunction , see e.g., [Reference Ciardelli11]—here we follow [Reference Ciardelli9] and present $\mathtt {InqB}$ in the same language $\mathcal {L}_P$ of intermediate logics. The intended interpretation of the logical operators is the same as for propositional logic (e.g., $p \land q$ stands for “both p and q hold”), with one exception: the disjunction operator $\vee $ is used to introduce alternative questions. For example, the formula $p \vee \neg p$ is intuitively interpreted as the question “whether p holds,” requesting information on which of the two alternatives holds.

As mentioned above, the semantics of $\mathtt {InqB}$ is defined in terms of information to properly characterize the logical relations between questions. The usual (classical) valuations (i.e., binary functions $w:\mathtt {AT}\rightarrow \{0,1 \}$ ) are interpreted as complete descriptions of the current state of affairs. We refer to the set $2^{\mathtt {AT}}$ of all classical valuations over $\mathtt {AT}$ as the evaluation space over $\mathtt {AT}$ . To represent pieces of information, inquisitive logic uses information states (or simply states), that is, subsets of the evaluation space. So for example, the information that “the atomic formula p is true” is represented by the set of all and only the evaluations satisfying p: $\left \{ w \in 2^{\mathtt {AT}} \middle | w(p) = 1 \right \}$ . This allows us to define the notion of support at a state, as follows.

Definition 2.11 (Support at a State)

Let $\varphi $ be a formula of $\mathcal {L}_P$ and $s\in \wp (2^{\mathtt {AT}})$ a state. We say that s supports $\varphi $ and we define $s\vDash \varphi $ inductively as follows:

$$ \begin{align*} \begin{array}{l @{\hspace{1em}} c @{\hspace{1em}} l} s\vDash p &\Longleftrightarrow & \forall w\in s \ ( w(p)=1) \\ s\vDash \top && \text{always} \\ s\vDash \bot &\Longleftrightarrow & s=\emptyset\\ s\vDash \psi \land \chi &\Longleftrightarrow & s\vDash \psi \text{ and } s\vDash \chi\\ s\vDash \psi \lor \chi &\Longleftrightarrow & s\vDash \psi \text{ or } s\vDash \chi \\ s\vDash \psi \rightarrow \chi &\Longleftrightarrow & \forall t \ ( \text{if }t\subseteq s \text{ and } t\vDash\psi \text{ then } t\vDash \chi ). \end{array} \end{align*} $$

For $p\in \mathtt {AT} $ and a state s, we introduce the notation , that is, is the set of classical valuations in s that make p true. Since $\neg \varphi = \varphi \rightarrow \bot $ , the semantic clause of negation is then the following:

$$ \begin{align*} &s\vDash \neg \varphi \Longleftrightarrow \forall t\ (\text{if }t\subseteq s \text{ then } t\nvDash\varphi \text{ or } t = \emptyset ). \end{align*} $$

The valid formulas of inquisitive logic (which with a slight abuse of notation we denote by $\mathtt {InqB}$ ) are the formulas $\varphi \in \mathcal {L}_P$ which are supported in every evaluation state:

$$ \begin{align*}\mathtt{InqB}= \{ \varphi\in \mathcal{L}_P : \forall s\in \wp(2^{\mathtt{AT}}), s\vDash \varphi \}.\end{align*} $$

We present a simple example to show that the support semantics works as intended: let us determine which states support the formula $p \vee \neg p$ .

$$ \begin{align*} \begin{array}{ll} s \vDash p \vee \neg p &\iff\; s \vDash p \text{ or } s \vDash \neg p \\ &\iff\; \forall w\in s\; (w(p) = 1) \text{ or } \forall t\subseteq s\; ( t \nvDash p \text{ or } t = \emptyset ) \\ &\iff\; \forall w\in s\; (w(p) = 1) \text{ or } \forall w\in s\; (w(p) = 0). \end{array} \end{align*} $$

That is, the formula $p \vee \neg p$ is supported by s if either all the valuations in s satisfy p or all the valuations in s do not satisfy p. This is in line with the intended interpretation of these objects: the question “whether p holds” (represented by $p \vee \neg p$ ) is resolved by the pieces of information (represented by the states s) from which we can either infer that p is true ( $w(p) = 1$ for every $w\in s$ ) or that p is false ( $w(p) = 0$ for every $w\in s$ ).

3.1 $\mathtt {DNA}$ -logics

We proceed by introducing the negative variant of an intermediate logic. Negative variants were first introduced by Miglioli et al. in [Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti37] and later employed by Ciardelli in [Reference Ciardelli9]. The account of [Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti37] is slightly different than the one adopted in [Reference Ciardelli9] and in the current paper, since the focus of [Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti37] is mainly the study of Medvedev’s logic and its properties. The main result of [Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti37] is, in fact, a new proof of the maximality of Medvedev’s logic among the intermediate logics with the disjunction property.

If $\varphi \in \mathcal {L}_P$ is an arbitrary formula, we often say that the formula obtained by replacing all the atomic letters in $\varphi $ with their negation is its negative variant.

Definition 3.1 (Negative Variant)

For every intermediate logic L, its negative variant $L^\neg $ is defined as follows:

A $\mathtt {DNA}$ -logic is then defined as the negative variant of some intermediate logic L. The name $\mathtt {DNA}$ stands for double negation atoms, which refers to the fact that, as we will see, $\mathtt {DNA}$ -logics prove $\neg \neg p \rightarrow p$ for all atomic formulas $p\in \mathtt {AT}$ . We will use the notation $L^\neg $ to refer to the negative variant of an intermediate logic L. If not specified otherwise, we reserve uppercase greek letters $\Gamma $ and $\Delta $ to denote arbitrary sets of formulas and $\Lambda $ and $\Pi $ to denote $\mathtt {DNA}$ -logics. As for an example of this kind of logics, Ciardelli showed in [Reference Ciardelli9, Theorem 3.4.9] that inquisitive logic is indeed a $\mathtt {DNA}$ -logic: he proved that $\mathtt {InqB}$ is the negative variant of all and only the intermediate logics extending Maksimova’s logic $\texttt {ND}$ and contained in Medvedev’s logic $\texttt {ML}$ . A well-known example of intermediate logic in this interval is the Kreisel–Putnam logic $\texttt {KP}$ . We refer to [Reference Ciardelli9, Section 3] for an overview of these logics and for further discussion on these results.

The following proposition provides us with an axiomatisation for every $\mathtt {DNA}$ -logic.

As an immediate consequence, we obtain an Hilbert-style axiomatization for $\mathtt {InqB}$ , based on the fact that $\mathtt {InqB} = \texttt {KP}^{\neg }$ . This system was originally presented and proved to be sound and complete for $\mathtt {InqB}$ in [Reference Ciardelli9] (see [Reference Ciardelli9, Definition 3.2.13] and [Reference Ciardelli9, Theorem 3.4.9]). The current formulation was presented in [Reference Bezhanishvili, Grilletti, Holliday, Iemhoff, Moortgat and de Queiroz5].

$$ \begin{align*} \mathbf{Axioms } & \hspace{10pt} \mbox{All tautologies of}\ \mathtt{IPC} \\ & \hspace{10pt} (\neg \varphi \rightarrow \psi\lor \chi) \rightarrow (\neg \varphi \rightarrow \psi) \lor (\neg \varphi \rightarrow \chi) \space \text{ for all } \varphi,\psi,\chi\in\mathcal{L}_P \\ &\hspace{10pt} \neg \neg p \rightarrow p \text{ for all } p\in\mathtt{AT} \\ \mathbf{Rule } & \hspace{10pt} \varphi, \varphi\rightarrow \psi \Rightarrow \psi. \end{align*} $$

As we will see later, $\mathtt {DNA}$ -logics give rise to a lattice structure ordered by the set-theoretic inclusion. The meet of two $\mathtt {DNA}$ -logics $\Lambda _0,\Lambda _1$ is just their intersection and their join is the closure of their union under modus ponens. We will thus write $\Lambda _0\land \Lambda _1:=\Lambda _0\cap \Lambda _1$ and $\Lambda _0\lor \Lambda _1:=(\Lambda _0\cup \Lambda _1)^{MP}$ , where we denote by $(\Gamma )^{MP}$ the closure under modus ponens of a set $\Gamma $ of formulas. If $\varphi $ can be obtained by closing the set $ \Gamma $ of formulas under modus ponens, then we write $\Gamma \vdash \varphi $ and we say that $\varphi $ is derivable from $\Gamma $ . One can show by standard reasoning that $\Gamma \vdash \varphi $ if and only if there is a finite set of formulas $\{\psi _i\}_{i\leq n}\subseteq \Gamma $ such that $\{\psi _i\}_{i\leq n}\vdash \varphi $ . We often write $\psi _0,\dots ,\psi _n\vdash \varphi $ for $\{\psi _i\}_{i\leq n}\vdash \varphi $ .

Proof. Assume without the loss of generality that $\Lambda _0 = L_0^\neg $ and $\Lambda _1 = L_1^\neg $ .

(i) It is straightforward to verify that:

Hence $\Lambda _0 \land \Lambda _1$ is the least set of formulas satisfying the conditions in Proposition 3.3 with respect to the intermediate logic $L_0 \cap L_1$ .

(ii) We show that $\Lambda _0 \vee \Lambda _1 = (\Lambda _0 \cup \Lambda _1)^{MP}$ is the least set of formulas satisfying the conditions in Proposition 3.3 with respect to the intermediate logic $L_0 \vee L_1 := (L_0 \cup L_1)^{MP}$ .

It suffices to show that $(L_0\lor L_1)^\neg = (L_0^\neg \cup L_1^\neg )^{MP}$ . By definition we have that $(L_0\lor L_1)^\neg = ((L_0\cup L_1)^{MP})^\neg $ and $ L_0^\neg \lor L_1^\neg = (L_0^\neg \cup L_1^\neg )^{MP}$ . It suffices to show that $((L_0\cup L_1)^{MP})^\neg = (L_0^\neg \cup L_1^\neg )^{MP}$ . $(\subseteq )$ Suppose $\varphi \in ((L_0\cup L_1)^{MP})^\neg $ . It follows that , hence for some formulas $\psi _0,\dots ,\psi _n\in L_0\cup L_1$ we have . We immediately obtain that . It follows that and, since $\neg \neg p \rightarrow p \in L_0^\neg \cup L_1^\neg $ for all $p\in \mathtt {AT}$ , we obtain $\varphi \in (L_0^\neg \cup L_1^\neg )^{MP}$ . $(\supseteq )$ Suppose that $\varphi \in (L_0^\neg \cup L_1^\neg )^{MP} $ . It follows that for some formulas $\psi _0,\dots ,\psi _n\in L_0^\neg \cup L_1^\neg $ we have that $\psi _0,\dots ,\psi _n\vdash \varphi $ , that is, there is a derivation of $\varphi $ from $\psi _0,\dots ,\psi _n$ . Therefore, and by substituting each $\psi _i$ with in the previous derivation, we obtain . So and consequently $\varphi \in ((L_0\cup L_1)^{MP})^\neg $ .

We denote by $\Lambda (\mathtt {IPC}^\neg ) $ the lattice of $\mathtt {DNA}$ -logics. Since intermediate logics also form a lattice $ \Lambda (\mathtt {IPC}) $ , we can then show that the map $(-)^\neg :\Lambda (\mathtt {IPC}) \rightarrow \Lambda (\mathtt {IPC}^\neg ) $ which assigns each intermediate logic to its negative variant is a lattice homomorphism.

3.2 Algebraic semantics for $\mathtt {DNA}$ -logics

In the existing literature, negative variants have been considered from a syntactic point of view [Reference Ciardelli9, Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti37]. An algebraic semantics for inquisitive logic was introduced in [Reference Bezhanishvili, Grilletti, Holliday, Iemhoff, Moortgat and de Queiroz5]. Here we extend this algebraic approach to $\mathtt {DNA}$ -logics.

Recall that, if H is a Heyting algebra, then we say that an element $x\in H$ is regular if $x=\neg \neg x$ . For any Heyting algebra H we then denote by $H_\neg $ the set:

$$ \begin{align*}H_\neg = \{ x\in H : x = \neg \neg x \} .\end{align*} $$

So $H_\neg $ consists of all regular elements of the Heyting algebra H. Note that since in every Heyting algebras we have that $\neg x = \neg \neg \neg x$ , the set of regular elements of H can also be specified as $H_\neg = \{ y\in H : \exists x \in H (y = \neg x) \}$ . We define $\mathtt {DNA}$ -models as follows.

We then say that $\mu $ is a $\mathtt {DNA}$ -valuation over the Heyting algebra H. Given a $\mathtt {DNA}$ -model $M=(H,\mu )$ , we define by induction the interpretation of any formula $\varphi \in \mathcal {L}_P$ .

Definition 3.7 (Interpretation of Arbitrary Formulas)

Given a $\mathtt {DNA}$ -model $M=(H,\mu )$ and a formula $\varphi \in \mathcal {L}_P$ , its interpretation

is defined by the following recursive clauses:

When the valuation $\mu $ is clear from the context, we simply write for the interpretation of $\varphi $ in H under $\mu $ . From the former definitions it is straightforward to adapt the usual definitions of truth at a model and validity. We say that a formula $\varphi $ is true under $ \mu $ in H or true in the model $ M=(H, \mu ) $ and write $M\vDash ^\neg \varphi $ if . We say that $\varphi $ is $\mathtt {DNA}$ -valid in H and write $H\vDash ^\neg \varphi $ if $\varphi $ is true in every model $M=(H,\mu )$ over H. Given a class $\mathcal {C}$ of Heyting algebras, we say that $\varphi $ is $\mathtt {DNA}$ -valid in $ \mathcal {C} $ and write $\mathcal {C}\vDash ^\neg \varphi $ if $\varphi $ is $\mathtt {DNA}$ -valid in every Heyting algebra $H\in \mathcal {C}$ . Finally, we say that $\varphi $ is a $\mathtt {DNA}$ -validity if $\varphi $ is valid in any Heyting algebra H. When the context is clear, we drop the qualification $\mathtt {DNA}$ from the definitions above and talk simply of validity.

$\mathtt {DNA}$ -validity and standard validity are closely intertwined. To see how, we first introduce the notion of negative variant of a valuation.

The following lemma, which is easy to prove, shows that the set of $\mathtt {DNA}$ -valuations and the set of negative variants of standard valuations coincide.

By the previous lemma, a generic $\mathtt {DNA}$ -valuation is always of the form $V^{\neg }$ for some valuation V. We will henceforth write $V^\neg $ for an arbitrary $\mathtt {DNA}$ -valuation. We can now prove the following important lemma.

Lemma 3.10. For every Heyting algebra H, for every valuation V and any formula $\varphi $ , we have

Proof. The proof goes by induction on the complexity of $\varphi $ . The only non-trivial case is $\varphi = p \in \mathtt {AT}$ :

From this we can derive the following result.

Thus we end up with the following proposition: if a Heyting algebra validates an intermediate logic, then it also validates its negative variant.

Notice that it is not true in general that $H\vDash ^\neg L^\neg $ entails $H\vDash L$ . $\mathtt {DNA}$ -valuations form a subclass of all valuation and it might very well be that a formula is true in a Heyting algebra under all $\mathtt {DNA}$ -valuations but not under all valuations. However, the next proposition is a weaker version of this fact which we will need later. Let $\langle H_\neg \rangle $ be the subalgebra of H generated by $H_{\neg }$ . First we prove the following lemma.

This allows us to prove the following result.

3.3 $\mathtt {DNA}$ -varieties

The algebraic semantics for $\mathtt {DNA}$ -logics that we have defined in the previous section motivates the introduction of $\mathtt {DNA}$ -varieties. We will define $\mathtt {DNA}$ -varieties as varieties of algebras which are additionally closed under so-called core-superalgebras. This notion plays an important role in the algebraic semantics of $\mathtt {DNA}$ -logics and is defined as follows.

A core superalgebra K of a Heyting algebra H is thus a subalgebra of H such that K and H share the same regular elements. $\mathtt {DNA}$ -varieties are then defined as follows.

Moreover, as $\mathtt {DNA}$ -logics can be seen also as negative variants of intermediate logic, one can regard $\mathtt {DNA}$ -varieties as special kinds of closure of standard varieties.

Definition 3.17 (Negative Closure of a Variety)

For every variety of Heyting algebras $\mathcal {V}$ , its negative closure $\mathcal {V}^\uparrow $ is defined as follows:

$$ \begin{align*}\mathcal{V}^\uparrow= \{H \in \mathrm{HA} : \exists A\in \mathcal{V} \text{ such that } A_{\neg}=H_{\neg} \text{ and } A\preceq H \}.\end{align*} $$

We use the notation $\mathcal {V}^\uparrow $ to refer to the negative variant of a variety $\mathcal {V}$ and we generally write $\mathcal {X}$ for $\mathtt {DNA}$ -varieties. If not specified otherwise, we reserve $\mathcal {C}$ to denote arbitrary classes of Heyting algebras, $\mathcal {V}$ or $\mathcal {U}$ to denote standard varieties and $\mathcal {X}$ or $\mathcal {Y}$ to denote $\mathtt {DNA}$ -varieties.

The following proposition establishes that every $\mathtt {DNA}$ -variety is the negative closure of a standard variety.

Proof. ( $\Rightarrow $ ) If a set of algebras $\mathcal {X}$ is a $\mathtt {DNA}$ -variety, then it is closed under subalgebras, homomorphic images and products and thus it is a variety. Moreover, since it is also closed under core superalgebras, it is straightforward to see that $\mathcal {X}=\mathcal {X}^\uparrow $ , so that we can see $\mathcal {X}$ as the negative variant of itself and thus as a $\mathtt {DNA}$ -variety.

( $\Leftarrow $ ) Let $\mathcal {V}^\uparrow $ be the negative variant of some standard variety $\mathcal {V}$ . To prove that $\mathcal {V}^\uparrow $ is a $\mathtt {DNA}$ -variety we need to check that $\mathcal {V}^\uparrow $ is closed under the above four operations.

(1) We check closure under subalgebras. Suppose $H\in \mathcal {V}^\uparrow $ and $K\preceq H$ . Then by definition of $\mathtt {DNA}$ -variety it follows that there is some $H'\in \mathcal {V}$ such that $ H^{\prime }_{\neg }=H_{\neg } $ and $ H'\preceq H $ . Now consider $K'=H'\cap K$ , since $K'$ is the intersection of two subalgebras of H, it will also be closed under the Heyting algebra operations. Thus we have that $K'$ is also a Heyting algebra and $K'\preceq H'$ and $K'\preceq K$ . Therefore, by the fact that $H'\in \mathcal {V}$ and $\mathcal {V}$ is closed under subalgebras, it then follows that $K'\in \mathcal {V}$ . Moreover, since $H^{\prime }_\neg =H_\neg \supseteq K_\neg $ , we have that $K^{\prime }_\neg = H^{\prime }_\neg \cap K_\neg = K_\neg $ . Finally, we showed that for $K'\in \mathcal {V}$ we have $K'\preceq K$ and $K^{\prime }_\neg = K_\neg $ , which entails $K\in \mathcal {V}^\uparrow $ .

(2) We check closure under homomorphic images. Suppose $H\in \mathcal {V}^\uparrow $ and $f: H\twoheadrightarrow K$ , then by the definition of $\mathtt {DNA}$ -variety we have that for some $H'\in \mathcal {V}$ that $ H^{\prime }_{\neg }=H_{\neg } $ and $ H'\preceq H $ . Consider $K'=f[H']$ . Since homomorphic images preserve subalgebras, we have $K'\preceq K$ and, by the closure of standard varieties under homomorphic images $K'\in \mathcal {V}$ . Moreover, since by assumption $H_\neg = H^{\prime }_\neg $ , we have $K_\neg =f[H_\neg ]=f[H^{\prime }_\neg ]=K^{\prime }_\neg $ . Thus for $K'\in \mathcal {V}$ we have $K'\preceq K$ and $K^{\prime }_\neg = K_\neg $ , which yields $K\in \mathcal {V}^\uparrow $ .

(3) We check closure under products. Suppose $H^i\in \mathcal {V}^\uparrow $ for all $i\in I$ of some index-set I. Then we need to check that $\prod _{i\in I} H^i\in \mathcal {V}^\uparrow $ . By the definition of $\mathtt {DNA}$ -variety it immediately follows that there is, for every $i\in I$ , a Heyting algebra $K^i\in \mathcal {V}$ such that $H^i_\neg =K^i_\neg $ , and $K^i\preceq H^i$ . Then by the closure under products of $\mathcal {V}$ , we have that $\prod _{i\in I} K^i\in \mathcal {V}$ . Now, since $K^i\preceq H^i$ holds for every $i\in I$ , it follows immediately that $\prod _{i\in I} K^i\preceq \prod _{i\in I} H^i$ . Similarly, we have that:

$$ \begin{align*}\left(\prod_{i\in I} H^i\right)_\neg=\prod_{i\in I} H^i_\neg=\prod_{i\in I} K^i_\neg=\left(\prod_{i\in I} K^i\right)_\neg.\end{align*} $$

Hence, by the fact that $\prod _{i\in I} K^i\in \mathcal {V}$ and the definition of $\mathtt {DNA}$ -variety, it follows that $\prod _{i\in I} H^i\in \mathcal {V}^\uparrow $ .

(4) We check closure under core superalgebras. Suppose $H\in \mathcal {V}^\uparrow $ and for some K we have that $H_\neg =K_\neg $ and $H\preceq K $ . By the definition of $\mathtt {DNA}$ -varieties we have that there is some $H'\preceq H $ such that $H'\in \mathcal {V}$ and $H^{\prime }_\neg = H_\neg $ . Since $H'\preceq H $ and $H\preceq K $ we then have $H'\preceq K $ by the transitivity of subalgebra relation. Moreover, since $H^{\prime }_\neg = H_\neg =K_\neg $ and $H\in \mathcal {V}$ , it finally follows that $K\in \mathcal {V}^\uparrow $ .

As in the case of standard varieties, $\mathtt {DNA}$ -varieties give rise to a lattice structure ordered by the set-theoretic inclusion. As it is customary doing, we implicitly exclude from the lattice of $\mathtt {DNA}$ -varieties the trivial $\mathtt {DNA}$ -variety of one-element algebras. The meet of two $\mathtt {DNA}$ -varieties $\mathcal {X}_0,\mathcal {X}_1$ is just their intersection and their join is the smallest class containing their union and closed under the $\mathtt {DNA}$ -variety operations.

For any class $\mathcal {C}$ of Heyting algebras we say that $\mathcal {X}$ is generated by the class $\mathcal {C}\subseteq \mathcal {X}$ and we write $\mathcal {X}=\mathcal {X}(\mathcal {C})$ if $\mathcal {X}$ is the least class of Heyting algebras such that $\mathcal {C}\subseteq \mathcal {X} $ and $\mathcal {X}$ is closed under subalgebras, homomorphic images, products and core superalgebras. It is then clear that $\mathcal {X}(\mathcal {C})$ is the smallest $\mathtt {DNA}$ -variety containing $\mathcal {C}$ and that $\mathcal {X}(\mathcal {C})=\mathcal {V}(\mathcal {C})^\uparrow $ . We will thus define $\mathcal {X}_0\land \mathcal {X}_1:=\mathcal {X}_0\cap \mathcal {X}_1$ and $\mathcal {X}_0\lor \mathcal {X}_1:=\mathcal {X}(\mathcal {X}_0\cup \mathcal {X}_1)$ . We proceed to prove the following proposition.

We denote the lattice of $\mathtt {DNA}$ -varieties by $ \Lambda (\mathrm{HA}^\uparrow ) $ . As varieties of Heyting algebras also form a lattice $ \Lambda (\mathrm{HA}) $ , one can then show that the map $(-)^\uparrow :\Lambda (\mathrm{HA}) \rightarrow \Lambda (\mathrm{HA}^\uparrow ) $ which assigns every variety of Heyting algebras to its negative closure is a lattice homomorphism.

Proof. Obviously $(-)^\uparrow $ sends $\bot _\Lambda (\mathrm{HA}) $ to $\bot _\Lambda (\mathrm{HA}^\uparrow ) $ and $\top _\Lambda (\mathrm{HA}) $ to $\top _\Lambda (\mathrm{HA}^\uparrow ) $ , so it suffices to check that $(-)^\uparrow $ preserves meets and joins.

(i) Consider two standard varieties $\mathcal {V}_0$ and $\mathcal {V}_1$ . Notice that if there are $A\in \mathcal {V}_0$ and $B\in \mathcal {V}_1$ such that $ A_{\neg }=H_{\neg }$ , $B_{\neg }=H_{\neg }$ and $A\preceq H$ , $B\preceq H $ , then $A\cap B\in \mathcal {V}_0\cap \mathcal {V}_1$ , $(A\cap B)_{\neg }=H_{\neg }$ and $A\cap B\preceq H$ .

$$ \begin{align*} (\mathcal{V}_0\land \mathcal{V}_1)^\uparrow &= \{H: \exists A\in \mathcal{V}_0\cap \mathcal{V}_1 \text{ such that } A_{\neg}=H_{\neg} \text{ and } A\preceq H \}\\ &= \{H: \exists A\in \mathcal{V}_0( A_{\neg}=H_{\neg}, A\preceq H ) \}\cap \{H: \exists A\in \mathcal{V}_1 (A_{\neg}=H_{\neg}, A\preceq H )\}\\ & = \mathcal{V}^\uparrow_0 \land \mathcal{V}^\uparrow_1. \end{align*} $$

which shows that $(-)^\uparrow $ preserves the meet operator.

(ii) Consider two standard varieties $\mathcal {V}_0$ and $\mathcal {V}_1$ , then we have by definition that $(\mathcal {V}_0\lor \mathcal {V}_1)^\uparrow =( \mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1))^\uparrow $ and $ \mathcal {V}^\uparrow _0 \lor \mathcal {V}^\uparrow _1 = \mathcal {X}(\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1)= \mathcal {V}(\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1)^\uparrow $ . It thus suffices to show that $\mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1)^\uparrow = \mathcal {V}(\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1)^\uparrow $ .

$(\subseteq )$ Let us suppose $H\in (\mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1))^\uparrow $ which implies that there is some $K\in \mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1)$ such that $K_\neg = H_\neg $ and $K\preceq H$ . Then clearly $K\in \mathcal {V}(\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1)$ and thus $H\in \mathcal {V}(\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1)^\uparrow $ . $(\supseteq )$ Suppose now $H\in \mathcal {V}(\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1)^\uparrow $ , then for some $K\in \mathcal {V}(\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1)$ we have that $K_\neg = H_\neg $ and $K\preceq H$ . In turn, this means that there exists a family of algebras $\{A_i : i\in I \} \subseteq \mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1$ such that $K \in \mathcal {V}(\{A_i : i\in I \})$ . Since each $A_i$ is in $\mathcal {V}^\uparrow _0 \cup \mathcal {V}^\uparrow _1$ , there exists algebras $B_i\in \mathcal {V}_0 \cup \mathcal {V}_1$ such that $B^i\preceq A^i$ and $A^i_\neg = B^i_\neg $ for every $i\leq n$ . Consequently $A_i \in \mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1)^{\uparrow }$ for every $i \leq n$ ; and $K \in \mathcal {V}(\{A_i : i\in I \}) \subseteq \mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1)^{\uparrow }$ . Since $\mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1)^{\uparrow }$ is a $\mathtt {DNA}$ -variety and H is a core superalgebra of K, we conclude that $H \in \mathcal {V}(\mathcal {V}_0\cup \mathcal {V}_1)^{\uparrow }$ .

We can already give a characterisation of $\mathtt {DNA}$ -varieties by adapting Tarski’s variety theorem to the case of $\mathtt {DNA}$ -varieties.

Let us remark that we have given to both $\mathtt {DNA}$ -logics and $\mathtt {DNA}$ -varieties a twofold characterisation. On the one hand, they can be described in terms of negative variants of some intermediate logics or in terms of negative closure of some variety of Heyting algebras. On the other hand, we can also consider $\mathtt {DNA}$ -logics and $\mathtt {DNA}$ -varieties as sets of formulas closed under some conditions or as classes of algebras closed under some operations.

3.4 The maps $Log^\neg $ and $Var^\neg $

There are two obvious ways to relate formulas and algebras. We define the map $Var^\neg $ sending sets of formulas to the class of Heyting algebras in which they are $\mathtt {DNA}$ -valid and the map $Log^\neg $ sending classes of Heyting algebras to the set of their $\mathtt {DNA}$ -validities. We have:

$$ \begin{align*} &Var^\neg: \Gamma \mapsto \{H\in \mathrm{HA} : H\vDash^{\neg} \Gamma \}; \\ &Log^\neg: \mathcal{C} \mapsto \{\varphi \in \mathcal{L}_P: \mathcal{C}\vDash^{\neg} \varphi \}. \end{align*} $$

We say that a $\mathtt {DNA}$ -variety of Heyting algebras $\mathcal {X}$ is $\mathtt {DNA}$ -defined by a set of formulas $\Gamma $ if $\mathcal {X}=Var^\neg (\Gamma )$ . A class of Heyting algebras $ \mathcal {C} $ is $\mathtt {DNA}$ -definable if there is a set $\Gamma $ of formulas such that $\mathcal {C}=Var^\neg (\Gamma )$ . When the context is clear, we often drop the qualification $\mathtt {DNA}$ and talk simply of definability. We say that a $\mathtt {DNA}$ -logic $\Lambda $ is algebraically complete with respect to a class of Heyting algebras $\mathcal {C}$ if $\Lambda =Log^\neg (\mathcal {C})$ . We will prove in the next section a definability theorem and an algebraic completeness theorem for $\mathtt {DNA}$ -logics. We will thus establish that every $\mathtt {DNA}$ -variety is defined by its validities and that every $\mathtt {DNA}$ -logic is complete with respect to its corresponding $\mathtt {DNA}$ -variety.

We will next show that $Var^\neg (\Gamma )$ is always a $\mathtt {DNA}$ -variety and $Log^\neg (\mathcal {C})$ is always a $\mathtt {DNA}$ -logic. First we prove the following important lemma showing that the $\mathtt {DNA}$ -validity of a formula is preserved by the key operations of a $\mathtt {DNA}$ -variety.

It follows immediately that for every set of formulas $\Gamma $ the class of Heyting algebras $Var^\neg (\Gamma )$ is a $\mathtt {DNA}$ -variety.

It is a straightforward consequence of Proposition 3.23 that every $\mathtt {DNA}$ -definable class of Heyting algebras is also a $\mathtt {DNA}$ -variety. The next proposition shows that for every class $\mathcal {C}$ of Heyting algebras its set of validities $Log^\neg (\mathcal {C})$ is a $\mathtt {DNA}$ -logic.

Proof. We check that for any class $\mathcal {C}$ of Heyting algebras the corresponding set of formulas $ Log^\neg (\mathcal {C}) $ is a $\mathtt {DNA}$ -logic. In particular, we show that $ Log^\neg (\mathcal {C})= Log(\mathcal {C})^\neg $ . We have:

This shows that $ Log^\neg (\mathcal {C}) $ is the negative variant of $Log(\mathcal {C})$ .

3.5 Duality between $\mathtt {DNA}$ -logics and $\mathtt {DNA}$ -varieties

We will now prove our main result about $\mathtt {DNA}$ -logics and $\mathtt {DNA}$ -varieties, showing that their lattices are dually isomorphic. Notice that, so far, we have considered $Log^\neg $ as a map defined over arbitrary classes of Heyting algebras and $Var^\neg $ as a map defined over arbitrary sets of propositional formulas. Now we restrict our attention to the case in which the domain of $Var^\neg $ is the lattice of $\mathtt {DNA}$ -logics $ \Lambda (\mathtt {IPC}^\neg ) $ and the domain of $Log^\neg $ is the lattice of $\mathtt {DNA}$ -varieties $ \Lambda (\mathrm{HA}^\uparrow ) $ .Footnote ³

Since we have shown above that $Var^\neg (\Gamma )$ is always a $\mathtt {DNA}$ -variety and $Log^\neg (\mathcal {C})$ is always a $\mathtt {DNA}$ -logic it follows that we have two maps:

$$ \begin{align*} &Var^\neg: \Lambda(\mathtt{IPC}^\neg) \rightarrow \Lambda(\text{HA}^\uparrow); \\[2pt] &Log^\neg: \Lambda(\text{HA}^\uparrow) \rightarrow \Lambda(\mathtt{IPC}^\neg). \end{align*} $$

We will now prove that these two maps describe a dual isomorphism between the lattice of $\mathtt {DNA}$ -logics and the lattice of $\mathtt {DNA}$ -varieties. Our proof essentially relies on the standard isomorphism between the lattice of intermediate logics and the lattice of varieties of Heyting algebras. An alternative proof, making use of Lindenbaum–Tarski algebras for $\mathtt {DNA}$ -logics, was given in [Reference Quadrellaro41]. Let us introduce the following diagram:

where the four objects in the diagram are the following:

$$ \begin{align*} &\Lambda(\mathtt{IPC}) \text{ is the lattice of intermediate logics;} \\ &\Lambda(\text{HA}) \text{ is the lattice of varieties of Heyting algebras;} \\ &\Lambda(\mathtt{IPC}^\neg) \text{ is the lattice of }\mathtt{DNA}\text{-logics;} \\ &\Lambda(\text{HA}^\uparrow) \text{ is the lattice of }\mathtt{DNA}\text{-varieties.} \end{align*} $$

And the arrows are the following. Firstly, $(-)^\neg : \Lambda (\mathtt {IPC}) \rightarrow \Lambda (\mathtt {IPC}^\neg ) $ is the map we introduced above that assigns to every intermediate logic L its negative variant $L^\neg $ . Secondly, $(-)^\uparrow : \Lambda (\mathrm{HA}) \rightarrow \Lambda (\mathrm{HA}^\uparrow ) $ is the map that assigns to each variety of Heyting algebras $\mathcal {V}$ its negative closure $\mathcal {V}^\uparrow $ . The isomorphism $\Lambda (\mathtt {IPC}) \cong ^{op}\Lambda (\mathrm{HA}) $ is given by the standard duality for intermediate logics and varieties of Heyting algebras. The two maps of this bijection are $Log: \Lambda (\mathrm{HA}) \rightarrow \Lambda (\mathtt {IPC}) $ and $Var: \Lambda (\mathtt {IPC}) \rightarrow \Lambda (\mathrm{HA}) $ , which we have defined in the preliminaries. By using the fact that $\Lambda (\mathtt {IPC}) \cong ^{op}\Lambda (\mathrm{HA}) $ we show now that also $\Lambda (\mathtt {IPC}^\neg ) \cong ^{op} \Lambda (\mathrm{HA}^\uparrow ) $ holds. We proceed as follows. First we show that the diagram that we have described commutes, then we show that $Var^\neg $ and $Log^\neg $ are inverse maps of each other and finally we prove they are order-reversing homomorphisms between $ \Lambda (\mathtt {IPC}^\neg ) $ and $ \Lambda (\mathrm{HA}^\uparrow ) $ . Thus we will obtain a dual isomorphism $\Lambda (\mathtt {IPC}^\neg ) \cong ^{op}\Lambda (\mathrm{HA}^\uparrow ) $ .

3.5.1 Commutativity of the diagram

We first prove the two following propositions, thereby establishing that our diagram commutes.

Proposition 3.25. For every intermediate logic L we have $Var^{\neg }(L^{\neg })= Var(L)^\uparrow $ .

Proof. $(\subseteq )$ Consider any Heyting algebra $H\in Var^{\neg }(L^{\neg })$ . We have $H\vDash ^\neg L^{\neg }$ and so by Proposition 3.14 that $\langle H_\neg \rangle \vDash L $ . So we have $\langle H_\neg \rangle \in Var(L)$ and since $\langle H_\neg \rangle _\neg =H_\neg $ and $\langle H_\neg \rangle \preceq H$ also $H\in Var(L)^\uparrow $ . $(\supseteq )$ Consider any Heyting algebra $H\in Var(L)^\uparrow $ , then there is some $K\in Var(L)$ such that $K\preceq H$ and $H_{\neg }=K_{\neg }$ . Then $K\vDash L$ and by Lemma 3.12 we obtain $K\vDash ^\neg L^\neg $ , which entails $K\in Var^\neg (L^\neg )$ . Finally, since $\mathtt {DNA}$ -varieties are closed under core superalgebra, it follows that $H\in Var^\neg (L^\neg )$ .□

Proposition 3.26. For every variety $\mathcal {V}$ of Heyting algebras $Log^{\neg }(\mathcal {V}^\uparrow )= Log(\mathcal {V})^\neg $ .

Proof. We prove both directions by contraposition. $(\subseteq )$ Suppose $\varphi \notin Log(\mathcal {V})^\neg $ , then , so there is some Heyting algebra $H\in \mathcal {V}$ such that . By Proposition 3.11 this means that $H \nvDash ^\neg \varphi $ and so, since $H\in \mathcal {V} \subseteq \mathcal {V}^\uparrow $ , we also have $\varphi \notin Log^{\neg }(\mathcal {V}^\uparrow )$ . $(\supseteq )$ Suppose $\varphi \notin Log^{\neg }(\mathcal {V}^\uparrow )$ . It follows that there is some Heyting algebra $H\in \mathcal {V}^\uparrow $ such that $H\nvDash ^\neg \varphi $ , hence by Lemma 3.13 we have that $\langle H_\neg \rangle \nvDash ^\neg \varphi $ . It follows by Proposition 3.11 that . Now, since $H\in \mathcal {V}^\uparrow $ , we have for some $K\in \mathcal {V}$ that $K\preceq H$ and $K_\neg = H_\neg $ . Therefore $\langle H_\neg \rangle \preceq K$ and $\langle H _\neg \rangle \in \mathcal {V}$ . Finally, since we get that and hence $\varphi \notin Log(\mathcal {V})^\neg $ .

In particular, when $\mathcal {V}$ is itself a $\mathtt {DNA}$ -variety we obtain the following corollary.

Corollary 3.27. For every $\mathtt {DNA}$ -variety $\mathcal {X}$ we have $Log^{\neg }(\mathcal {X})= Log(\mathcal {X})^\neg $ .

3.5.2 Definability theorem and algebraic completeness

By relying on the commutativity result described above, we can now prove that the two maps $Var^\neg $ and $Log^\neg $ are inverse of one another. It is then easy to see that suitable versions of the definability theorem and algebraic completeness follow from this result.

Proposition 3.28. $Var^\neg \circ Log^\neg = 1_{\Lambda (\mathrm{HA}^\uparrow ) }$ .

Proof. For any $\mathtt {DNA}$ -variety $\mathcal {X}$ we have:

$$ \begin{align*} Var^\neg(Log^\neg (\mathcal{X})) &= Var^\neg(Log (\mathcal{X})^\neg) & \text{(by Corollary 3.27)}\\ &=Var(Log (\mathcal{X}))^\uparrow & \text{(by Proposition 3.25)}\\ &=\mathcal{X}^\uparrow & \text{(by standard duality)}\\ &=\mathcal{X}. & \end{align*} $$

And thus $Var^\neg \circ Log^\neg = 1_{\Lambda (\mathrm{HA}^\uparrow ) }$ .

Theorem 3.29 (Definability Theorem)

Every $\mathtt {DNA}$ -variety $\mathcal {X}$ is defined by its $\mathtt {DNA}$ -validities, i.e., for every Heyting algebra H,

$$ \begin{align*} H\in \mathcal{X} \Leftrightarrow H\vDash^\neg Log^\neg(\mathcal{X}). \end{align*} $$

We then have that every $\mathtt {DNA}$ -variety is $\mathtt {DNA}$ -definable. Moreover, by Proposition 3.23 we have that every $\mathtt {DNA}$ -definable class is also a $\mathtt {DNA}$ -variety, the following corollary also follows.

Corollary 3.30 (Birkhoff Theorem for $\mathtt {DNA}$ -Varieties)

A class of Heyting algebras $\mathcal {C}$ is a $\mathtt {DNA}$ -variety if and only if it is $\mathtt {DNA}$ -definable by some set of formulas.

The algebraic completeness of $\mathtt {DNA}$ -logics is proved as follows.

Proposition 3.31. $Log^\neg \circ Var^\neg = 1_{\Lambda (\mathtt {IPC}^\neg ) }$ .

Proof. For any $\mathtt {DNA}$ -logic $\Lambda $ such that $\Lambda =L^\neg $ we have:

$$ \begin{align*} Log^\neg(Var^\neg(\Lambda)) &= Log^\neg(Var^\neg(L^\neg)) &\\[-1pt] &=Log^\neg( Var(L)^\uparrow) & \text{(by Proposition 3.25)}\\[-1pt] &=Log(Var(L))^\neg & \text{(by Proposition 3.26)}\\[-1pt] &=L^\neg & \text{(by standard duality)}\\[-1pt] &=\Lambda. & \end{align*} $$

And thus $Log^\neg \circ Var^\neg = 1_{\Lambda (\mathtt {IPC}^\neg ) }$ .

Theorem 3.32 (Algebraic Completeness)

Every $\mathtt {DNA}$ -logic $\Lambda $ is complete with respect to its corresponding $\mathtt {DNA}$ -variety, i.e., for every $\varphi \in \mathcal {L}_P$ ,

$$ \begin{align*} \varphi\in \Lambda \Leftrightarrow Var^\neg(\Lambda)\vDash^\neg \varphi. \end{align*} $$

3.5.3 Dual isomorphism

Finally, by relying on the standard dual isomorphism $\Lambda (\mathrm{HA}) \cong ^{op}\Lambda (\mathtt {IPC}) $ and the commutative square above, it is easy to show that $Var^\neg $ and $Log^\neg $ are order-reversing homomorphisms that invert the lattice structure of $ \Lambda (\mathtt {IPC}^\neg ) $ and $ \Lambda (\mathrm{HA}^\uparrow ) $ .

Proposition 3.33. $Var^\neg $ is an order-reversing homomorphism.

Proof. It suffices to check that $Var^\neg $ inverts meet and join. Let $\Lambda _0,\Lambda _1$ be two $\mathtt {DNA}$ -logics such that $\Lambda _0=L_0^\neg $ and $\Lambda _1=L_1^\neg $ . The case for $\land $ is as follows:

$$ \begin{align*} Var^\neg(\Lambda_0\land \Lambda_1) &= Var^\neg(L_0^\neg\land L_1^\neg) & \text{ }\\[-1pt] &= Var^\neg((L_0\land L_1)^\neg) & \text{(by Proposition 3.5)}\\[-1pt] &= Var(L_0\land L_1)^\uparrow & \text{(by Proposition 3.25)} \\[-1pt] &= (Var(L_0) \lor Var (L_1) )^\uparrow & \text{(by standard duality)} \\[-1pt] & = Var(L_0)^\uparrow \lor Var (L_1)^\uparrow & \text{(by Proposition 3.20)} \\[-1pt] & =Var^\neg(L_0^\neg) \lor Var^\neg(L_1^\neg) & \text{(by Proposition 3.25)} \\[-1pt] & =Var^\neg(\Lambda_0) \lor Var^\neg(\Lambda_1). & \end{align*} $$

The case for $\lor $ is analogous.

Proposition 3.34 $Log^\neg $ is an order-reversing homomorphism.

Proof. It suffices to check that $Log^\neg $ inverts meet and join. Let $\mathcal {X}_0,\mathcal {X}_1$ be two $\mathtt {DNA}$ -varieties such that $\mathcal {X}_0=\mathcal {V}^\uparrow _0$ and $\mathcal {X}_1=\mathcal {V}^\uparrow _1$ . The case for $\land $ is as follows:

$$ \begin{align*} Log^\neg(\mathcal{X}_0\land \mathcal{X}_0) &=Log^\neg(\mathcal{V}^\uparrow_0\land \mathcal{V}^\uparrow_1) & \\[-1pt] &= Log^\neg( (\mathcal{V}_0\land \mathcal{V}_1)^\uparrow) & \text{(by Proposition 3.20)}\\[-1pt] & =Log(\mathcal{V}_0\land \mathcal{V}_1)^\neg & \text{(by Proposition 3.26)} \\[-1pt] &= (Log(\mathcal{V}_0)\lor Log(\mathcal{V}_1))^\neg & \text{(by standard duality)} \\[-1pt] & =Log(\mathcal{V}_0)^\neg\lor Log(\mathcal{V}_1)^\neg & \text{(by Proposition 3.5)} \\[-1pt] &= Log^\neg(\mathcal{V}^\uparrow_0)\lor Log^\neg(\mathcal{V}^\uparrow_1) & \text{(by Proposition 3.26)} \\[-1pt] &= Log^\neg(\mathcal{X}_0)\lor Log^\neg(\mathcal{X}_1). & \end{align*} $$

The case for $\lor $ is analogous.

It is a consequence of the previous results that $Var^\neg $ and $Log^\neg $ are two order-reversing homomorphisms between $\Lambda (\mathtt {IPC}^\neg ) $ and $\Lambda (\mathrm{HA}^\uparrow ) $ which are inverse of one another. The following duality theorem follows.

Theorem 3.35 (Duality)

The lattice of $\mathtt {DNA}$ -logics is dually isomorphic to the lattice of $\mathtt {DNA}$ -varieties of Heyting algebras, i.e., $\Lambda (\mathtt {IPC}^\neg ) \cong ^{op}\Lambda (\mathrm{HA}^\uparrow ) $ .

4.1 Connections to intermediate logics

In the previous section we have introduced $\mathtt {DNA}$ -logics as negative variants of intermediate logics under the map $(-)^\neg :\Lambda (\mathtt {IPC}) \rightarrow \Lambda (\mathtt {IPC}^\neg ) $ . Now we will investigate the relation between intermediate logics and $\mathtt {DNA}$ -logics in more detail. We will first show that the map $(-)^\neg $ which sends every intermediate logic to its negative variant is not injective. The following proposition was proved by Ciardelli in [Reference Ciardelli9, Lemma 5.2.20] and exemplifies how different intermediate logics can share the same negative variant. We recall that $\mathtt {KC}$ is the logic of the weak excluded middle, i.e., $ \mathtt {KC} = \mathtt {IPC}+ \neg p \lor \neg \neg p $ .

Proof. Suppose L is an intermediate logic such that $ \mathtt {KC} \subseteq L$ . One can show that for every formula $\varphi $ we have $\varphi \lor \neg \varphi \in L^\neg $ . We prove this by induction on the complexity of $\varphi $ . For the base case, suppose that $p \in \mathtt {AT}$ , then since $ \mathtt {KC} \subseteq L$ we have for all $p\in \mathtt {AT}$ that $\neg p \lor \neg \neg p \in L $ and therefore that $p \lor \neg p \in L^\neg $ . The induction steps follow easily by observing that for every formulas $\psi $ and $\chi $ we have

$$ \begin{align*} (\psi \vee \neg \psi) \land (\chi \vee \neg \chi) \to ( ( \psi\odot\chi ) \vee \neg (\psi \odot \chi) ) \in \mathtt{IPC} \qquad\text{for }\odot \in \{ \land, \vee, \to \}. \end{align*} $$

This shows that $L^\neg = \mathtt {IPC} + \varphi \lor \neg \varphi =\mathtt {CPC}$ .

Therefore, for intermediate logics $L_0,L_1$ such that $\mathtt {KC}\subseteq L_0,L_1$ and $L_0\neq L_1$ we have that $L_0^\neg =L_1^\neg =\mathtt {CPC}$ , hence $(-)^\neg $ is clearly not injective. Every $\mathtt {DNA}$ -logic $\Lambda $ thus determines a subset of the lattice $ \Lambda (\mathtt {IPC}) $ of those logics which have $\Lambda $ as their negative variant. It is easy to see that this subset is also a sublattice, since the map $(-)^\neg $ is a homomorphism. Similarly, since also $(-)^\uparrow $ is a homomorphism, we can also consider the sublattice of all varieties $\mathcal {V}$ in $ \Lambda (\mathrm{HA}) $ whose negative closure is $\mathcal {X}$ . We then define the preimage of a $\mathtt {DNA}$ -logic and the preimage of a $\mathtt {DNA}$ -variety as follows.

By the duality $\Lambda (\mathtt {IPC}) \cong ^{op}\Lambda (\mathrm{HA}) $ and the fact that the square introduced in Section 3.5 commutes, we then immediately have the following proposition.

The isomorphism $\mathcal {I}(\Lambda )\cong ^{op}\mathcal {I}(\mathcal {X})$ above is the restriction of the dual isomorphism $\Lambda (\mathtt {IPC}) \cong \Lambda (\mathrm{HA}) $ . We will now use this duality to characterize the two lattices $\mathcal {I}(\Lambda )$ and $\mathcal {I}(\mathcal {X})$ .

First, we prove that the preimage $\mathcal {I}(\Lambda )$ of some $\mathtt {DNA}$ -logic $\Lambda $ has a greatest element and we provide a characterisation of it. The following notion of schematic fragment of a $\mathtt {DNA}$ -logic was first introduced under the name of standardization in [Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti37, Section 3] and later considered by Ciardelli in [Reference Ciardelli9, Section 3.4].

Definition 4.4 (Schematic Fragment)

Let $\Lambda $ be a $\mathtt {DNA}$ -logic, we define its schematic fragment $Schm(\Lambda )$ as:

$Schm(\Lambda )$ is the set of all schematic formulas in $\Lambda $ , namely those formulas for which $\Lambda $ is closed under uniform substitution. One can easily check that $Schm(\Lambda )$ is an intermediate logic and that $Schm(\Lambda )^\neg = \Lambda $ . Moreover, the following proposition show that $Schm(\Lambda )$ is the maximal intermediate logic whose negative variant is $\Lambda $ .

The following theorem immediately follows by the previous propositions.

Therefore, the preimage $\mathcal {I}(\Lambda )$ of a $\mathtt {DNA}$ -logic $\Lambda $ has always a greatest element. By Theorem 3.35 we also obtain a dual characterisation of the corresponding $\mathtt {DNA}$ -varieties. In fact, we have that $Var(Schm(\Lambda ))$ is the least variety whose negative closure is $Var^\neg (\Lambda )$ . We define the map $least_V: \Lambda (\mathrm{HA}^\uparrow ) \rightarrow \Lambda (\mathrm{HA}) $ as follows:

$$ \begin{align*}least_V: \mathcal{X} \mapsto Var(Schm(Log^\neg(\mathcal{X}))) .\end{align*} $$

The following proposition follows easily.

Therefore, for every $\mathtt {DNA}$ -logic $\Lambda $ we have that $ Schm(\Lambda )$ is the greatest logic in $\mathcal {I}(\Lambda )$ and $ least_V (Var^\neg (\Lambda ))$ is the least variety in $\mathcal {I}(Var^\neg (\Lambda ))$ .

Similarly, one can show that the lattice $\mathcal {I}(\Lambda )$ has always a least element, which has so far been neglected in the literature. That this holds follows directly from the fact that for every $\mathtt {DNA}$ -variety $\mathcal {X}$ , there is a greatest variety whose negative closure is exactly $\mathcal {X}$ .

The following theorem immediately follows by the previous propositions and $\mathtt {DNA}$ -duality.

We thus define a map $least_L: \Lambda (\mathtt {IPC}^\neg ) \rightarrow \Lambda (\mathtt {IPC}) $ as follows:

$$ \begin{align*} least_L: \Lambda \mapsto Log( Var^\neg(\Lambda)). \end{align*} $$

The following proposition follows easily.

Therefore, it is the case that for every $\mathtt {DNA}$ -logic $\Lambda $ we have that $ least_L(\Lambda )$ is the smallest logic in $\mathcal {I}(\Lambda )$ and $ Var^\neg (\Lambda )$ is the greatest variety in $\mathcal {I}(Var^\neg (\Lambda ))$ .

By the former results above it thus follows that the sublattices $\mathcal {I}(\Lambda )$ and $\mathcal {I}(\mathcal {X})$ are bounded sublattices of $ \Lambda (\mathtt {IPC}) $ and $ \Lambda (\mathrm{HA}) $ . We introduce the following definitions.

In [Reference Miglioli, Moscato, Ornaghi, Quazza and Usberti37, Section 3] and [Reference Ciardelli9, Section 5.2] intermediate logics L such that $L=Schm(L^\neg )$ are called stable. The following proposition thus establishes that a logic is $\mathtt {DNA}$ -maximal iff it is stable. However, we will not use here this terminology, as the notion of stable logic has been employed e.g., in [Reference Ilin28] with a rather different meaning. The following proposition is an immediate consequence of our definition and the previous results.

4.2 Regular Heyting algebras

The previous characterisation of $\mathtt {DNA}$ -maximal and $\mathtt {DNA}$ -minimal logics is in a sense asymmetrical: we have a syntactic criterion for maximality and a semantic one for minimality. We are now after a semantic criterion for maximality. To this sake, we will now define regular Heyting algebras, which also play a major role in the context of $\mathtt {DNA}$ -logics in general.

These algebras have been introduced in [Reference Bezhanishvili, Grilletti, Holliday, Iemhoff, Moortgat and de Queiroz5] to provide an algebraic semantics to propositional inquisitive logic. A regular Heyting algebra is an algebra generated by its set $H_\neg $ of regular elements. For this reason we call regular Heyting algebras also regularly generated. Already in the previous section we have described some important properties of regular algebras in Lemma 3.13 and Proposition 3.14. Now we prove two further results showing that varieties $\mathcal {V}$ with the same negative closure $\mathcal {X}$ have the same collection of regular Heyting algebras. We first show the following proposition.

By the dual isomorphism $\Lambda (\mathtt {IPC}^\neg ) \cong ^{op}\Lambda (\mathrm{HA}^\uparrow ) $ we then obtain the following proposition.

We thereby have that all standard varieties whose negative closure is the same $\mathtt {DNA}$ -variety contain exactly the same regularly generated Heyting algebras. Interestingly, by Proposition 4.15 in order to check whether a regular Heyting algebra H validates an intermediate logic L, it is sufficient to check whether $H\ \mathtt {DNA}$ -validates $L^{\neg }$ (i.e., whether H validates $L^{\neg }$ under $\mathtt {DNA}$ -valuations).

Finally, we can strengthen the previous results and show that regular Heyting algebras provide a semantic characterisation of $\mathtt {DNA}$ -maximal logics. In [Reference Ciardelli, Abramsky, Kontinen, Väänänen and Vollmer10, Section 5.2] a sufficient criterion for $\mathtt {DNA}$ -maximality was given in the context of Kripke frames: Ciardelli established that if L is the logic of a class of finite, everywhere branching trees, then it is $\mathtt {DNA}$ -maximal. We propose here a criterion in terms of regular algebras which is both sufficient and necessary.

Proof. $(\Rightarrow )$ By Proposition 4.12 this is equivalent to the statement that if an intermediate logic L is such that $L=Log(\mathcal {C})$ , where $\mathcal {C}$ is a class of regularly generated Heyting algebras, then $L=Schm(L^\neg )$ . So, suppose that $\mathcal {C} $ is a class of regularly generated Heyting algebras, we need to show that $Log(\mathcal {C})= Schm(Log(\mathcal {C})^\neg )$ . Since $Schm(Log(\mathcal {C})^\neg )$ is $\mathtt {DNA}$ -maximal it follows that $Log(\mathcal {C})\subseteq Schm(Log(\mathcal {C})^\neg )$ , so that we only need to show that $Schm(Log(\mathcal {C})^\neg )\subseteq Log(\mathcal {C})$ . Now suppose by contraposition that $\varphi \notin Log(\mathcal {C}) $ , then we have that for some $H\in \mathcal {C}$ and for some valuation V, we have that $(H, V) \nvDash \varphi $ . Now, since H is regularly generated, every element $x_i\in H$ can be written out as a polynomial $\delta _i(\overline {y^{k}_{i}})$ of regular elements of H. Then we define the $\mathtt {DNA}$ -valuation $\mu : p^{k}_{i} \mapsto y^{k}_{i}$ so that we then get . Let $q_1,\dots ,q_l$ be a list of the distinct variables appearing in $\varphi $ , and define indexes $j_1,\dots ,j_l$ such that $V(q_i) = x_{j_i}$ . Moreover, define . We then have that , and consequently $(H, \mu ) \nvDash \psi $ . Since $H\in \mathcal {C}\subseteq \mathcal {C}^\uparrow $ , it follows that $\psi \notin Log^\neg ( \mathcal {C}^\uparrow ) = Log(\mathcal {C})^\neg $ . Finally, since $\psi $ is a substitution instance of $\varphi $ , it follows that $\varphi \notin Schm(Log(\mathcal {C})^\neg )$ .

( $\Leftarrow $ ) Suppose that L is a $\mathtt {DNA}$ -maximal logic and consider its corresponding variety $Var(L)$ . We let $Var_R(L)$ be the subclass of $Var(L)$ consisting of regular Heyting algebras only. Now, we have that $Var(L)\subseteq Var_R(L)^\uparrow $ , since for every $H\in Var(L)$ , we have $\langle H_\neg \rangle \in Var_R(L)$ , hence $H\in Var_R(L)^\uparrow $ . As obviously $Var_R(L)\subseteq Var(L)$ , it immediately follows that $Var(L)^\uparrow = Var_R(L)^\uparrow $ . We thus obtain:

$$ \begin{align*} L^\neg &= Log(Var(L))^\neg & \text{ } \\ &= Log^\neg(Var(L)^\uparrow) & \text{(by Proposition 3.26) }\\ &= Log^\neg(Var_R(L)^\uparrow) & \text{(by } Var(L)^\uparrow = Var_R(L)^\uparrow) \\ & = Log^\neg(\mathcal{V}(Var_R(L))^\uparrow) & \text{ (since }\mathcal{V}(Var_R(L))^\uparrow= Var_R(L)^\uparrow ) \\ & = Log(\mathcal{V}(Var_R(L)))^\neg & \text{(by Proposition 3.26)} \\ & = Log(Var_R(L))^\neg. \end{align*} $$

The last move is justified by the well-known fact that if $\mathcal {K}$ is a class of Heyting algebras and $\mathcal {V}(\mathcal {K})$ the variety generated by it, then $Log(\mathcal {K})=Log(\mathcal {V}(\mathcal {K}))$ (see, e.g., [Reference Chagrov and Zakharyaschev8, Chapter 7]). It follows by the $\mathtt {DNA}$ -maximality of L that $Log(Var_R(L))\subseteq L $ . Moreover, since we clearly have that $L \subseteq Log(Var_R(L)) $ it follows that $L=Log(Var_R(L)) $ , yielding that L is the logic of a class of regularly generated Heyting algebras.

Hence we can restate Proposition 4.12 in purely semantical terms.

4.3 Birkhoff’s theorem for $\mathtt {DNA}$ -varieties

We will prove in this section a version of Birkhoff’s theorem for $\mathtt {DNA}$ -varieties. While in the standard setting Birkhoff’s theorem states that varieties are generated by their subdirectly irreducible algebras, in our context we will prove that $\mathtt {DNA}$ -varieties are generated by their regular, subdirectly irreducible members. Interestingly, another method to generate $\mathtt {DNA}$ -varieties is by constructing the Lindenbaum–Tarski algebra of their corresponding $\mathtt {DNA}$ -logic, see for details [Reference Quadrellaro41, Section 3.3.2].

Recall that if $\mathcal {X}$ is a $\mathtt {DNA}$ -variety, then we say that $\mathcal {X}$ is generated by the class $\mathcal {C}\subseteq \mathcal {X}$ if $\mathcal {X}=\mathcal {X}(\mathcal {C})=\mathcal {V}(\mathcal {C})^\uparrow $ . We firstly prove the following useful theorem.

A first approximation of a Birkhoff’s theorem for $\mathtt {DNA}$ -varieties is given by the following result, stating that every $\mathtt {DNA}$ -variety $\mathcal {X}$ is generated by its collection of regular Heyting algebras. If $\mathcal {X}$ is a $\mathtt {DNA}$ -variety, then we denote by $\mathcal {X}_{R}$ its subclass of regular Heyting algebras.

We thus have, by the standard version of Birkhoff’s theorem, that every $\mathtt {DNA}$ -variety is generated by its subdirectly irreducible elements and, by the previous proposition, that every $\mathtt {DNA}$ -variety is generated by its regular elements. We can actually prove more, namely that $\mathtt {DNA}$ -varieties are generated by their regular, subdirectly irreducible elements. Now if $\mathcal {X}$ is a $\mathtt {DNA}$ -variety, we denote by $\mathcal {X}_{RSI}$ its subset of regular subdirectly irreducible Heyting algebras. We will thus show that for every $\mathtt {DNA}$ -variety we have $\mathcal {X}=\mathcal {X}(\mathcal {X}_{RSI})$ . Let us first recall the following result from the literature, originally due to Wronski [Reference Wronski45].

By using this fact we can prove Birkhoff theorem for $\mathtt {DNA}$ -varieties.

Proof. By the dual isomorphism between $\mathtt {DNA}$ -logics and $\mathtt {DNA}$ -varieties it suffices to show that $Log^\neg (\mathcal {X})=Log^\neg (\mathcal {X}(\mathcal {X}_{RSI})) $ , which is equivalent by Theorem 4.18 to $Log^\neg (\mathcal {X})=Log^\neg (\mathcal {X}_{RSI}) $ . The direction $Log^\neg (\mathcal {X})\subseteq Log^\neg (\mathcal {X}_{RSI}) $ follows immediately from the inclusion $\mathcal {X}_{RSI}\subseteq \mathcal {X}$ . It thus suffices to show that $Log^\neg (\mathcal {X}_{RSI}) \subseteq Log^\neg (\mathcal {X})$ .

Suppose by contraposition that $\varphi \notin Log^\neg (\mathcal {X}) $ , then for some $H\in \mathcal {X}$ and some $\mathtt {DNA}$ -valuation $V^\neg $ , we have that $(H,V^{\neg })\nvDash ^\neg \varphi $ and so, by reasoning as in the proof of Lemma 3.13, that $(\langle H_\neg \rangle, V^{\neg }) \nvDash ^\neg \varphi $ . Then, since

it follows by Lemma 4.20 that there is a subdirectly irreducible algebra C such that there is surjective homomorphism $h:\langle H_\neg \rangle \twoheadrightarrow C$ with $h(x )=s_C$ . Then, since homomorphisms preserve regular elements, the valuation $U^\neg = h\circ V^\neg $ is a $\mathtt {DNA}$ -valuation. Now let $p_0,\dots ,p_n$ be the variables in $\varphi $ , it follows by the properties of homomorphisms that:

From which it immediately follows that $ (C,U^\neg )\nvDash \varphi $ and so that $C\nvDash^\neg \varphi $ . Now, since $H\in \mathcal {X}$ , we have that $\langle H_\neg \rangle \in \mathcal {X}$ and so since $h:\langle H_\neg \rangle \twoheadrightarrow C$ also that $C\in \mathcal {X}$ . Moreover, we have that C is subdirectly irreducible and regular, as it is homomorphic image of $\langle H_\neg \rangle $ . Finally, this means that $C\in \mathcal {X}_{RSI} $ and so that $\varphi \notin Log^\neg (\mathcal {X}_{RSI}) $ , which proves our claim.

4.4 Locally tabular $\mathtt {DNA}$ -logics and $\mathtt {DNA}$ -varieties

The notions of local tabularity and local finiteness play an important role in the theory of intermediate logics and in universal algebra at large. Here we introduce a suitable notion of local finiteness for $\mathtt {DNA}$ -varieties and $\mathtt {DNA}$ -logics, which we will later employ in our study of inquisitive logic.

We say that a Heyting algebra H is $\mathtt {DNA}$ -finitely generated if there are finitely many elements $x_0,\dots ,x_n\in H_\neg $ such that $\langle x_0,\dots ,x_n \rangle = H$ . We then define locally finite $\mathtt {DNA}$ -varieties and locally tabular $\mathtt {DNA}$ -logics.

When the context makes it clear we then drop the prefix $\mathtt {DNA}$ and talk simply of local finiteness and local tabularity. The following proposition follows straightforwardly and allows us to relate the local finiteness of intermediate logics to the local finiteness of $\mathtt {DNA}$ -logics.

A property of $\mathtt {DNA}$ -logics which is closely connected to local finiteness is the finite model property (FMP). We introduce it as follows.

When the context makes it clear we drop the prefix $\mathtt {DNA}$ and simply talk of finite model property. The finite model property allows, for every formula $\varphi \notin \Lambda $ , to find a finite algebra H which validates $\Lambda $ and refutes $\varphi $ . Similarly to the case of local finiteness, the finite model property of an intermediate logic entails the finite model property of its negative variant.

If a $\mathtt {DNA}$ -variety has the finite model property we can further refine our version of Birkhoff theorem. We denote by $\mathcal {X}_{RFSI}$ the collection of finite, regular, subdirectly irreducible elements in $\mathcal {X}$ .