From what I know, the law of double negation is often simplified as p <=> ~~p. Intuitionist logic splits the biconditional into DNI and DNE. DNI: p -> ~~p DNE: ~~p -> p and denies DNE while affirming DNI. My question is whether there is a similar system which does the opposite, i.e., denies DNI while affirming DNE?

3 Answers 3


Yes there is. As you say, intuitionistic logic has DNI but not DNE. There are also dual-intuitionistic logics whose connectives operate in a fashion that is dual to those of intuitionistic logic. Dual-intuionistic logic has DNE but not DNI. Intuitionistic logic includes the law of non-contradiction (LNC) but not the law of exlcuded middle (LEM) so it is paracomplete. Dual-intuitionistic logic includes LEM but not LNC, so it is paraconsistent.

Here are a couple of references on dual-intuitionistic logic.

Yaroslav Shramko, "Dual Intuitionistic Logic and a Variety of Negations: The Logic of Scientific Research". Studia Logica 80, pp. 347-367, (2005)

Igor Urbas "Dual-Intuitionistic Logic". Notre Dame Journal of Formal Logic 37(3), pp. 440-451, (1996).

There is also another question on the Philosophy Stack Exchange about dual-intutionistic logic and some of the answers there contain references.


Just as Intuitionism can be translated to classical S4 modal logic, there is a logic based off of classical GL modal logic developed by Albert Visser called Formal Propositional Logic (FPL) which does not validate DNI. In general, if you take the Gödel-Tarski-McKinsey translation, but remove that the relation between states is reflexive, then the resulting propositional logic won’t validate DNI. This is the result of that (P&~P)⊭⊥ without reflexivity.


My answer is just a remark to prove that what you call DNI follows from very basic logical assumptions.

Let us write

A1,...,An |- B

to say that B is provable from the assumptions A1,...,An. A theorem is a statement A that is provable from no assumptions; to say that A is a theorem, we write

nothing |- A.

Consider a proof system where the following rules hold:

  1. Modus ponens

For all statements A, B,

A, A -> B |- B.

  1. ??? (I don't know the name of this rule)

For all statements A, B, C,


A,B |- C


nothing |- A -> (B -> C)

Then, in this proof system, we have

|- A -> ((A -> B) -> B).

Moreover, the usual definition of ~A is just A -> FALSE.

Therefore, DNI is a theorem in such a proof system.

  • Your rule 2 follows from two right implication introduction steps! It’s more commonly phrased as “given An U {B} |- C, then An |- B-> C”. This works because -> is the material implication, but fails in some logics with a stronger conditional.
    – Paul Ross
    Commented Jun 26, 2023 at 6:52

You must log in to answer this question.

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