Does double negation distribute over implication intuitionistically?

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

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.

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.