My main concern is to separate different forms of logic. I am hoping to use negation as a way to do that.
In the abstract to "Web Rules Need Two Kinds of Negation", Gerd Wagner writes
... there are two kinds of negation: a weak negation expressing non-truth, and a strong negation expressing explicit falsity.
I don't know what this difference is well enough to spot it in a natural deduction proof. I imagine the negation of a proposition P for classical logic is always strong negation. For the intuitionist it may always be a weak negation. However, I am not sure if that is the case.
Underlying these concerns is the title question of just what this difference is so I can make use of it.
Wagner, G. Web Rules Need Two Kinds of Negation. In F. Bry, N. Henze and J. Maluszynski (Eds.), Principles and Practice of Semantic Web Reasoning Proc. of the 1st International Workshop, PPSW3 '03. Springer-Verlag LNCS 2901, 2003. Retrieved from https://oxygen.informatik.tu-cottbus.de/publications/wagner/WebRules2Neg.pdf