Double negation distributes over conjunction

Question

In Exercise I.1.11.(ii) of Johnstone's Stone Spaces, it is claimed that in any Heyting algebra, $$\lnot\lnot (a \land b) = \lnot\lnot a \land \lnot\lnot b.$$

It is easy to see one direction: Since $\lnot\lnot$ is order preserving, $\lnot\lnot(a\land b) \leq \lnot\lnot a$ and $\lnot\lnot (a\land b) \leq \lnot\lnot b$, so $\lnot\lnot (a\land b) \leq \lnot\lnot a \land \lnot\lnot b$.

But the reverse inequality is escaping me.

Answer 1

Recall that $\lnot x$ is an abbreviation of $x \to \bot$. Thus, $\lnot (a \land b)$ is equal to $a \to \lnot b$, which is less than or equal to $\lnot \lnot b \to \lnot a$; hence, $$\lnot \lnot a \land \lnot \lnot b \land \lnot (a \land b) \le \lnot \lnot a \land \lnot \lnot b \land (\lnot \lnot b \to \lnot a) \le \lnot \lnot a \land \lnot a \le \bot$$ and therefore $\lnot \lnot a \land \lnot \lnot b$ is less than or equal to $\lnot \lnot (a \land b)$, as required.

Answer 2

Here is a different way of looking at Zhen Lin's answer, which is more Hilbert-style and may be easier to follow for some. One useful metatheorem here is that an implication holds in every Heyting algebra if and only if the implication is provable in intuitionistic propositional logic, so we can just work in intuitionistic logic with any established proof system.

We have assumed $(a \to \bot)\to\bot$ and $(b\to\bot)\to\bot$. Assume $(a \land b) \to \bot$. Then we have

1. $(a \land b) \to \bot$, by assumption
2. $a \to (b \to \bot)$, by Currying
3. $a \to \bot$, assuming $(b \to \bot)\to \bot$
4. $\bot$, assuming $(a \to \bot) \to \bot$
5. $((a \land b) \to \bot) \to \bot$, applying the deduction theorem from 1 to 4

So $\lnot \lnot a \land \lnot\lnot b \to \lnot\lnot(a \land b)$.