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?


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

  • $\begingroup$ What is $\le$ in $W\cap U\le V$? $\endgroup$
    – celtschk
    Jul 13 '13 at 7:07
  • $\begingroup$ You can read it as $\subseteq$. $\endgroup$
    – Zhen Lin
    Jul 13 '13 at 11:10
  • 2
    $\begingroup$ Do you mean that as "it's another way to write $\subseteq$", or as "while it is something different, in this context the differences are not important"? $\endgroup$
    – celtschk
    Jul 13 '13 at 21:15
  • 2
    $\begingroup$ @celtschk We're interpreting the lattice of open sets as a Heyting algebra. The algebra has a relation $\le$, which we interpret in this case as $\subseteq$. So here they mean the same thing, but there are Heyting algebras where $\le$ means something else $\endgroup$
    – fhyve
    Jan 17 '16 at 8:11
  • $\begingroup$ Really nice to see this example here. $\endgroup$ Mar 2 '20 at 11:00

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.

  • 8
    $\begingroup$ Incidentally, we can make the last one if we have call/cc (i.e. classical logic). First save the continuation and return a $p\to\alpha$. Then, if anyone ever calls that, remember the $p$ and use the saved continuation to go back in time and return a $q\to\alpha$ instead. When the latter return value is called, you have both a $p$ and a $q$ and can therefore use the original function to get an $\alpha$. $\endgroup$ Mar 14 '12 at 20:02
  • 3
    $\begingroup$ @Henning: +1 for call/cc and time travel! $\endgroup$
    – Zhen Lin
    Mar 14 '12 at 20:17
  • 1
    $\begingroup$ @HenningMakholm If we have call/cc we have $p \lor \neg p$... But yes, you are correct, I like this idea very much and I am happy I am not alone here ;-) Could you look at my proof attempt? $\endgroup$
    – dtldarek
    Mar 14 '12 at 20:25
  • $\begingroup$ @dtldarek: I'm afraid I don't understand what you've written. Are you trying to show that there can't be a proof of $\lnot (p \land q) \vdash \lnot p \lor \lnot q$? This can't be achieved without choosing a specific model, i.e. a specific cartesian closed category. Because there are certainly cartesian closed categories in which there is a function of type $(p \times q \to \alpha) \to (p \to \alpha) + (q \to \alpha)$... $\endgroup$
    – Zhen Lin
    Mar 14 '12 at 20:56
  • 3
    $\begingroup$ For a syntactic proof that $\neg(p\land q)\not\vdash\neg p\lor\neg q$, I think the simplest avenue might be to use a Gentzen-style proof system, such that if there's a derivation of $\neg(p\land q)\vdash\neg p\lor\neg q$, it must have a cut-free proof where every sentence everywhere is a subsentence of the conclusion. Then, since $\neg p\lor \neg q$ is never a proper subformula of anything, the bottommost right rule must conclude $\neg p\lor \neg q$ from either $\neg p$ or $\neg q$, and the premise for that wouldn't even be a classically valid sequent. $\endgroup$ Mar 14 '12 at 22:33

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

enter image description here

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:

enter image description here

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

  • $\begingroup$ Additionally, in a Heyting algebra, $\neg(a \land b) = \neg a \lor \neg b$ is equivalent to the somewhat simpler condition $\neg a \lor \neg\neg a = \top$. These are usually called Stone algebras; in my answer above the first lattice example is not Stone, but the 2nd one is. $\endgroup$
    – Fizz
    Mar 19 at 5:53
  • $\begingroup$ Also, since 2-to-4 element lattices are all Stone (i.e. Boolean and/or chains), I think the 5-element "inverted kite" above is the minimal counterexample for De Morgan failure in a Heyting algebra. $\endgroup$
    – Fizz
    Mar 19 at 8:03

Your Answer
