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

  • (no subject)

    Poking around the library again today. Found out Martin Schongauer had already developed the amazing German Renaissance cross-hatching style I had…

  • (no subject)

    Ah, some delightful broken english in my inbox. Italicized is the one part I believe sincerely. How there.? How are you? You single? And I'm single…

  • (no subject)

    Someone please call up Germany for me and tell them to stop sending me email about the 1945 bombing of Dresden. It was a horrible thing to have done,…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded