Prove double negation of LEM in intuitionistic logic I understand that in intuitionistic logic, the law of excluded middle $P \lor \lnot P$ and double negation elimination $\lnot \lnot P \to P$ are not true in general (for every proposition $P$). However, I understand that $\lnot \lnot (P \lor \lnot P)$ and $P \to \lnot \lnot P$ are intuitionistically true in general. Is there an "intuitive" intuitionistic proof for these?
 A: In general, see Glivenko's result.
Your statements we can prove by proving theorems in the positive fragment of intuitionistic logic with a propositional variable $C$ and then letting $C=\bot$.

*

*The double negation introduction, $A\to \neg\neg A$, is modus ponens in the form $$A\to ((A\to C)\to C)$$

*Similarly, $\neg\neg(A\lor\neg A)$ is the special case of $$\big[\big(A\lor(A\to C)\big)\to C\big]\to C$$
To see why this holds, note that when assuming $\big(A\lor(A\to C)\big)\to C$, it functions as a valid premise for itself.

It's worth pointing out that this goes through in logics weaker than intuitionistic logic. We do not need the principle of explosion to show it - and indeed we don't even use a conjunction "$\land$".

A more pedestrian proof of the latter can be obtained as follows. First note that the following holds:
$$\Big[\big((A\lor B)\to C\big)\land \big(((A\to C)\land (B\to C))\to D\big)\big]\to D$$
To see why this holds, note that expression $(A\lor B)\to C$ says that both $A$ and $B$ imply $C$, which is exactly what the second expression demands to prove $D$. Now consider the special case $B=A\to\bot$ and $C=D=\bot$, then this reads
$$\neg\big[\neg (A\lor \neg A) \land \neg((\neg A) \land \neg (\neg A)) \big]$$
Here the second term is just the [non-contradiction principle] for $\neg A$ and this holds by modus ponens. We're again left with $\neg\neg (A\lor \neg A)$.
Note: The user in the comments points out a variant of this proof that effectively uses one of the valid De Morgan's laws and also again the noncontradiction principle.
This avoids the fourth propositional variable, $D$. It basically uses $(P\to\bot) = \neg P$ instead of $\neg(P\land \neg\bot) = \neg P$ that I used above.
A: For $P \to \lnot \lnot P$.
Note that negation introduction is "safe" also for Intuitionistic Logic.
According to the BHK interpretation we have:

There is no proof of $\bot$


A proof of $P\to Q$ is a function that converts a proof of $P$ into a proof of $Q$.

Assume we have a proof of $P$ and assume that we have a proof of $P \to \bot$. By Modus Ponens, we get a proof of $\bot$, that is impossible.
Thus, starting from a proof of $P$, we can build a function that converts a proof of $P \to \bot$ into a proof of $\bot$, i.e. into a proof of $(P \to \bot) \to \bot$.

For $¬¬(P∨¬P)$, we have to observe that Intuitionistic rejection of LEM means that LEM is not valid, not that it is false.
In IL we prove that $¬(P∨¬P)$ leads to a contradiction, and this amounts to a prove of $¬¬(P∨¬P)$.
The proof uses negation introduction and disjunction introduction, and both principles are intuitionistically safe.
From an Intuitionistic point of view (Brouwer, 1908), LEM amounts to the (unreliable) principle that every mathematical problem is decidable, while $¬¬(P∨¬P)$ amounts to asserting the principle that no absolutely unsolvable problem exists (Heyting, 1934).
A: here is an intuitive-ish intuitionistic proof of $¬¬(p \vee \neg p)$. Since $\neg x$ means $x \to \bot$, we need to show $\neg (p \vee \neg p) \vdash \bot$.  That means it's enough to show that $\neg (p \vee \neg p) \vdash \neg p$, since once we have $\neg p$ we can get $p \vee \neg p$ which together with $\neg (p \vee \neg p)$ gives $\bot$ as required.
To show $\neg(p\vee \neg p) \vdash \neg p$ it's enough to show $p, \neg(p\vee \neg p) \vdash \bot$. But that's easy: $p \vdash p \vee \neg p$, so $p, \neg (p \vee \neg p)\vdash p \vee \neg p$, and again recalling that $\neg x$ is $x \to \bot$ we get $p, (\neg(p\vee\neg p)) \vdash \bot$.
