 The correspondence theory of negation as impossibility and negation as unnecessity in a language with \(\top\), \(\bot\), \(\wedge\), and \(\vee\) has been developed in Lahav, Marcos, and Zohar 2017, using methods of the theory of basic sequent systems from Lahav and Avron 2013 in order to obtain various cut-admissibility results. Moreover, Lahav and his co-authors also consider the addition of so-called adjustment operators and the definability of classical negation.