7

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

Dorry
  • 71
  • 2

2 Answers2

5

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

Kevin Carlson
  • 52,457
  • 4
  • 59
  • 113
martini
  • 84,101
  • I think you were missing a negation in the original version. – Kevin Carlson Oct 21 '12 at 07:52
  • @KevinCarlson Thx. – martini Oct 21 '12 at 07: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
  • 1
    I still found this answer useful, even though it doesn't address your specific question, because it proves that: if the axiom ¬¬y≅y holds (for every y), then the law of excluded middle holds. – David Spivak Jan 29 '17 at 13:10
1

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

HA

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

Daniil
  • 1,157