@ Joel - I don’t think your answer is correct. It is close. In classical logic we want \$$\neg \neg x = x \$$. I can think of Heyting algebras where this is violated. The most we can guarantee is \$$x \leq (x \to \bot) \to \bot \$$.

I'm with Keith E. Peterson on this one.

**Puzzle MD (Glivenko's Theorem).** Let \$$(A, \leq, \wedge, \vee, \bot, \top, \to)\$$ be a Heyting algebra. Define \$$\overline{\overline{A}} := \\{(a \to \bot) \to \bot \ :\ a \in A\\}\$$. Prove in the Heyting subalgebra \$$(\overline{\overline{A}}, \leq, \wedge, \vee, \bot, \top, \to)\$$ that \$$\sim x := x \to \bot\$$ is the left adjoint that Keith is talking about in his puzzle.