November 20th, 2008

beartato phd

(no subject)

Chatted with Christoph Benzmüller briefly about Frank's idea of the possibility of taking the HLF linear logic encoding trick and using it to trick Leo II into doing linear logic theorem proving.

Had a couple more reasonably exciting category-theory ideas occur to me clustered around Seely's 1987 lics paper on the 2-categorical structure of the lambda-calcullus that neelk pointed me toward. Five minutes of fairly simple crank-turning revealed that the modifications (i.e 3-cells) in the biadjunctions behind implication and conjunction go one way, and in disjunction they go the other way. I checked [Seely 1979] in the references of the above paper and his calculations seem to agree with mine.

But what he couldn't have speculated on back then were the consequences for focusing, which wouldn't be invented for another several years...

So: even though we know positive connectives are left adjoints and negative connectives are right adjoints, the biadjunction also seems to be tracking, of the two functors involved, which is the "logical connective" and which is the "corresponding judgmental widget".

It stands to reason that probably this is another way to view the reason that you can compose positive (resp.) negative connectives and get another positive (resp. negative) connective; with like polarities, they actually have arrows pointing the same direction that compose appropriately.