So I tried to come up with some fiddly token-passing translation (of course) to understand it through, because that's the one hammer I have.
I ended up with a very strange sort of... tri-polar? syntax for the source language. I have
positive props P ::= ↓G | P ⊕ P | 0
negative props N ::= ↑G | N & N | ⊤
games G ::= {N|P} | G + G
The notation {N|P} is meant to echo the ONAG notation of left and right moves. For the fiddly translation, conjure up parametrically (i.e. imagine you are invoking ∀R or ∃L to get them) a plain old set-theoretic set S, and a distinguished point x ∈ S of it. The translation has three phases:
[P, a, b] outputs a positive proposition in linear logic
[N, a, b] outputs a negative proposition in linear logic
[G, a, b] outputs a positive proposition in linear logic
and both a and b are subsets of S. The translation is:
[P1 ⊕ P2, a, b] = [P1, a, b] ⊕ [P2, a, b]
[0, a, b] = 0
[N1 & N2, a, b] = [N1, a, b] & [N2, a, b]
[⊤, a, b] = ⊤
[↓G, a, b] = (x ∈ b) ⊗ [G, a, b]
[↑G, a, b] = ↑((x ∉ b) ⊗ [G, a, b])
[G1 + G2, a, b] = ∃c1,c2.(a = c1 ∩ c2) ⊗ [G1, c1, b] ⊗ [G2, c2, b]
[{N|P}, a, b] = ↓(((x ∈ a) ⊸ [N, a, b]) & ((x ∉ a) ⊸ ↑[P, a, b]))
and you read off "Left player wins G assuming Left starts" by the provability of
∃a.[↓G, a, a] ⊦ 0
and "Left player wins G assuming Right starts" by the provability of
∃a.[↑G, a, a] ⊦ 0
The propositions x ∈ a and x ∉ a are passed around as linear tokens in the context signalling that it's left's (∈) or right's (∉) turn to play, and the subset a that we're concerned about the point x being in or not gives the address of the current part of the expression tree that the player is thinking about moving in. Doing proof search starting from ∃a.[↓(G1 + G2), a, a] ⊦ 0 we get to the state
(x ∈ a), ∃c1,c2.(a = c1 ∩ c2) ⊗ [G1, c1, a] ⊗ [G2, c2, a] ⊦ 0
and thence to
(x ∈ c1 ∩ c2), [G1, c1, c1 ∩ c2] ⊗ [G2, c2, c1 ∩ c2] ⊦ 0
which is equivalent to
(x ∈ c1) & (x ∈ c2), [G1, c1, c1 ∩ c2], [G2, c2, c1 ∩ c2] ⊦ 0
so the synchronous player, whose turn it is, has to make a choice whether to play in [G1, c1, c1 ∩ c2], which will consume (x ∈ c1) and eventually yield (x ∉ c1 ∩ c2), or to play in [G2, c2, c1 ∩ c2], which will consume (x ∈ c2) and eventually yield (x ∉ c1 ∩ c2). But then note that (x ∉ c1 ∩ c2) is equivalent to (x ∉ c1) ⊕ (x ∉ c2) --- the asynchronous player makes a nondeterministic choice among the two subgames to play in, as they should.
With this setup I can show through an easy induction that the zero game 0 = {⊤|0} (I'm being careful to distinguish the zero game 0 where both players have no options from the logical 0 which is specifically about the asynchronous player having no options) actually is a unit for addition, i.e. G ⊣⊢ {⊤|0} + G, by which I mean [G, a, a] ⊣⊢ [{⊤|0} + G, a, a], but two sad things happen:
- This proof seems to break if I try to add multiplicatives to the source language
- I don't get equivalence of the zero game with the nim game consisting of two heaps of size one, written {*|*} in ONAG notation, and {{{⊤|0}|{⊤|0}}|{{⊤|0}|{⊤|0}}} in my language here. The logical treatment seems to think that it's "better" that you can make at least one move in {*|*}, where as you don't even have a move in 0, so bisimulation fails.
However, if we write 1 = {0|0}, then the logic can tell that two representations of 2 are equivalent: {1|0} ⊣⊢ {0 & 1|0} (in ONAG notation this would have been written {1|} = {0,1|})