Proof that regular elements of Heyting algebra form a Boolean algebra Let H be a Heyting algebra with join operation v.  It's a well-known fact that the regular elements of H form a Boolean algebra if v is redefined as (a, b) -> (a V b)**  However, I can't find this clearly proved anywhere.  I'm stuck because I can't see why, for p, q in H,(not necessarily regular) (p ^ q)** = p** ^ q**.  I think that, if I can prove that point, I can prove the whole result.  Thanks a lot for your help.
Paul Epstein
 A: I will address the specific question of how to show $\lnot\lnot(a\land b) = \lnot\lnot a\land \lnot\lnot b$ in a Heyting algebra.
Since $\lnot$ is order-reversing, $\lnot\lnot$ is order preserving. So $\lnot\lnot (a\land b) \leq \lnot\lnot a$ and $\lnot\lnot(a\land b) \leq \lnot\lnot b$. Hence: $$\lnot\lnot (a\land b) \leq \lnot\lnot a \land \lnot\lnot b.$$
In the other direction, to show $\lnot\lnot a \land \lnot\lnot b \leq \lnot\lnot(a\land b)$, it suffices to show: $$\lnot \lnot a \land \lnot \lnot b \land \lnot(a\land b)\leq \bot.$$
Note first that $\lnot(a\land b) \land (a \land b) = \bot$, so $\lnot(a\land b) \land a \leq \lnot b$, so $\lnot(a\land b) \leq a \rightarrow \lnot b$.
Note also that $x \land (x\rightarrow y) \land (y\rightarrow z) = x\land y \land (y\rightarrow z) = x \land y \land z \leq z$, so $(x\rightarrow y)\land (y\rightarrow z) \leq x\rightarrow z$.
Now:
\begin{align*}
\lnot \lnot a \land \lnot \lnot b \land \lnot(a\land b) &\leq \lnot\lnot a \land \lnot \lnot b \land (a \rightarrow \lnot b)\\
& = \lnot\lnot a \land (a\rightarrow \lnot b) \land (\lnot b \rightarrow \bot)\\
&\leq ((a\rightarrow \bot) \rightarrow \bot) \land (a\rightarrow \bot)\\
&\leq \bot,
\end{align*}
as desired.

For the more general question of how to show that the regular elements of a Heyting algebra form a Boolean algebra: I first learned this fact from Johnstone's book Stone Spaces,  where it appears (with a proof) as Proposition 1.13 on p. 10.
