7
$\begingroup$

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

2 Answers 2

4

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

  • 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.2017-01-29
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.