Observations

In Boolean logic, ¬(A∧B) ≡ (¬A∨¬B); in intuitionism - no so fast.

In intuitionism you can only prove that (¬A∨¬B) ⊢ ¬(A∧B) , but not the opposite way.

Example? Use the semantics trick from Wikipedia.

Namely, take the partial order of open subsets of the set of real numbers between 0 and 1, [0,1]. It is a Heyting algebra (for an obvious reason not worth discussing here. Negation is defined like this: take a set complement, and take its interior (the largest open subset). So, e.g. for [(a,b)], the complement is [0,a)∪(b,1]

Now take A=[0,0.5) and B=(0.5,1]. These two sets don't intersect, so their conjunction is ⊥, and ¬(A∧B) is ⊤.

Actually, A = ¬B and B = ¬A.

And their disjunction, A∨B, is [0,0.5)∪(0.5,1], which is not ⊤.

Q.E.D. We have an example where this equivalence from Boolean logic, ¬(A∧B) ≡ (¬A∨¬B), does not hold. Profit!

If somebody can show me an example from a finite lattice, that would be very cool. The example I had in my book is just wrong.