Is there a system of logic which denies DNI?

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

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

For all statements A, B, C,

if

A,B |- C

then

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.