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.