Actually I think I made an error yesterday having to do with positive atoms. My current state of thinking (having just woken up, so take it with a grain of salt) is that normal natural deduction is weak negative focusing (that is, of the four things in the following list: [negative focus, positive focus, negative inversion, positive inversion] it forces you do to only the first) except it internalizes identity at negative props in a way that allows you to escape focus (assuming you want to allow non-eta-long proofs in your conception of "normal natural deductions") and, at least given the rules for variables we usually use, it forces all atoms to be negative.

The one counterexample I was thinking of for how natural deduction identifies some proofs that focusing doesn't was (with all of P,P',Q,Q' meant to be positive atoms, with ^ being up-shift) x : P, f : P → ^P', y : Q, g : Q → ^Q' |- P' * Q'. In natural deduction, there's only apparently one proof of this, namely the pair (f x, g y). In a focused sequent calculus, I can left-rule up f x and g y in an order independent of each other.

The mistake, I think, is that positive atoms, like other positive connectives, should really have some kind of closed-scope elim, which in natural deduction would enforce the ordering. If all the atoms were negative, and I jiggled around the shifts appropriately, there would be only one sequent proof.
Tags:
• #### (no subject)

I am 36! Didn't do much birthday-related today really. Had some breakfast with my dad in the morning before he left, and a very busy day following…

• #### (no subject)

Oh also it is my birthday, which I am sort of casually trying to ignore. I am old! Whatever.

• #### (no subject)

Had some nice Peruvian food in midtown as a kind of off-date birthday-celebrating thing with K and Sean and Arielle. Learned that they're planning to…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic