Independence results in formal topology

We analyze a family of games by using formal topology as a tool. In order to win any game in the family one has to find a sequence of moves leading to one of the final states for that game. Thus, two results are relevant to the topic: to find terminating strategies and/or to show that every strategy is terminating. We will show that the language of formal topology can be useful to represent in a topological framework both of the problems, and in particular that the property of termination of all the strategies for a game is equivalent to the discreteness of a suitable formal space. Finally, we will provide some examples of games which are terminating according to any strategy, that is, such that the associated formal spaces are discrete, but the first order formulas expressing such a discreteness cannot be proved in Peano Arithmetic.

► The problem of termination for a countable family of games is analyzed.
► The language of formal topology is shown to be suitable to represent such a problem.
► Termination is shown to be equivalent to discreteness of a suitable topological space.
► All our games are terminating and so the associated spaces are discrete.
► But such a discreteness is independent from first order arithmetic.