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

-

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