Definition 1.5.1 (Double-negation translation). We recursively define the $\neg \neg$-translation ${\phi }^N$ of a proposition $\phi$ in the following way:

• If $p$ is a primitive proposition, then $p^N:=\neg \neg p$;

• ${(\phi \wedge \psi )}^N:={\phi }^N\wedge {\psi }^N$

• ${(\phi \to \psi )}^N:={\phi }^N\to {\psi }^N$

• ${(\phi \vee \psi )}^N:=\neg (\neg {\phi }^N\wedge \neg {\psi }^N)$

• ${(\neg \phi )}^N:=\neg {\phi }^N$