A de-Morgan law for Heyting lattices Please show that $\lnot(a\vee b) = \lnot a\wedge \lnot b$ for any Heyting algebra. [Corrected: exchanged $\vee$ and $\wedge$.]
(I prefer to receive the answer is dual terminology, that is about co-Heyting algebras.)
 A: I will prove that the corresponding formulae are logically equivalent in intuitionistic propositional logic. 
First, suppose $\lnot (a \lor b)$; we wish to prove $\lnot a \land \lnot b$. Assume $a$. Then $a \lor b$, which is a contradiction, so we discharge $a$ and deduce $\lnot a$. Similarly, we may deduce $\lnot b$. Thus $\lnot a \land \lnot b$.
Conversely, suppose $\lnot a \land \lnot b$. Assume $a \lor b$. Since $\lnot a$ and $\lnot b$, we use $\lor$-elimination to deduce that $a \lor b \to \bot$, i.e. $\lnot (a \lor b)$.

Here is the proof spelled out in the language of Heyting algebras. To show that $x = y$ in a poset, it is enough to show that both $x \le y$ and $y \le x$.
First, notice that $a \land \lnot (a \lor b) \le (a \lor b) \land \lnot (a \lor b) \le \bot$, so $a \land \lnot (a \lor b) \le \bot$, so $\lnot (a \lor b) \le \lnot a$. Similarly, $\lnot (a \lor b) \le \lnot b$. It follows that $\lnot (a \lor b) \le \lnot a \land \lnot b$.
On the other hand, $\lnot a \land \lnot b \land (a \lor b) = (\lnot a \land \lnot b \land a) \lor (\lnot a \land \lnot b \land b)$ by the distributive law, and $\lnot a \land \lnot b \land a = \lnot a \land \lnot b \land b = \bot$, so $\lnot a \land \lnot b \land (a \lor b) = \bot$. Thus, $\lnot a \land \lnot b \le \lnot (a \lor b)$.
