Jason (jcreed) wrote,

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...
Tags: focusing, logic, math, twelf

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded