Equivalence between middle excluded law and double negation elimination in Heyting algebra

Question

It's well-know that in intuitionistic logic, middle excluded law and double negation elimination are equivalent.

For example, in Johnstone - Topo theory, I read that, in a Heyting algebra, $p\vee\neg p=\top$ holds if and only if $\neg\neg p=p$ for all elements $p$.

In particular, it's easy to prove $(p\vee\neg p)\leq(\neg\neg p\Rightarrow p)$: for we have $p\Rightarrow(\neg\neg p\Rightarrow p)=(p\wedge\neg\neg p)\Rightarrow p=\top$ and $\neg p\Rightarrow (\neg\neg p\Rightarrow p)=(\neg p\wedge\neg\neg p)\Rightarrow\perp\Rightarrow p=\top$, consequently, $(p\vee\neg p)\Rightarrow(\neg\neg p\Rightarrow p)=\top$.

On the other hand, I can't prove inverse inclusion $(\neg\neg p\Rightarrow p)\leq (p\vee\neg p)$.

Thus my question is:

In a Heyting algebra, does $(\neg\neg p\Rightarrow p)\leq (p\vee\neg p)$ holds?

The proof that I founded here don't satisfy me because it proves only the inference rule $(\neg\neg p\Rightarrow p)\vdash (p\vee\neg p)$.

Answer 1

As you apparently already know, if $((\neg\neg p)\implies p)=\top$ for all $p$ in some Heyting algebra, then also $(p\lor\neg p)=\top$ for all $p$ in that Heyting algebra. Nevertheless, if $((\neg\neg p)\implies p)=\top$ for a particular $p$ in a Heyting algebra, it does not follow that $(p\lor\neg p)=\top$ for that same $p$.

For example, $((\neg\neg p)\implies p)=\top$ is true whenever $p$ is of the form $\neg q$, because $(\neg\neg\neg q)\implies(\neg q)$ is intuitionistically valid. But it is not intuitionistically valid that $(\neg q)\lor(\neg\neg q)$.

A simple explicit counterexample is the Heyting algebra of open subsets of the real line. Let $p$ be the open half-line $(0,\infty)$. The negation $\neg p$, i.e., the largest open set disjoint from $p$, is the open half-line $(-\infty,0)$, and $\neg\neg p$ equals $p$. So $((\neg\neg p)\implies p)=\top$, but $(p\lor\neg p)=\mathbb R-\{0\}\neq\top$.

Answer 2

We cannot prove in intuitionsitc logic :

$\vdash (\lnot \lnot p \Rightarrow p) \Leftrightarrow (p \lor \lnot p)$.

---

As you said, we can prove :

$(p \lor \lnot p) \Rightarrow (\lnot \lnot p \Rightarrow p)$.

For the other "direction", we can prove only a "negative version" of the theorem.

References are to Intuitionistic logic and to Heyting algebra.

1) $(\lnot \lnot p \Rightarrow p) \le (\lnot p \Rightarrow \lnot \lnot \lnot p)$ --- the law : $a \Rightarrow b \le \lnot b \Rightarrow \lnot a$ is intuitionistically valid

2) $(\lnot p \Rightarrow \lnot \lnot \lnot p) \le (\lnot p \Rightarrow \lnot p)$ --- the law : $\lnot \lnot \lnot a = \lnot a$ is intuitionistically valid

3) $= \lnot (\lnot p \land p)$ --- the law : $(a \Rightarrow \lnot b) = \lnot (a \land b)$ is intuitionistically valid

4) $= \lnot \lnot (\lnot \lnot p \lor \lnot p)$ --- weak De Morgan's law : $\lnot (x \land y) = \lnot \lnot (\lnot x \lor \lnot y)$ holds in HA

Conclusion :

$(\lnot \lnot p \Rightarrow p) \le \lnot \lnot (\lnot \lnot p \lor \lnot p)$

i.e.

$\vdash (\lnot \lnot p \Rightarrow p) \Rightarrow \lnot \lnot (\lnot \lnot p \lor \lnot p)$.

---

Addendum

Here we have a proof with sequent calculus LK of :

$\vdash (\lnot \lnot P \supset P) \supset (P \lor \lnot P)$.

i) left thread :

$${P \Rightarrow P \over P \Rightarrow P \lor \lnot P } \, \lor\text{-right} \,$$

ii) right thread :

$${P \Rightarrow P \over P, \lnot P \Rightarrow } \, \lnot\text{-left}$$

$${\over \lnot P \Rightarrow \lnot P } \, \lnot\text{-right}$$

$${\over \lnot P \Rightarrow P \lor \lnot P } \, \lor\text{-right}$$

$${\over \Rightarrow P \lor \lnot P, \lnot \lnot P} \, \lnot\text{-right}$$

Note. The last step is not intuitionistically valid because violates the restriction that :

a sequent in LJ is of the form $\Gamma \Rightarrow \Delta$, where $\Delta$ consists of at most one formula.

iii) conclusion

Now we "join" the two threads :

$${P \Rightarrow P \lor \lnot P \quad \quad \Rightarrow P \lor \lnot P, \lnot \lnot P \over \lnot \lnot P \supset P \Rightarrow P \lor \lnot P }\, \supset\text{-left}$$

$${\over \Rightarrow (\lnot \lnot P \supset P) \supset (P \lor \lnot P) }\, \supset\text{-right}$$

Regarding the impossibility of finding a proof of it in LJ, see Jan von Plato, Elements of Logical Reasoning (2013), page 82 :

Given $A \lor \lnot A$, if $\lnot \lnot A$ is assumed, $A$ follows and therefore the implication $\lnot \lnot A \supset A$ follows from $A \lor \lnot A$. An easy proof search in intuitionistic sequent calculus gives a formal derivation for :

$A \lor \lnot A \supset (\lnot \lnot A \supset A)$.

A similar proof search for the converse fails, for there is no derivation of :

$(\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.

[...]

The overall situation is that if $\vdash \lnot \lnot A \supset A$, then $\vdash A \lor \lnot A$, but not $\vdash (\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.