 After examining the interplay between negation, implication, and co-implication, recent work on negation as a modal operator in display calculi, a generalization of Gentzen’s seuqent calculi, can be considered. There the above notions of negation as impossibility and unnecessity can be captured by structural sequent rules, see the supplement  Substructural negations: negation as a modal operator in display calculi.