# 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. Nov 10, 2015 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. Nov 10, 2015 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). Nov 10, 2015 at 17:35

By substituting $$¬A$$ for $$B$$ in $$¬¬(A∨B)→(¬¬A∨¬¬B)$$ we can easily derive weak excluded middle $$¬¬A∨¬A$$ which is certainly not intuitionistically acceptable. Hence $$¬¬(A∨B)→(¬¬A∨¬¬B)$$ is also not acceptable.

$$\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}$$ under the subspace topology, 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$. Nov 10, 2015 at 20:42
• @RobArthan: Thank you, your answer is very clear! Nov 10, 2015 at 21:10
• @AndreasBlass: also your answer is very clear, thank you! Nov 10, 2015 at 21:15
• My topology is pretty bad, are you certain $\lnot \lnot (A \lor B) = [0, 1]$ ? I am getting $(0, 1)$ according to the definition of interior I'm finding. The third bullet point here: en.wikipedia.org/wiki/Interior_(topology)#Examples . Also how are you defining $\top$ ? Thanks Nov 9, 2021 at 7:41
• I should have made it clearer that we are working with the subspace topology on $[0, 1]$ here. $[0, 1]$ is open in that topology. Hence $\mathrm{Int}([0, 1]) = [0, 1]$. $\top$ is the open set $[0, 1]$ (it's not open viewed as a subset of $\Bbb{R}$ but it is open in the subspace topology on $[0, 1]$). Nov 9, 2021 at 21:10

Before getting down to technicalities, in cases like this it is worth first thinking informally. So, should we expect $$\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$$ to hold intuitionistically, given an informal BHK-style understanding of the connectives? If we are in a position to rule out being able to refute $$A \lor B$$, does that mean we must already be in a position to rule out being able to refute $$A$$ or alternatively in a position to to rule out being able to refute $$B$$?

Intuitively(!) not. So that gives us a motivation for expecting the given wff to fail as an intuitionistic theorem, and hence to look for a Kripke counter model. And as Andreas Blass shows, once you start looking for a suitable model, given the constraints, you'll quickly land on one!