March 23rd, 2013

beartato phd

(no subject)

Reading some of simrob's draft paper and accompanying formalization reminds me that I don't know of anything stopping me from fully twelfing up my own completeness-of-focusing proof, which ought to run fairly closely parallel to his. If I remember right, the places where he gets a for-free uniform substitution principle of focal things into suspended things, e.g.

Γ |- [P]
Γ, <P> |- C
-------------------------
Γ |- C

I expect I should also get that for free from the cut principle for the unfocused logic, because the translation of [P] on the right and <P> on the left should work out to the same thing.

Hmm I should try doing that one of these days...