Prove double negation of LEM in intuitionistic logic

Question

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?

Answer 1

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

Answer 2

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, assume $\big(A\lor(A\to C)\big)\to C$ and note that it functions as a valid premise for itself: Just the left side of "$\lor$" says $A$ implies $C$, meaning we conclude $A\to C$. Now using this for the right side of "$\lor$" we conclude $C$.

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$", which I'll make use of in the motivation part.

---

Consider modus ponens in the curried form $(B\land (B\to C))\to C$. Again with $C=\bot$, we obtain the valid non-contradiction principle $\neg(B\land \neg B)$. Consider the more particular $\neg(\neg A\land \neg \neg A)$, saying that the proposition $B=\neg A$ cannot be witnessed and rejected at the same time. Three of the four De Morgan's laws are intuitionistically valid. If you're taking the latter for granted, the double-negated excluded middle $\neg\neg(A\land \neg A)$ is also proven after pulling the negation through the bracket. And in a consistent system, you may also read $A\to\neg\neg A$ as expressing that if $A$ has been established, then it cannot anymore be rejected.

---

For a pedestrian proof, 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 its validity, 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$. The special case $B=A\to\bot$ and $C=D=\bot$ of this reads $$\neg\big[\neg (A\lor \neg A) \land \neg((\neg A) \land \neg (\neg A)) \big]$$ We recognize the established the non-contradiction principle on the right and are thus 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 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.

Answer 3

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