Jason (jcreed) wrote,
Jason
jcreed

I've gotten caught up in the last few days working on a new tack on a vague idea concerning the proof of completeness for focussing, which I first had about this time last year. The underlying dogma I'm clinging to is that focussing is not so much about forcing decomposition into little alternating phases, but more about which logical connectives really exist for a given judgmental setup, and more to the point, which connectives can be coalesced - the answer being, of course, those of the same polarity.

This means that asynchronous connectives need not be eagerly decomposed, and this simplifies the soundness proof. The bookkeeping for showing completeness this way has always been off-puttingly ugly and un-modular, though I did manage to slog through it once. Yesterday afternoon I discovered a nice little encoding of the context discipline of focussing of intuitionistic logic into (depending how you look at it) a variant of ordered logic with a couple of only mildly exotic modal operators, or, if you prefer, perfectly ordinary ordered logic with focussing applied only to positive atoms and the copy rule.

Inside this encoding:

  • The bookkeeping of tracking the long-term effects of asynchronous decomposition can be fully internalized into the language of propositions
  • The essential commutativity properties of asynchronous decomposition fall out as two easy-to-state lemmas, one for positive connectives, and one for negative
  • The total amount of proof-work to establish focalisation is evidently linear in the number of logical connectives


I'm really quite happy with it.
Tags: focussing, math
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 9 comments