Do De Morgan's laws hold in propositional intuitionistic logic?

In Wikipedia page on intuitionistic logic, it is stated that excluded middle and double negation elimination are not axioms. Does this mean that De Morgan's laws, stated $$ \lnot (p \land q) \iff \lnot p \lor \lnot q \\ \lnot (p \lor q) \iff \lnot p \land \lnot q,$$ cannot be proven in propositional intuitionistic logic?

Solution 1:

The answer is "three quarters yes, one quarter no."

The one which is valid is the one with the disjunction inside the negation: $$\lnot p \land \lnot q \dashv \vdash \lnot (p \lor q)$$ For the other law, only one implication is valid: $$\lnot p \lor \lnot q \vdash \lnot (p \land q)$$

The proofs are left as an exercise to the reader.

To show that the last implication is invalid, we need to know some model theory for intuitionistic propositional logic. Recall that the rules of inference for intuitionistic propositional logic are sound when interpreted in a Heyting algebra: that is, if $p \vdash q$ in intuitionistic logic, and $[p]$ and $[q]$ are the corresponding interpretations in some Heyting algebra $\mathfrak{A}$, then $[p] \le [q]$.

Now, there is a rich and fruitful source of Heyting algebras in mathematics: the frame of open sets of any topological space is automatically a Heyting algebra, with the Heyting implication defined by $$(U \Rightarrow V) = \bigcup_{W \cap U \le V} W$$ Hence, the negation of $U$ is the interior of the complement of $U$. Now, consider $X = (0, 2)$, and let $U = (0, 1)$ and $V = (1, 2)$. Then, $\lnot U = (1, 2)$ and $\lnot V = (0, 1)$, so $\lnot U \cup \lnot V = X \setminus \{ 1 \}$. On the other hand, $U \cap V = \emptyset$, so $\lnot (U \cap V) = X$. Thus, $\lnot U \cup \lnot V \le \lnot (U \cap V)$, as expected, but $\lnot (U \cap V) \nleq \lnot U \cup \lnot V$. We conclude that $$\lnot (p \land q) \nvdash \lnot p \lor \lnot q$$

Solution 2:

It seems I managed to prove three implications using Curry-Howard isomorphism, but the fourth seems to be false.

$\neg(p \lor q) \Rightarrow \neg p \land \neg q$: $$ f = \lambda g.\ \langle \lambda x.\ g\ (\mathtt{Left}\ x), \lambda y.\ g\ (\mathtt{Right}\ y) \rangle $$ $\neg(p \lor q) \Leftarrow \neg p \land \neg q$:

\begin{align*} f &= \lambda (g, h).\ \lambda (\mathtt{Left}\ x).\ g\ x \\\ f &= \lambda (g, h).\ \lambda (\mathtt{Right}\ x).\ h\ x \end{align*}

$\neg(p \land q) \Leftarrow \neg p \lor \neg q$:

\begin{align*} f &= \lambda (\mathtt{Left}\ g).\ \lambda (x, y).\ g\ x \\\ f &= \lambda (\mathtt{Right}\ h).\ \lambda (x, y).\ h\ y \end{align*}

To prove $$\neg(p \land q) \Rightarrow \neg p \lor \neg q$$ I would need to transform a function $p \times q \to \alpha$ to one of the $p \to \alpha$ or $q \to \alpha$, but it is impossible to obtain two of them (both $p$ and $q$) at once. This is the intuition, but I would need something more for the proof.

Edit 1: Relevant link: http://ncatlab.org/nlab/show/de+Morgan+duality .

Edit 2: Here is a proof attempt (but I am not sure it is correct, if someone can tell, please do):

Let's assume that there exists a function $$F : \forall \alpha, p, q.\ (p \times q \to \alpha) \to (p \to \alpha) + (q \to \alpha).$$ Then, by the naturality of $F$ we have that it always returns $\mathtt{Left}$ or always returns $\mathtt{Right}$. Without the loss of generality let's assume that $F(f) = \mathtt{Left}\ g$ for any $f$. Then it follows that there exists $$ F_1 : \forall \alpha, p, q.\ (p \times q \to \alpha) \to (p \to \alpha). $$ However, $F_1(\lambda x.\ \lambda y.\ y) : \forall \alpha, \beta.\ \beta \to \alpha$ what means $\forall \beta.\ \beta \to \bot$ and that concludes the proof.

Solution 3:

Here's a finite example that basically reproduces what's happening in Zhen Lin's answer/counterexample:

Take a 4-element boolean lattice (labelled 1-2-3-4 above) and a "supertop" to it (labelled 5, above). The elements of the antichain of this lattice (2 and 3) are still pseudocomplements of each other, although no longer complements, which goes hand-in-hand with the "enriched" lattice not being Boolean anymore. (You can check that e.g. $2\land x \le1$ [still] has the greatest solution 3.) It's also easy to see that this lattice is still distributive (because it has exactly 5 elements that's an easy check), so a Heyting lattice because it's finite and distributive.

Now, the meet of the two elements of the antichain is still the bottom element, but because we added the new "supertop" 5, the psedocomplement of the bottom (labelled 1) is going to be 5 in this enriched lattice (because $1 \land x \le 1$ now admits a greater solution (5) than 4 which was the top of the Boolean lattice we started with, so $\neg (2 \land 3) = 5$ now, whereas the "supertop" does nothing for the join of the preudocomplents of the elements of the antichain, i.e. $\neg 2 \lor \neg 3= 3 \lor 2 = 4$.

This is para is not a proof, but note that this supertop doesn't affect the other De Mogran law: $\neg (2 \lor 3) = \neg 4 = 1$ and $\neg 2 \land \neg 3 = 3 \land 2 = 1$.

(Apologies for using 1 as the bottom element, I now this can be slightly confusing.)

The following part (also) isn't proof of anything, but it does give an additional intuition why only one of De Mogran's laws breaks in a Heyting algebra... and why I added a supertop above, instead of a superbottom, labelled 0 below:

Then, "nothing happens" as far De Morgan's laws are concerned because the definition of a pseudocomplement is relative to the (new) (super)bottom. So $\neg (2 \land 3) = \neg 1 = 0$ but $\neg 2 \lor \neg 3 = 0 \lor 0 = 0$ now as well because adding this superbottom (0) actually changed the pseudocomplements of both 2 and 3 (as well as that of 1).

Likewise this super-bottomed lattice fails to break the other De Morgan law: $\neg (2 \lor 3) = \neg 4 = 0$ and $\neg 2 \land \neg 3 = 0 \land 0 = 0$.