Does double negation distribute over disjunction intuitionistically?

Question

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.

Answer 1

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

Answer 2

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!

Answer 3

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.