Actually I think I made an error yesterday having to do with positive…: jcreed

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.

(no subject)

(no subject)

(no subject)

Error