Jason (jcreed) wrote,
Jason
jcreed

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.
Tags: games, linear logic, logic, math
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments