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).