 A well-known example of a logic with two negation operations is Heyting-Brouwer logic, also known as bi-intuitionistic logic, see Rauszer 1980, Goré 2000. In addition to intuitionistic negation, bi-intuitionistic logic contains a so-called co-negation that is in a sense dual to intuitionistic negation. In bi-intuitionistic logic \(\top\) is definable as \((p \rightarrow p)\) and \(\bot\) as \((p \coimp p)\) for some atomic formula \(p\). The intuitionistic negation \(\osim A\) of \(A\) is then definable as \((A \rightarrow \bot\)) and the co-negation \(- A\) of \(A\) as \((\top \coimp A)\). Whereas intuitionistic negation is a forward-looking impossibility operation with respect to the information order in compatibility frames, i.e.,  \[ {\cal M}, w \models \osim A \mbox{ iff } \forall u (w\leq u \mbox{ implies } {\cal M}, u \not \models A),\]  co-negation is a backward-looking unnecessity operator:  \[ {\cal M}, w \models - A \mbox{ iff } \exists u (u \leq w \mbox{ and } {\cal M}, u \not \models A).\] 