Then it just could be that your proof idea might work. At least
in three minutes I couldn't see anything wrong with it...
Woo, my idea passes the Three Minutes of Frank test! Although I did have a (later discovered to be) completely broken proof that once passed Three Minutes of Kevin, so I shouldn't get my hopes up too high.
To
fancybred and/or lambdacalculus, who are probably the only people who actually care:Translate the multiple conclusion labelled sequent calculus into a single conclusion labelled natural deduction system which has rules like
G; D, u:A[p] |- M : A[p]
----------------------------
G; D |- letcc u in M : A[p]
G; D, u:A[p] |- M : A[q] G |- q <= p
----------------------------------------
G; D, u:A[p] |- throw M to u : *
G, A[a], a>=p; D |- M : B[p]
-----------------------------
G; D |- λx.M : A → B[p]
Now we want to get rid of all the throws and letccs. The unused ones are easiest. Consider as a redex
letcc u in M
if u is never used in M. Let it reduce to M. Also consider as a redex any term of the form
letcc u in C[throw M to u]
where C is a term-context-with-hole and M is a term itself without any throws in it. Let it reduce to just the term M. Then the claim is that all the label business prevents the obvious potential problem — that M has free variables that used to be bound somewhere in C — from occurring. If M itself had throws in it, this would be unsound. Consider a term like
letcc u : C in g (λx:A. letcc v : B in throw (throw f x to v) to u)
for g : (A → B) → C, f : A → B. If we do the outer throw first, then x (and indeed also v) escapes its scope; so we must do the inner one.
So if both of these reductions are type-preserving (and the only issue, really, is that of variable scoping) then we're set, because certainly they're terminating. Run both until you reach a normal form, erase all labels, and voila, you've got a truly intuitionistic proof.