### Abstract

This is a formalisation of the main result of Gale and Stewart from 1953, showing that closed finite games are determined. This property is now known as the Gale Stewart Theorem. While the original paper shows some additional theorems as well, we only formalize this main result, but do so in a somewhat general way. We formalize games of a fixed arbitrary length, including infinite length, using co-inductive lists, and show that defensive strategies exist unless the other player is winning. For closed games, defensive strategies are winning for the closed player, proving that such games are determined. For finite games, which are a special case in our formalisation, all games are closed.

### License

BSD License

### Topics

- Mathematics/Games and economics

### Session GaleStewart_Games

- MoreCoinductiveList2
- MoreENat
- MorePrefix
- AlternatingLists
- GaleStewartGames
- GaleStewartDefensiveStrategies
- GaleStewartDeterminedGames

### Depends on

- Positional Determinacy of Parity Games

### Auto-related entries

- Local Lexing
- Menger’s Theorem

## Cite

×

GaleStewart_Games-AFP

    @article{GaleStewart_Games-AFP,
      author  = {Sebastiaan J. C. Joosten},
      title   = {Gale-Stewart Games},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/GaleStewart_Games.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Apr 28, 2021 : Isabelle2021