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.
Tags:
• #### (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…

• #### (no subject)

Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

• #### (no subject)

Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic