# 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$.]

• Are you sure about the question? it is not a theorem in Heyting Logic – Willemien Aug 29 '13 at 9:35
• @Willemien: It is exercise (i) in I.1.11 of "Stone Spaces" book – porton Aug 29 '13 at 9:43
• @Willemien: I confused $\vee$ and $\wedge$. Sorry – porton Aug 29 '13 at 9:44
• It seems that there is an error in this question: see groups.google.com/forum/#!topic/sci.math/Gqoyc_2IdYM – porton Aug 29 '13 at 11:04
• See here for the correctness of de Morgan's laws in intuitionistic logic. – Zhen Lin Aug 29 '13 at 11:19

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)$.

• I don't understand something: Do you use contradiction in intuitionistic propositional logic? – porton Aug 29 '13 at 11:32
• Sure. That's the only way to prove a negative. – Zhen Lin Aug 29 '13 at 12:38
• I'm finally confused. Could you clear? (especially whether the original formula is true in all Heyting algebras) – porton Aug 29 '13 at 12:43
• Yes, the original equation is true in all Heyting algebras. – Zhen Lin Aug 29 '13 at 12:45
• The definition of $\lnot a$ is $a \to \bot$, so by the deduction theorem, to prove $\lnot a$, it is enough to show that a contradiction follows from $a$. Now, once we have shown that two formulae are logically equivalent in propositional intuitionistic logic, it follows that the corresponding equation is true in all Heyting algebras. – Zhen Lin Aug 29 '13 at 12:55