Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Quodlibet. Then $p_{A\vee\lnot A,\bot}^{(\lnot (A\vee\lnot A)\rightarrow(A\vee\lnot A))\rightarrow(A\vee\lnot A)}\lambda_{u^{\lnot(A\vee\lnot A)}} . f_{A\vee\lnot A}^{\bot\rightarrow (A\vee\lnot A)} u (\vee_+^{\lnot A\rightarrow A\vee\lnot A} \lambda_{v^A}.u(\vee_+^{A\rightarrow A\vee\lnot A} v))$ proves the law of the excluded middle $A\vee\lnot A$.

Now, the function `call-with-current-continuation`

, or short `call/cc`

, in scheme, has the signature of $p$ (in Haskell, this one is replaced by its negative translation). The rest of the above term is covered by the Curry Howard Isomorphism, and therefore, using an instance of `call/cc`

as a realizer of $p$ gives a program of type $A\vee\lnot A$.

Of course, something that one expects in programs extracted from constructive proofs must fail here, otherwise one could decide every proposition $A$. I was just wondering, what exactly it is.

Scheme's `call/cc`

will fail with this term, since the continuation is called twice - but that is not really a problem, since one could just copy the whole context of the continuation and bind it into a new function which can then be called multiple times - that would produce a lot of overhead, but still would provide an effective algorithm which must not exist.

And having a `call/cc`

in the beginning of a term does also not seem very useful, but inside another term, this should not be a problem.

Then, maybe in this context we must not use $f$. Normally, instances $f$ of the Ex Falso Quodlibet must never be called, and in this term, it could be called (and would give an instance of $A\vee\lnot A$) - but on the other hand, the continuation is called twice before ever coming to call $f$, so I am not sure whether this is actually the problem.

And then of course, $u$ is called twice, once with an instance of $A\vee\lnot A$ that eliminates to $A$, and once with an instance that eliminates to $\lnot A$. So probably calling $u$ with both outcomes of $A\vee\lnot A$ may produce endless loops or strange behaviour.

As I said, I am not sure what exactly fails here. Does anybody know?