`Then it just could be that your proof idea might work. At least`

in three minutes I couldn't see anything wrong with it...

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]

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.