As a unified approach if we have an ( read any) infinite board game described as $\mathcal{G}$ using a particular axiom set A..

can a sentence be devised in A which automatically answers the basic questions for the game ie

  • Won in k moves given any state of the game
  • Draw in l moves given any state of the game
  • Unending play/Stalemate

    Let the axiom set itself is a decidable theory say Presburger arithmetic; so the question of un-decidability does not arise.

    Also note that the board itself is an infinite one and so are the number of pieces.Physical examples if required would be infinite -- chess, 4-in-a-row, Go to name a few.

    In addition to the list above there are multiple such statements on games on infinite boards. I will try to enumerate a few just to exemplify questions which can be posed about $\mathcal{G}$

  • Is it possible to have a a pair of positions A and B, such that we can go from configuration A to B by legal moves, but not from B to A - Reversible Chess
  • Win in finite moves n in a row in $R^2$

  • $\endgroup$
    • 1
      $\begingroup$ I don't understand what you mean by "describing" a game in a weak axiomatic system like Presburger arithmetic. It would make good sense for systems like Peano arithmetic that admit coding of finite sequences and sets, but Presburger arithmetic lacks such coding ability, and this lack is crucial for decidability. $\endgroup$ Jul 4, 2013 at 15:27
    • $\begingroup$ I would say that part of what it means to "describe" a game would be that you can express the "win-in-k" and "draw-in-l" problems. But I don't extend this to the "stalemate" problem, since that is infinitary in nature over the state space, as it refers to the existence of a strategy. $\endgroup$ Jul 4, 2013 at 15:46

    1 Answer 1


    I explain in my answer to Richard Stanley's question on the decidability of infinite chess that this is precisely how Dan Brumleve, Philip Schlicht and I proved that the mate-in-$n$ problem of infinite chess is decidable. Namely, we introduced the first-order structure of chess $\frak{Ch}$, whose objects are the various positions of infinite chess and whose relations express the basic chess concepts, relating one position to another when it can be reached by a legal white bishop move, for example. In our article, The mate-in-$n$ problem of infinite chess is decidable, we prove that $\frak{Ch}$ is an automatic structure in the sense of finite automata theory, and also interpretable in Presburger arithemetic. The point now is that the mate-in-$n$ problem is expressible in this structure, and therefore any particular mate-in-$n$ question can be viewed as an assertion in the language of Presburger arithmetic. In particular, the axioms of Presburger arithmetic answer the question of whether any given finite position is mate-in-$n$ or not. And similarly it settles every instance of the drawn-in-$l$ problem.

    We don't know, however, how to express the general won-position problem or the drawn-position problem in this language, and it is an open question whether these questions are decidable.

    It seems to me that part of what it must mean to say that you have "described" a game in a system is that you are indeed able to express such concepts as the "win-in-$k$" problem and the "draw-in-$l$" problem, since these problems are expressible using only finitely many quantifiers over the state space of all positions. The "won-position" and "drawn-position" problems, however, are not finitary in nature, since they inquire about the existence of a strategy, an infinitary object. In general, winning strategies in such games can have strictly hyperarithmetic complexity, and so we do not expect them to be determined by Presburger arithmetic. In the case of infinite chess, this is still open, and one can view the situation as asking whether chess ultimately is simple or complicated.

    I find it extremely interesting to note that if the won-position problem is not decidable, then in fact there will be finite chess positions such that the question of whether they are winning or not for white will be independent of whatever background axiom system you choose to adopt. The reason is that if all such questions were provable in such a system, then we would have a decision procedure by looking for proofs.

    Lastly, let me point out that your three bullet points are not exhaustive, since a position can be a winning position for white, without it being win-in-$k$ for any particular $k$, because black in his play can ensure arbitrarily long play before ultimately losing. This is the main point of Johan Wästlund's question checkmate in $\omega$ moves, which is ultimately about the existence of transfinite game values in infinite chess. (See also my article Transfintie game values in infinite chess.)

    • 1
      $\begingroup$ We haven't tried that. What was important about chess, to do the interpretation in Presburger arithmetic, is that new pieces never come into the position (so we don't need to code arbitrary length sequences but only fixed length) and also the pieces move on straight lines whose equations are expressible in Presburger arithmetic. If there was a piece (a pterodactyl?) moving on a parabola, for example, it would break the proof. $\endgroup$ Jul 4, 2013 at 15:58

    Your Answer

    By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

    Not the answer you're looking for? Browse other questions tagged or ask your own question.