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

However, I see how a fix for your answer.

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