Jason (jcreed) wrote,

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: logic, math, read-only, sharing

  • (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


    Anonymous comments are disabled in this journal

    default userpic

    Your IP address will be recorded