Is there a version of intuitionistic logic, or at least some sort of logic, where ¬¬𝘈 → 𝘈 is kept but LEM is not?

Question

The Wikipedia article on double negation in logic says that intuitionistic logic does happen to keep ¬¬¬A → ¬A, as well as A → ¬¬A. I'm pretty confused by this, but I'll take it for granted for now. Still, by whatever means are used to preserve those conditionals, can one fine-tune a logic so that it has ¬¬A → A straight-up but doesn't validate LEM?

Peculiar "hill to die on" I suppose, but the denial of DNE has always been my core sticking point with intuitionistic logic. I appreciate that in mathematics, for example, there can be a sort of "double negation" that stays negative (as with imaginary numbers), but otherwise, my intuition of denying a denial, or logically negating a logical negation, is of positively asserting whichever atomic sentences are at stake.^💥💥 Compromising on LEM would be more intuitively plausible, in my eyes, if DNE could be preserved, and considering how many obscure variables there are in logical structures, I'd hope that there's some DNE-friendly, even if LEM-averse, option out there.

(I thought maybe this essay might cover such a possibility, but by scanning through it so far, it just seems to me that "adding DNE to intuitionistic logic" is taken to yield something isomorphic to classical logic, so who knows...)

---

^💥💥To be more precise and realistic: if I write down A, and then put ¬ down before it, I imagine this as if I am erasing A from the page (even if I am not erasing it literally). So by putting ¬ before itself, I imagine erasing the ¬ that is adjacent to the A, which leaves me with A by itself, then. But perhaps one might speak of two explosives next to a flimsy house, for example: detonating the bomb adjacent to the other bomb but not the house might, indeed, destroy the bomb that is adjacent to the house, but this might mean triggering the house-adjacent bomb, which will still go on to destroy the house. That might be a foolish metaphor but it's my best attempt so far to assign some physically intuitive significance to double negation (without elimination).

Answer 1

In one sense there is a straightforward answer to your question just by saying you can invent any logic you like. If you want to create a logic with ¬¬A → A as a theorem but not A ∨ ¬A then go ahead. The only issue is whether such a logic has a useful application and/or interesting semantics.

It is true that adding ¬¬A → A to intuitionistic logic yields classical logic, so such a logic could not be a superintuitionistic logic. In fact, I haven't tried to prove it, but I think such a logic would be contra-classical, and not just a sublogic of classical logic.

Using the BHK interpretation of intuitionism, negation can be understood as having a sense like "I can prove that there is no proof". So, asserting A means, "I can prove A", asserting ¬A means, "I can prove there is no proof of A", and asserting ¬¬A means, "I can prove that there is no proof that there is no proof of A". This helps to explain why ¬¬A is weaker than A and does not entail it. I may be able to demonstrate that there is no way to disprove A without actually proving A. But conversely, proving A is an excellent way to demonstrate that A cannot be disproved, so A → ¬¬A is quite acceptable.

Concerning your footnote on negation, there are many different ways to understand negation. In fact, although it seems like negation ought to be the simplest of the all the logical connectives to understand, as soon as you progress beyond logic 101, it turns out to be remarkably complex and entire books have been written about it. See, for example, the SEP article on negation, and Laurence Horn's, A Natural History of Negation (1989).

What you describe is sometimes called the subtraction or cancellation interpretation of negation. A proposition A says of A that it is true, and ¬A retracts this, leaving nothing. Peter Strawson used this understanding of negation to argue against the principle of explosion on the basis that a proposition together with its retraction simply cancels itself out and so nothing follows.

A more common interpretation of negation is that of complementation. A represents a collection of possibilities, or information states, or something, and ¬A represents the collection that is its complement.

Another option is to understand negation as a kind of modal operator whose job is to take a proposition and return its opposite, or its denial, or its rejection, in some sense of those terms. One important version of this account is the Routley Star, which is commonly used within relevance logics.

Answer 2

Bumble's post fails to answer your question. There is a very simple logic that anyone familiar with non-classical logic would know, called Kleene's 3-valued logic (3VL). 3VL satisfies DNE but not LEM. All the other rules of FOL (see here) also hold except for ⇒intro, which has to be changed from ( ( A ⊢ B ) ⊢ A⇒B ) to ( A∨¬A ; ( A ⊢ B ) ⊢ A⇒B ). And to be able to prove more we should strengthen ∨elim to ( A∨B ; ( A ⊢ C ) ; ( B ⊢ C ) ) ⊢ C ). We can actually easily extend the deductive system further to make it semantically complete for 3VL, by adding extra symbols and axioms to allow us to reason about the 3rd truth-value null. 3VL is not just an idea; it actually represents real digital logic circuits (with [true, false, null] captured by [pull-up, pull-down, open] respectively).