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

2 Answers 2


There is a logic called bi-intuitionistic logic, which combines elements of intuitionistic and dual intuitionistic logics. It includes a strong intuitionistic implication connective and the corresponding strong negation of intuitionism, i.e. that ¬A is equivalent to A → ⊥. It also includes a dual of implication, which is a subtraction or exclusion connective and a corresponding weak negation ~A that is equivalent to ⊤ - A.

It is possible to interpret the strong negation ¬A as something like "A is provably false", because the truth of A implies absurdity. The weak negation ~A can be interpreted as something like "it is consistent to assume that A is false because we have no proof of A".

Bi-intuitionistic logic is still at the cutting edge of logic research, so I am not aware of any simple and accessible guides to it. A google search brings up a bunch of academic papers about its proof theory and Kripke semantics, but it is fairly heavy going. I hope this is better than nothing for you.


From the point of view of three-valued logic, it is possible to define three negations and connect them to concepts of modal logic. These have further connections to double negation and to the law of the Excluded Middle and the principle of Bivalence.

For a standard negation, The same double negation property of the classical two-valued negation holds, so ~~P = P. The LEM and Bivalence both hold or both fail.

There is a weak negation that can be understood as not necessarily or not provably) P. Double negation does not hold: By this deinition, ~~P -> P but not conversely. The principle of bivalence (p v ~P) holds, but noncontradiction (~ P & ~P) fails.

There is a strong negation that can be understood as not possibly P,necessarily not P, or provably not P). Double negation does not hold: By this definition, P -> ~~P but not conversely. Bivalence and noncontradiction both hold. It appears that intuitionism uses the strong negation.

EDIT: 2/27/2023 Corrected errors and misstatements.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .