In the early 90s, I adapted Lorenzen's game semantics of logic to give a "geometrical" description of what is going on during cut elimination (interaction between two strategies), obtaining a proof of termination which I believe is essentially different from the one of Gentzen. This introduced the notion of pointer sequence and visibility, which was used later in game semantics of simply typed lambda calculus. The termination argument, published in the proceeding of CLICS 92, was used in P.-L. Curien's paper Abstract Bohm trees , MSCS 8 (1998), to present a general termination argument about abstract machine evaluation of lambda terms (it is not known yet if there is a more direct argument for this termination result).

The same argument was then used later in a paper of P. Clairambault and R. Harmer on Totality in Arena Games and later as a key result for compositional higher-order modal checking. See also the comment by Dominic Hughes and the course by Stefano Berardi. See also the following paper by Hugo Herbelin explaining connections between sequent calculus and Lorenzen's notion of games.

This game interpretation was suggested by Bernays' presentation of Gentzen's first (unpublished) consistency proof of arithemtic. Tait also found independently a similar interpretation also inspired by Bernays' presentation. As said above, what I think is new here is that it provides a proof of termination of cut elimination different from the one of Gentzen.

Here is the first occurence of the idea, sent to the TYPES mailing list in December 1991. The argument is by induction on the depth of the cut formula, but actually defines a "cut-protocol" which would work even if the formula is not well-founded.

This interpretation has been used by F. Aschieri in this paper where he provides a remarkable refinement of Gentzen's bounds for cut-elimination: the complexity depends on the depth of backtracking of the two interacting strategies. See also the following presentation. Here are some older references.

- An introductory paper (June 91) where I try to describe the problem: how to get a termination proof for cut-elimination by a direct "geometric" description of what is going on, using game semantics

- The original article (March 92) describing interaction between two strategies that can backtrack. (It was published in a much revised form.) Here is a version with slides (March 92).

- The published version (accepted March 93, published in 95) of the previous paper.

I tried to present a general survey in particular, I mention S. Berardi's discovery that the notion of visibility can be extended for infinite games. My question about complexity was solved later by the work of Aschieri mentionned above.

Stefano Berardi wrote also some description of this approach with more references.

One can also generalize the game to allow the strategy to play with functions, that are thought of as stating general laws that can be refined by interaction. One gets in this way a natural computational interpretation of dependent choice with classical logic. This was actually Spector's starting point, and similar attempts can be found in the notebooks of Gödel. Using this game semantics, I suggested a realizability interpretation of countable choice. The following paper is an example of what can be done in this direction.

Last modified: Fri Sep 13 22:08:32 MET DST 2002