This article provides an algebraic study of the propositional system $\mathtt {InqB}$ of inquisitive logic. We also investigate the wider class of $\mathtt {DNA}$-logics, which are negative variants of intermediate logics, and the corresponding algebraic structures, $\mathtt {DNA}$-varieties. We prove that the lattice of $\mathtt {DNA}$-logics is dually isomorphic to the lattice of $\mathtt {DNA}$-varieties. We characterise maximal and minimal intermediate logics with the same negative variant, and we prove a suitable version of Birkhoff’s classic variety theorems. We also introduce locally finite $\mathtt {DNA}$-varieties and show that these varieties are axiomatised by the analogues of Jankov formulas. Finally, we prove that the lattice of extensions of $\mathtt {InqB}$ is dually isomorphic to the ordinal $\omega +1$ and give an axiomatisation of these logics via Jankov $\mathtt {DNA}$-formulas. This shows that these extensions coincide with the so-called inquisitive hierarchy of [9].1

This paper contains a proof–theoretic account of unification in intermediate logics. It is shown that many existing results can be extended to fragments that at least contain implication and conjunction. For such fragments, the connection between valuations and most general unifiers is clarified, and it is shown how from the closure of a formula under the Visser rules a proof of the formula under a projective unifier can be obtained. This implies that in the logics considered, for the n-unification type to be finitary it suffices that the m-th Visser rule is admissible for a sufficiently large m. At the end of the paper it is shown how these results imply several well-known results from the literature.