Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question

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

share|cite|improve this answer
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

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.