26
$\begingroup$

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?

$\endgroup$
30
$\begingroup$

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

$\endgroup$
  • $\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
21
$\begingroup$

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.\ \lambda h.\ \lambda (\mathtt{Left}\ x).\ g\ x \\\ f &= \lambda g.\ \lambda h.\ \lambda (\mathtt{Right}\ x).\ g\ 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.

$\endgroup$
  • 6
    $\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$ – Henning Makholm Mar 14 '12 at 20:02
  • 2
    $\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$ – Henning Makholm Mar 14 '12 at 22:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy