Jason (jcreed) wrote,

Guh. I think I actually understand cut elimination now. At least assuming I am correctly believing "side formula" to mean "not the formula in which a connective is introduced in this step". Then the asymmetry between how many left commutative and right commutative cases is due to the asymmetry (about the turnstile) of the intuitionistic truth judgment, and the fact that principal, left commutative, and right commutative cover everything, is that if the cut formula isn't a side formula on the left, and isn't a side formula on the right, then it's being introduced on the right and left in the two derivations being cut together, and the rules have to match up because the principal connective is the same in both cases. Gah, gah, gah. Sequent calculi... so... cute...

Now I just need to understand how this all works out in the linear case so I can <ahahaha>magically and instantaneously solve all the problems of a more fully linear logical framework motivated by such a cut-elimination proof that have been open research problems essentially since Frank's 1994 tech report and assaulted vigorously since then by him and Iliano</ahahaha>. I will shake my fists spitefully at everyone I have failed to convince that deep down, despite all of my attempts at humility and accurate evaluation of my own intellectual abilities, I am really an arrogant bastard at heart.

Also had a bit of a double-piano jam session with Ann Lewis. It was pretty fun. I continue to be saddened by how many people aren't familiar with "While my guitar gently weeps", but now N has been reduced to N-1.

  • (no subject)

    Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…

  • (no subject)

    Sean's back in town --- good fun working with nonremote teammates.

  • (no subject)

    Sean's in town at work, good times.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment