Does double negation distribute over implication intuitionistically?

Does the equivalence $$\neg\neg (P \rightarrow Q) \leftrightarrow (\neg\neg P \rightarrow \neg\neg Q)$$ hold in propositional intuitionistic logic? In propositional classical logic the equivalence holds obviously since $P \leftrightarrow \neg\neg P$. However, the similar-looking implication $\neg\neg (P \vee Q) \rightarrow (\neg\neg P \vee \neg\neg Q)$ is not intuitionistically acceptable. The validity of the backward implication comes up in some questions about type theory as well.

Somewhat surprisingly, the identity does hold in intuitionistic logic. We give three arguments: an informal natural deduction-style proof, a formal proof in the Agda proof assistant, and a formal derivation tree in the contraction-free intuitionistic sequent calculus G4ip.

Informal proof

We prove the implications $\neg\neg (P \rightarrow Q) \rightarrow (\neg\neg P \rightarrow \neg\neg Q)$ and $(\neg\neg P \rightarrow \neg\neg Q) \rightarrow \neg\neg (P \rightarrow Q)$ separately.

We start with the former, $\neg\neg (P \rightarrow Q) \rightarrow (\neg\neg P \rightarrow \neg\neg Q)$. Our strategy is as follows: we will assume that $\neg\neg(P \rightarrow Q)$, $\neg\neg P$ and $\neg Q$ all hold. If we can derive a contradiction from these assumptions, we'll be able to conclude $\neg\neg Q$. To derive a contradiction from our assumptions, it suffices to prove $\neg P$.

1. Assume $\neg\neg (P \rightarrow Q)$.
2. Assume $\neg\neg P$.
3. Assume $\neg Q$.
4. Assume $P$.
5. Since $P$ holds (4), so does $(P \rightarrow Q) \rightarrow Q$.
6. Using (3), we get $(P \rightarrow Q) \rightarrow (Q \wedge \neg Q)$.
7. We conclude $\neg (P \rightarrow Q)$ from (6), which contradicts (1).
8. We discharge assumption (4), and by contradiction (7) conclude $\neg P$, which contradicts (2).
9. We discharge assumption (3), and by contradiction (8) conclude $\neg\neg Q$.
10. We discharge assumption (2), and by (9) conclude $\neg\neg P \rightarrow \neg\neg Q$.
11. We discharge assumption (1), and by (10) conclude $\neg\neg (P \rightarrow Q) \rightarrow (\neg\neg P \rightarrow \neg\neg Q)$, which was to be shown.

The other direction, $(\neg\neg P \rightarrow \neg\neg Q) \rightarrow \neg\neg (P \rightarrow Q)$ is proven using a very similar strategy: we assume $\neg\neg P \rightarrow \neg\neg Q$ and $\neg (P \rightarrow Q)$, and derive that both $\neg Q$ and $\neg\neg Q$ follow from these assumptions.

1. Assume $\neg\neg P \rightarrow \neg\neg Q$.
2. Assume $\neg (P \rightarrow Q)$.
3. Assume $Q$.
4. From (3) we have $P \rightarrow Q$, which contradicts (2).
5. We discharge assumption (3), and conclude $\neg Q$.
6. Assume $\neg P$.
7. From (6) we have $P \rightarrow P \wedge \neg P$.
8. By ex contradictione quodlibet on (7) we have $P \rightarrow Q$, which contradicts (2).
9. We discharge assumption (6) and by contradiction (8) conclude $\neg \neg P$.
10. From (1) and (9) we have $\neg\neg Q$, which contradicts (5).
11. We discharge assumption (2) and by contradiction (10) conclude $\neg\neg (P \rightarrow Q)$.
12. We discharge assumption (1) and by (11) conclude $(\neg\neg P \rightarrow \neg\neg Q) \rightarrow \neg\neg (P \rightarrow Q)$, which was to be shown.

Agda proof

The Agda proof is a straightforward transcription of the informal proof presented above:

module _ where

open import Data.Empty

¬¬ : Set → Set
¬¬ A = (A → ⊥) → ⊥

contradiction : ∀ {P Q : Set} → P → (P → ⊥) → Q
contradiction a nA with nA a
... | ()

¬¬-distributes-over-→-1 : ∀ P Q → ¬¬ (P → Q) → ¬¬ P → ¬¬ Q
¬¬-distributes-over-→-1 P Q not[P-implies-Q] nnP nQ =
  contradiction nP nnP where
  nP : P → ⊥
  nP p = not[P-implies-Q] (λ p-implies-q → nQ (p-implies-q p))

¬¬-distributes-over-→-2 : ∀ P Q → (¬¬ P → ¬¬ Q) → ¬¬ (P → Q)
¬¬-distributes-over-→-2 P Q nnP-implies-nnQ not[P-implies-Q] =
   contradiction nQ nnQ where
   nQ : Q → ⊥
   nQ q = not[P-implies-Q] (λ p → q)
   nnP : ¬¬ P
   nnP nP = not[P-implies-Q] (λ p → contradiction p nP)
   nnQ : ¬¬ Q
   nnQ = nnP-implies-nnQ nnP

Sequent proof

Here we prove only the more difficult direction: the argument differs a bit from the other two, as it amounts to proving the desired goal via the lemma $(\neg\neg A \rightarrow \neg\neg B) \rightarrow (\neg B \rightarrow (A \rightarrow B)$.

At a higher level, this equivalence is easy to prove using the monadicity of double negation: this is the tautology $$\lnot\lnot P \rightarrow [(P \rightarrow \lnot\lnot Q) \rightarrow \lnot\lnot Q].$$ As a consequence of this, as a derived inference rule, we can conclude that if $\Gamma, P \vdash \lnot\lnot Q$, then $\Gamma, \lnot\lnot P \vdash \lnot\lnot Q$. Intuitively, what this means is: if the desired conclusion is a double negation, then we can freely eliminate double negations in hypotheses, add instances of LEM $\phi \vee \lnot\phi$ to the assumptions, etc.

So, for the forward direction, we easily reduce to showing that $\lnot\lnot(P\rightarrow Q), \lnot\lnot P \vdash \lnot\lnot Q$. By the principle above, then it suffices to show $P \rightarrow Q, P \vdash \lnot\lnot Q$. But since $Q \rightarrow \lnot\lnot Q$, and $P\rightarrow Q, P \vdash Q$ is trivial, we are now done.

Similarly, for the reverse direction, we easily reduce to showing $\lnot\lnot P \rightarrow \lnot\lnot Q \vdash \lnot\lnot(P \rightarrow Q)$. We can now introduce $P\vee \lnot P$ and $Q\vee \lnot Q$ into the context; then, using that $P\vee \lnot P$ implies $\lnot\lnot P \leftrightarrow P$, we can reduce $\lnot\lnot P \rightarrow \lnot\lnot Q$ to $P \rightarrow Q$. Then trivially, $P\rightarrow Q, P \vee \lnot P, Q \vee \lnot Q \vdash \lnot\lnot(P \rightarrow Q)$.

Under the Curry-Howard correspondence, a typical proof of the tautologies $P \rightarrow \lnot\lnot P$ and $\lnot\lnot P \rightarrow [(P \rightarrow \lnot\lnot Q) \rightarrow \lnot\lnot Q]$ corresponds closely to the continuation monad $\operatorname{Cont}(\bot)$. Then for example, the forward direction of the proof in Haskell-like notation might look like:

\(nnpq : ~~(P -> Q)) (nnp : ~~P) .
    do {
        pq <- nnpq;     -- pq : P -> Q
        p <- nnp;       -- p : P
        return (pq p)   -- (pq p) : Q  so  return (pq p) : ~~Q
    }

On a related note, the above proofs could be considered an elaboration of an application of Glivenko's theorem that in propositional logic, $\Gamma \vdash P$ classically if and only if $\Gamma \vdash \lnot\lnot P$ intuitionistically. Glivenko's theorem then makes for trivial proofs that $\lnot\lnot(P\rightarrow Q), \lnot\lnot P \vdash \lnot\lnot Q$ and $\lnot\lnot P \rightarrow \lnot\lnot Q \vdash \lnot\lnot(P \rightarrow Q)$ intuitionistically.

Here's a briefer version of essentially the same argument, using other (perhaps better known?) facts about intuitionisic logic.

For the direction $\neg\neg(P\to Q) \to (\neg\neg P \to \neg\neg Q)$, note that this is equivalent to $\neg\neg(P\to Q) \wedge \neg\neg P \to \neg\neg Q$. Since $\neg\neg$ preserves $\wedge$ and is functorial, this follows from $(P\to Q) \wedge P \to Q$, which is clear.

For the direction $(\neg\neg P \to \neg\neg Q) \to \neg\neg(P\to Q)$, we assume $\neg\neg P \to \neg\neg Q$ and $\neg (P\to Q)$ for a contradiction. But $\neg(P\to Q)$ is equivalent to $\neg\neg P \wedge \neg Q$. Since we have $\neg\neg P\to \neg\neg Q$, we get $\neg\neg Q$, which combined with $\neg Q$ is a contradiction.