# Does double negation distribute over disjunction intuitionistically?

Does the following equivalence

$$\lnot \lnot (A \lor B) \leftrightarrow (\lnot \lnot A \lor \lnot \lnot B)$$

hold in propositional intuitionistic logic? And in propositional minimal logic? (In propositional classical logic this is obvious since $A \leftrightarrow \lnot\lnot A$ is classically provable.)

Actually I have a proof that $(\lnot \lnot A \lor \lnot \lnot B) \to \lnot \lnot (A \lor B)$ holds in propositional minimal logic, so I'm interested in the converse implication:

$$\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$$

If it is minimally or/and intuitionistically provable, I would like a (reference to a) direct proof in natural deduction-style.

• Can you post axiom sets/rules of inference here? I know I can find intuitionistic axioms which seem standard, but I'm not so sure about minimal logic. – Doug Spoonwood Nov 10 '15 at 16:13
• @DougSpoonwood: The list of axioms for (first-order and then, in particular, propositional) intuitionistic logic is available for example here. The list of axioms for (first-order and then, in particular, propositional) minimal logic is just obtained by the list above removing the axiom $\lnot A \to (A \to B)$ (ex-falso-quodlibet). However, I would prefer a direct proof in natural deduction-style (if any), if it is possible. – Taroccoesbrocco Nov 10 '15 at 16:27
• @Taroccoesbrocco A good rule of thumb is that to prove a disjunction intuitionistically, you'll need to be able to prove one of its disjuncts. (I'm excluding cases like $A \to (B \lor C)$ (where you could try to prove $A$ first, and then use conditional elimination) and $A \land (B \lor C)$ (where you could use conjunction elimination).) From the left side, I don't think that you can infer either $\lnot\lnot A$ or $\lnot\lnot B$, so I don't think you'll be able to get the right side. You can get from the right side to the left, though (as you've shown). – Joshua Taylor Nov 10 '15 at 17:35

$\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$ is not intuitionistically acceptable. One way of seeing this is by considering the Heyting algebra whose elements are the open subsets of the unit interval $[0, 1] \subseteq \Bbb{R}$, with $A \lor B = A \cup B$, $A \to B = \mathsf{int}(A^c\cup B)$ and $\bot = \emptyset$ (see https://en.wikipedia.org/wiki/Heyting_algebra). In this Heyting algebra, $\lnot\lnot A$ is the interior of the closure of $A$ and $A \to B$ is $\top$ iff $A \subseteq B$. Hence if $A = [0, 1/2)$ and $B = (1/2, 1]$, $\lnot \lnot (A \lor B) = [0, 1]$ while $\lnot \lnot A \lor \lnot \lnot B = [0, 1] \mathop{\backslash} \{1/2\}$ and $\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$ is not $\top$.
• Just in case the OP is more familiar with Kripke models than with topological ones, here's a Kripke counterexample. The underlying partially ordered set consists of $a,b,c$ with $c<a$ and $c<b$ while $a$ and $b$ are incomparable. Let $A$ be true only at $a$ and let $B$ be true only at $b$. Then $\neg\neg A$ and $\neg\neg B$ are also true only at $a$ and $b$, respectively, so their disjunction is true at $a$ and $b$ but not at $c$. On the other hand, $\neg\neg(A\lor B)$ is true everywhere, including $c$. – Andreas Blass Nov 10 '15 at 20:42