# Proving that double negation elimination implies law of excluded middle, in Heyting algebra

Let a Heyting algebra $H$ be given. Suppose $x \in H$.

Prove the following: if $\neg \neg x \cong x$, then $x \vee \neg x \cong \top$.

(To be precise: here $\top$ means the (essentially unique) top element of the lattice, and negation $\neg$ is defined as usual in a Heyting algebra, namely $\neg x$ is $x \Rightarrow \bot$. Here $\bot$ is the bottom element of the lattice, of course again essentially unique.)

I tried everything, nothing seems to work. (NB: I managed to prove the converse; my argument was, however, not directly 'reversable'.)

-

The converse does not really follow. Consider, as a counter example, the following Heyting algebra

$\neg a = b$ and $\neg \neg a = \neg b = a$. Thus, $\neg \neg a \to a$. However, $\neg a \vee a = b \vee a \neq 1$

Maybe you have wanted to prove something a bit different. Given a Heyting algebra $H$ s.t. for all formulae $\varphi$, such that $\neg\neg \varphi \to \varphi$ in $H$, we have $\varphi \vee \neg \varphi$ in $H$. For that you can use the proof method described in martini's post.

-

As $\neg \neg y \cong y$ for $y \in H$, it suffices to prove $\neg\neg(x \vee \neg x) \cong \top$. Now $\neg(x \vee \neg x) \cong \neg x \land \neg \neg x \cong x\land \neg x \cong \bot$ (as the used de Morgan's law holds in Heyting algebras). And finally $\neg \bot \cong \top$.

-
I think you were missing a negation in the original version. – Kevin Carlson Oct 21 '12 at 7:52
@KevinCarlson Thx. – martini Oct 21 '12 at 7:56
This proof seems wrong to me. It is given that $\neg \neg x \cong x$, but who said that $\neg \neg y \cong y$ for all $y \in H$!? (Edit: I cannot respond directly to martini's post. I don't know why.) I have never said this. I.e. I do not agree that "it suffices to prove that $\neg \neg (x \vee \neg x ) \cong \top$". Can somebody confirm this? – Dorry Oct 21 '12 at 12:35
@Dorry I am probably very late to the party, but you are absolutely right. The proof in question is simply wrong and does not work. – Daniil Jul 22 '15 at 17:13