University of Cambridge

Logic
&
Semantics

Who wins infinite plays?

By Martin Hyland

Games used to model computation typically allow infinite plays which represent non-termination. When modelling proofs however one needs to know who has won (finite and) infinite plays. In traditional logic (e.g. descriptive set theory) who wins which infinite plays is given as part of the structure of the game. There is however a more interesting possibility for proof theory: one can stipulate that the player whose fault it is that the interaction has gone on for ever should lose. I shall explain how this works out in practice first in a (too) simple example and then in a serious example. I may also say a little about games and the non-degeneracy of the mu-lattice hierarchy.