Thought some more about what happens when you take
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. |