There are two ways to go about this:
Proof theory. We analyse the formal proofs in the inference system given, and show that there can be no formal proof of double negation elimination. This is difficult and depends a lot on the details of the inference system.
Model theory. We construct a model of intuitionistic propositional logic in which double negation elimination is visibly false. This is much easier and less sensitive to details, but is conceptually more challenging.
First of all, what is a model of intuitionistic propositional logic? It is an algebraic structure $\mathfrak{A}$ equipped with constants $\top$ and $\bot$ as well as binary operations $\land$, $\lor$, $\to$, plus a partial order $\le$, such that the following soundness rule is valid: given formulae $\phi$ and $\psi$ in the language of intuitionistic propositional logic with propositional variables $x, y, z, \ldots$, if the sequent $\phi \vdash \psi$ is provable, then $\phi \le \psi$ in $\mathfrak{A}$ for all choices of $x, y, z, \ldots$ in $\mathfrak{A}$.
For example, $\mathfrak{A}$ could be a Heyting algebra, which is a algebraic structure satisfying some axioms. First of all $\mathfrak{A}$ is a (bounded) lattice:
- Unit laws:
\begin{align}
\top \land x & = x &
\bot \lor x & = x \\
x \land \top & = x &
x \lor \bot & = x
\end{align}
- Associativity, commutativity, and idempotence:
\begin{align}
(x \land y) \land z & = x \land (y \land z) &
(x \lor y) \lor z & = x \lor (y \lor z) \\
x \land y & = y \land x &
x \lor y & = y \lor x \\
x \land x & = x &
x \lor x & = x \\
\end{align}
- Absorption law:
\begin{align}
x \land (x \lor y) & = x &
x \lor (x \land y) & = x
\end{align}
One can then verify that $x \le y$ defined by $x \land y = x$ is a partial order on $\mathfrak{A}$ and that $\top$, $\bot$, $\land$, $\lor$ have their usual order-theoretic meanings. We then add some axioms for $\to$:
- Distributive law:
$$x \to (y \land z) = (x \to y) \land (x \to z)$$
- Internal tautology:
$$x \to \top = \top$$
- Internal weakening:
$$y \to (x \land y) = y$$
- Internal modus ponens:
$$x \land (x \to y) = x \land y$$
Exercise. Show that $y \le z$ implies $(x \to y) \le (x \to z)$, and $x \le ((x \land y) \to y)$ and $((x \to y) \land y) \le x$, and hence or otherwise that $x \land y \le z$ if and only if $x \le (y \to z)$.
Exercise. Verify the soundness rule for interpreting intuitionistic propositional logic in a Heyting algebra.
Proposition. Double negation elimination is not valid in intuitionistic propositional logic.
Proof. We construct a three-element Heyting algebra to falsify double negation elimination. Let $\mathfrak{A} = \{ \bot, \omega, \top \}$ and define the binary operations as below:
\begin{align}
\begin{array}{|r|ccc|}
\hline
\land & \bot & \omega & \top \\
\hline
\bot & \bot & \bot & \bot \\
\omega & \bot & \omega & \omega \\
\top & \bot & \omega & \top \\
\hline
\end{array} &&
\begin{array}{|r|ccc|}
\hline
\lor & \bot & \omega & \top \\
\hline
\bot & \bot & \omega & \top \\
\omega & \omega & \omega & \top \\
\top & \top & \top & \top \\
\hline
\end{array} &&
\begin{array}{|r|ccc|}
\hline
\to & \bot & \omega & \top \\
\hline
\bot & \top & \top & \top \\
\omega & \bot & \top & \top \\
\top & \bot & \omega & \top \\
\hline
\end{array}
\end{align}
Then, observe that $((\omega \to \bot) \to \bot) = \top$, but $\top \nleq \omega$. Therefore $(x \to \bot) \to \bot$ cannot be an axiom of intuitionistic propositional logic.
Remark. De Morgan's laws remain valid in this Heyting algebra. Find one which falsifies part of De Morgan's laws. (See this question.)
One of the semantics for intuitionistic propositional logic is to interpret propositions' "truth values" in a Heyting algebra instead of a Boolean algebra. One of the ways to define a Heyting algebra is as a partial order that, as a thin category, is finitely cocomplete and Cartesian closed. This suggests that we can probably interpret intuitionistic propositional logic more generally in finitely cocomplete Cartesian closed categories, and this does in fact work.
Note that a colimit of a morphism $P\to Q$ is the wrong way to think about an implication. That colimit is going to be isomorphic to $Q$ itself. Rather you want the exponential object $Q^P$ provided by Cartesian closedness; one way to see this is to see that the evaluation map for exponentials, in propositional terms, essentially establishes modus ponens.
There is a way to extend the idea to first order logic, but it takes a little more gear. The easiest setup to understand for the first order case is where we have functor $P:\mathcal{C}^{op}\to\mathbf{Cat}$ such that $P(C)$ is finitely cocomplete and Cartesian closed for all $C$, and the $P(f)$ preserve that structure and all have left and right adjoints satisfying some nice-ness conditions. Then we can think of the objects of $P(C)$ as "predicates on $C$", the $P(f)$ as "substitution of terms", and the right and left adjoints are quantification. There are more general structures that are more flexible than these $\mathbf{Cat}$-valued functors, but I think these are the easiest gateway for later figuring out what those structures (namely fibred categories) are trying to do, should you end up wanting to look into them more.
Best Answer
Turns out that my question is answered in great detail here: http://www.ps.uni-saarland.de/~duchier/python/continuations.html