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:
• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic