positive props P ::= ↓G | P ⊕ P | 0
negative props N ::= ↑G | N & N | ⊤
games G ::= {N|P}
And the interpretation
{N|P} = (left ⊸ N) & (right ⊸ P)
↓G = left ⊗ G
↑G = right ⊗ G
and you consider the classical negation of {N|P}. It's not quite the negative of a game in the Conway-Berlekamp-Guy sense... (defined by -{P|N} = {-N|-P} and -(P ⊕ P) = -P & -P and -↑G = ↓-G and so on) but it seems related somehow. You get
{N|P}⊥ = (left ⊗ N⊥) ⊕ (right ⊗ P⊥)
(↓G)⊥ = left ⊸ G⊥
(↑G)⊥ = right ⊸ G⊥
and then proof search on, say, left, {N|P}⊥ ⊢ 0 actually plays out very similarly to that on left, {-P|-N} ⊢ 0, as long as left ⊸ left ⊸ 0 and right ⊸ right ⊸ 0. I posted on twitter about the idea of making this kind of behavior judgmentally intrinsic.
