Jason (jcreed) wrote,

Aaaaaah I maybe think I understand what's going on with Liang's "A Unified Proof-Theoretic Framework for Classical, Intuitionistic and Linear Logics" enough to start explaining to myself why there's that proliferation of so many weird connectives on page 5.

It goes like this: if you're intuitionistic, you can have a simple two-level logic with intrinsically persistent connectives on one level, and intrinsically linear connectives on another. There are adjoint connectives F and U connecting the two syntactic categories.

R ::= UI | R ∧ R | R ⇒ R | ...
I ::= FR | I ⊗ I | I ⊸ I | ...

In this syntax, the modal operator ! decomposes as FU, the comonad arising in the standard way from the adjunction of F and U.

If you want to polarize this, well, there are negatives and positives at both levels. So it splits into R+, R-, I+, and I-. Turns out F is positive and U is negative. There is a pair of shift operators at each level.

R+ ::= ↓R- | R+ ∧+ R+ | ... R- ::= ↑R+ | UI- | R+ ⇒ R- | ...
I+ ::= ↓I- | FR+ | I+ ⊗ I+ | ... I- ::= ↑I+ | I+ ⊸ I- | ...

Ok, but now you want classical logic. Things work out mostly how you expect at the linear level, and you get all the connective-collapses you expect: additve and and or collapse as duals, and lollipop becomes just a version of par, which is dual to tensor. But think about how box and ! work in classical modal and linear logics, respectively: the dual of box is diamond, the dual of ! is ?. So since we have intrinsically persistent propositions (which are the linear logic analogue of intrinsically valid propositions in a two-level modal logic) their duals must be intrinsically merely-possible propositions. So everything in R+ and R- (which are "upstairs" relative to I- and I+) dualizes not to some other connective in R- and R+, but to a mirror image "downstairs" in a new pair of syntactic classes L- and L+ below I- and I+. We get:

R+ ::= ↓R- | R+ ∧+ R+ | ... R- ::= ↑R+ | UI- | R+ ⊔ R- | ...
I+ ::= ↓I- | FR+ | I+ ⊗ I+ | ... I- ::= ↑I+ | UL- | I- ⅋ I- | ...
L+ ::= ↓L- | FI+ | L- ⊠ L+ | ... L- ::= ↑L+ | L- ∨- L- | ...

where R- is dual to L+, R+ is dual to L-, and I- is dual to I+. I've taken the liberty of rewriting ⇒ as ⊔ to match the notation in the paper.

The difficulty in verifying that this explanation is correct is that the paper doesn't include any of the shifts, neither ↑/↓-style nor U/F-style. They're all implicit in the fiddly side conditions of the "reaction" rules. Although, given that including them raises the logical-connective count from the already-high 28 to 38, I'm sympathetic to the desire to leave them out...

Fortunately I also think I know how to translate the whole pile down to good ol' ∀, ∧, ∨, and ⇒.

Tags: classical, linear, logic, math, modal

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded