Intuitionistic logic: double negation and LOEM removed?

Question

Why are double negation and the law of excluded middle excluded from the theory vs one of classical logic?

I see that the law of the excluded middle $\lnot(p \land \lnot p)$ requires double negation elimination when DeMorgans is applied. Therefore I think the rationale depends on double negation elimination. I searched and did not find a straightforward answer to this.

Answer 1

Try the entry on intuitionist logic in the Beginning Mathematical Logic study guide, particularly §8.3. This explains, after a fashion, the so-called BHK constructive interpretation of the connectives ... so see if that helps. You can download the guide from https://www.logicmatters.net/tyl.

Answer 2

Refer to this post for a Fitch-style system for classical FOL (first-order logic). IFOL (Intuitionistic FOL) corresponds to not treating propositions as having a truth-value, but rather as assertions of justification. "$A$." in IFOL means "we can justify $A$.", not "$A$ is true.". In IFOL, "$⇒$" is not classical implication; "$A⇒B.$" in IFOL means "We can convert any justification of $A$ into a justification of $B$.". And "$∧,∨$" in IFOL commute with "we can justify" (e.g. "$A∨B$." means "We can justify $A$ or we can justify $B$."). Also, in IFOL "$¬$" is not negation; "$¬A$" is instead defined as "$A⇒{⊥}$", which hence means "We can convert any justification of $A$ into a justification of contradiction.". (I shall not go into quantifiers and equality in this post.)

Now take a look again at the referenced rules for all the boolean operations in classical FOL, and check whether they are correct for the above meaning, where we read "If $A$:" in that system to mean "Given any justification of $A$:". You can check that the core rules are all correct except for ¬¬elim. Notice that ¬intro is correct by definition of "$¬$", and ¬elim is correct by that same definition plus ⇒elim. So in IFOL we keep all the core rules except ¬¬elim. Now this is not enough; there is one more rule that is correct for IFOL: $ \def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}} $

⊥elim
  $\fitch{⊥}{A.}$

This rule is redundant for classical FOL, but we need to add it after removing ¬¬elim in order to get a complete deductive system for IFOL. LEM is redundant in classical FOL, and is wrong for IFOL so of course we do not add it.

Of course there are other known semantics for IFOL, but the above semantics is surely the closest to what the original founders of intuitionistic logic were thinking. Note that this semantics is also kind of intuitionistic. We never once consider the question of whether we can justify something or not as having a truth-value. Rather, we make a statement only when we have actually justified it. The BHK interpretation has the same essence as this semantics. You can also take a look at Kripke semantics, which is in my view a more classical semantics, and not really what intuitionism is all about.