27
$\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?

2 Answers 2

32

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$

  • 2
    @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 else2016-01-17
21

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.

  • 0
    @HenningMakholm I admit I do not understand the details of what you have written, but I know the idea and where to look further. Thank you!2012-03-14