 As already remarked, the classification of unary connectives as negations may depend on the presence or absence of other logical operations. If the propositional language to which a negation operation is added contains only conjunction and disjunction (and atomic formulas), a natural starting point is to assume that one is dealing with a so-called distributive lattice logic (cf. Dunn and Zhou 2005). A distributive lattice logic is a single-antecedent and single-conclusion proof system in the language with only conjunction \(\wedge\) and disjunction \(\vee\). In addition to reflexivity and transitivity of the derivability relation \(\vdash\), the following inferential schemata are assumed: