September 19th, 2012

beartato phd

(no subject)

Okay so the nice thing about making up a (negative) connective P $ N and defining it as (P -o 0) + N while imagining that ^P is kinda like q * P and vN is kinda like q -o P is that it seems at first like you get an inference rule

G, D, [N] |- C G |- [P]
G, D, [P $ N] |- C

Where you're allowed to discard some resources to prove the P, but continue on with the N. But I'm cheating a little bit when I say this is the "generated" inference rule. What's going on is every stable proposition in the context begins with a "q -o" left over from blurring on a downarrow. Similarly on the right there's going to be a "q *". So think about the case where I gobble up a q-o in the process of focusing on something on the left. It eventually drills down to P $ N = (P -o 0) + N. Suddenly I blur and asynchronously decompose the +, but I don't have my token q back because I very much on purpose didn't put the token-return into the definition of P $ N! So I have no choice but to continue decomposing the N and the P in their respective branches, because every other proposition in sight requires a token to do anything.

The fault with this is that if P $ N ever ends up on the right, this assumption is no longer true. The act of failing to provide a token on the left maps to the act of failing to require a token on the right. So the above inference rule isn't really legitimate: I'd have to invent a zoo of stupid custom judgments to sketch out the shape of the implied state machine of walking through the focusing phases of (P -o 0) + N, and it would be real gross.