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.
 A: 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$.

*

*Assume $\neg\neg (P \rightarrow Q)$.

*Assume $\neg\neg P$.

*Assume $\neg Q$.

*Assume $P$.

*Since $P$ holds (4), so does $(P \rightarrow Q) \rightarrow Q$.

*Using (3), we get $(P \rightarrow Q) \rightarrow (Q \wedge \neg Q)$.

*We conclude $\neg (P \rightarrow Q)$ from (6), which contradicts (1).

*We discharge assumption (4), and by contradiction (7) conclude $\neg P$, which contradicts (2).

*We discharge assumption (3), and by contradiction (8) conclude  $\neg\neg Q$.

*We discharge assumption (2), and by (9) conclude $\neg\neg P \rightarrow \neg\neg Q$.

*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.

*

*Assume $\neg\neg P \rightarrow \neg\neg Q$.

*Assume $\neg (P \rightarrow Q)$.

*Assume $Q$.

*From (3) we have $P \rightarrow Q$, which contradicts (2).

*We discharge assumption (3), and conclude $\neg Q$.

*Assume $\neg P$.

*From (6) we have $P \rightarrow P \wedge \neg P$.

*By ex contradictione quodlibet on (7) we have $P \rightarrow Q$, which contradicts (2).

*We discharge assumption (6) and by contradiction (8) conclude $\neg \neg P$.

*From (1) and (9) we have $\neg\neg Q$, which contradicts (5).

*We discharge assumption (2) and by contradiction (10) conclude $\neg\neg (P \rightarrow Q)$.

*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)$.

A: 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.
A: 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.
