Game semantics of linear logic



Linear logic is a weird sort of logic. It’s most commonly explained by saying that the “weakening” rule: Sorry, your browser does not support SVG. and the “contraction” rule Sorry, your browser does not support SVG.. In other words - you have to use all the assumptions, and you can’t use an assumption more than once. This is usually interpreted in terms of resources - just because I can make a Sorry, your browser does not support SVG. out of two As doesn’t mean I can do it with one Sorry, your browser does not support SVG.. And I can’t just throw an Sorry, your browser does not support SVG. away that I might not need - I need to find a process for getting rid of it.

However, there’s also another way of thinking about linear logics - in terms of games. The combinators of linear logics become ways of combining games into other games. The interpretation of the deduction rules is now that a proof of the sequent Sorry, your browser does not support SVG. should provide a winning strategy for Sorry, your browser does not support SVG..

Let us be a bit more (but not too) precise. There are two players. Following convention, we call them the prover, P, and the opponent, O. It is understood that we are “on the side” of P, although we could equally well do it the other way - the logic is symmetric enough for that. A game has a starting player (in many treatments, it is assumed the opponent always goes first, but not here). Play is usually assumed to proceed back and forth, each player making one move at a time, but this is not important - the most important thing is that in each position, there is a well-defined next player. Each player has a number of possible moves, only some of which may be legal in a given position - by “position”, we simply mean the sequence of moves so far. We generally think of a player as losing when they have to move, but have no legal moves.

The most basic operator is the “dual” or “negation” operator, Sorry, your browser does not support SVG.. This simply interchanges the position of the players. The next operator is Sorry, your browser does not support SVG.. This game consist of playing Sorry, your browser does not support SVG. and Sorry, your browser does not support SVG. simultaneously - the player must move in whatever game the opponent just moved in, while the opponent can switch games at will.

Clearly, a winning strategy for this game, for the player, entails a winning strategy for each component game. In this sense, this game is like logical “and”.

But there’s also another operator like “and”, which is written Sorry, your browser does not support SVG.. This is played as follows: the opponent chooses a game, then that game is played to completion, and its winner wins the whole game.

Here is a difference between these operators: There is a canonical strategy for Sorry, your browser does not support SVG., but not for Sorry, your browser does not support SVG.. How does this work? To play Sorry, your browser does not support SVG., we must play the opponent’s side in Sorry, your browser does not support SVG.. Assume wlog that the player goes first in Sorry, your browser does not support SVG.. We have the player start playing in Sorry, your browser does not support SVG., then copy this move into Sorry, your browser does not support SVG.. Whatever they play in response, we go to Sorry, your browser does not support SVG. and play that as our response to them, and so on. We’re guaranteed to win (exactly) one of the games, since the two games will be exactly mirrored. If this doesn’t make sense, imagine playing two chess games against another person - one as black, one as white. Starting with the game in which they’re white, they make a move. You copy this move on the other chessboard. They respond with black, which you also copy on the fist board. When they mate you at some point on one board, you copy this immediately, winning the other game.

This strategy won’t work for Sorry, your browser does not support SVG.. Here we would have to decide at the beginning which game we have a winning strategy in, then choose that one.

In logic, this means that the sequent Sorry, your browser does not support SVG. is provable, but Sorry, your browser does not support SVG. isn’t.

So far, we’ve only looked at the two forms of conjunction. There is also two forms of disjunction, given simply by Sorry, your browser does not support SVG., Sorry, your browser does not support SVG.. We could restate the above discussion as “ Sorry, your browser does not support SVG. is not provable, but $is”. This means we have a form of excluded middle, but another form of excluded middle doesn’t hold.

Now what is the meaning of a general sequent of the form Sorry, your browser does not support SVG., where both Sorry, your browser does not support SVG. and Sorry, your browser does not support SVG. are multisets. We can interpret such a sequent as asserting the existence of a strategy for the game Sorry, your browser does not support SVG.. A proof is supposed to identify a specific strategy for the game. This also means that any sequent can be replaced by a one-sided one, which means linear logic can be expressed all in terms of one-sided sequents (which is indeed true).

Now we can think about the lack of contraction - we can examine simply the fact that Sorry, your browser does not support SVG. is not a provable sequent.

To prove this sequent, we would want a strategy for Sorry, your browser does not support SVG.. We can think of this again in the case where Sorry, your browser does not support SVG. is chess. Imagine that instead of two games, there are three, two where you are black. You can only respond on whatever black board where your opponent just moved as white, or move as white on the board where you are white (forcing your opponent to respond there). And when you respond as black, your opponent can switch to the other black board. You can only mirror one of these onto the game where you’re white, so the strategy-stealing trick no longer works.

On the other hand, weakening is valid in this semantics. We do have a strategy for the game Sorry, your browser does not support SVG.. Here you have two white boards and one black, and you can simply ignore the white board you don’t need, since you now have full control over which board you move on.

This is all written out in Blass: A game semantics for linear logic.