Game semantics of linear logic [game-semantics-of-linear-logic]

Linear logic is a weird sort of logic. It's most commonly explained by saying that the "weakening" rule: <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_570c4c92abfcb8419f3d26233037e0de1c74aecf.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> and the "contraction" rule <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_b3da13021d306636a1a258e2de559738f5f41da8.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_8582cbf09790ec5906444f9f5df9cd00053cb98e.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> out of two As doesn't mean I can do it with one <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. And I can't just throw an <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_fbc8e225dbcfabfee571f016d25f90b9b3aca8af.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> should provide a winning strategy for <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>.

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, <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_bc4947b04e7ea496037197a0809d11da55422409.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. This simply interchanges the position of the players. The next operator is <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_279df3c8f4a8f9a7e4ae8fbdb05c6f1d880f9c99.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. This game consist of playing <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> and <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_8582cbf09790ec5906444f9f5df9cd00053cb98e.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_cd339c6a9fd60f255d5641e7b67849d12862ec66.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_c224d906e554f6971f4d8beea3fbf24f53936870.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>, but not for <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_c7ea9bf60399dae5f34e826d4f1a8ecc0a4a6030.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. How does this work? To play <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_c224d906e554f6971f4d8beea3fbf24f53936870.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>, we must play the opponent's side in <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_d3860e22107b32eb22a9449fa3807d8f08cea676.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. Assume wlog that the player goes first in <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. We have the player start playing in <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>, then copy this move into <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_bc4947b04e7ea496037197a0809d11da55422409.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. Whatever they play in response, we go to <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_c7ea9bf60399dae5f34e826d4f1a8ecc0a4a6030.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_8964387a593f0de3a11f74446080e77066b64d2e.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> is provable, but <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_1e6005344886e5204b0108a5d3703657626bc38c.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> isn't.

So far, we've only looked at the two forms of conjunction. There is also two forms of disjunction, given simply by <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_332bfcca70f28fa5e5f48759a18df39665e5212c.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>, <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_b6e991d197297486fb377f8b2f7a71d7df9a0212.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. We could restate the above discussion as "<object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_67c4e3051ed267d97a37f2525aea5d5118ea2b30.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_b995dd0c8fb474bb2182224fbeab583cfacd8a49.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>, where both <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_82b14cc542ef22dba87993b12dd6d6d310f947d7.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> and <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a33a2d6e25b53b1938ccfc129cc9544b9628375b.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> are multisets. We can interpret such a sequent as asserting the existence of a strategy for the game <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_3415bd826597d728f3ee0489dbfa6c59ba7f9f84.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_4e379c847bf45683840230c2b93ef93f20c24be8.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> is not a provable sequent.

To prove this sequent, we would want a strategy for <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_404495e2a205415c8b6fc83ff9a40bce2b9ef3c4.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. We can think of this again in the case where <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_a7d92cc965ef976b84b9370a6f429d98bc7d2fb9.svg" class="org-svg"> Sorry, your browser does not support SVG.</object> 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 <object type="image/svg+xml" data="/ox-hugo/20200414104653-blog_posts_afddd41d83bccf2bec783f5e313950c75d967c4b.svg" class="org-svg"> Sorry, your browser does not support SVG.</object>. 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.