Return to Answer

Many of us are familiar with the White to mate in 3 variety of chess problems, and we may consider the natural analogue in infinite chess. Thus, we refine the winning-position problem, which asks whether a designated player has a winning strategy from a given position, to the mate-in-$n$ problem, which asks whether a designated player can force a win in at most $n$ moves from a given finite position. (And note that as discussed in Johan Wästlunds's question checkmate in $\omega$ moves?, there are finite winning positions in infinite chess which are not mate-in-$n$ for any finite $n$.) Even so, the mate-in-$n$ problem appears still to be very complicated, naturally formulated by assertions with $2n$ many alternating quantifiers: there is a move for white, such that for every black reply, there is a countermove by white, and so on. Assertions with such quantifier complexity are not generally decidable, and one cannot expect to search an infinitely branching game tree, even to finite depth. So one might naturally expect the mate-in-$n$ problem to be undecidable.

Many of us are familiar with the White to mate in 3 variety of chess problems, and we may consider the natural analogue in infinite chess. Thus, we refine the winning-position problem, which asks whether a designated player has a winning strategy from a given position, to the mate-in-$n$ problem, which asks whether a designated player can force a win in at most $n$ moves from a given finite position. (And note that as discussed in Johan Wästlunds's question checkmate in $\omega$ moves?, there are finite winning positions in infinite chess which are not mate-in-$n$ for any finite $n$.) Even so, the mate-in-$n$ problem appears still to be very complicated, naturally formulated by assertions with $2n$ many alternating quantifiers: there is a move for white, such that for every black reply, there is a countermove by white, and so on. Assertions with such quantifier complexity are not generally decidable, and one cannot expect to search an infinitely branching game tree, even to finite depth. So one might naturally expect the mate-in-$n$ problem to be undecidable.

Many of us are familiar with the White to mate in 3 variety of chess problems, and we may consider the natural analogue in infinite chess. Thus, we refine the winning-position problem, which asks whether a designated player has a winning strategy from a given position, to the mate-in-$n$ problem, which asks whether a designated player can force a win in at most $n$ moves from a given finite position. (And note that as discussed in Johan Wästlunds's question checkmate in $\omega$ moves?, there are finite winning positions in infinite chess which are not mate-in-$n$ for any finite $n$.) Even so, the mate-in-$n$ problem appears still to be very complicated, naturally formulated by assertions with $2n$ many alternating quantifiers: there is a move for white, such that for every black reply, there is a countermove by white, and so on. Such kinds of assertions are not generally decidable, and one cannot expect to search an infinitely branching game tree, even to finite depth. So one might naturally expect the mate-in-$n$ problem to be undecidable.

Despite this, Philipp Schlicht and I have proved that the mate-in-n problem of infinite chess is computably decidable, and uniformly so. We have just submitted this article to the CiE 2012, and I hope to speak on it there in June.

J. D. Hamkins and P. Schlicht, "The mate-in-n problem of infinite chess is decidable," 10 pages, arxiv pre-print, submitted to CiE 2012.

Abstract. Infinite chess is chess played on an infinite edgeless chessboard. The familiar chess pieces move about according to their usual chess rules, and each player strives to place the opposing king into checkmate. The mate-in-$n$ problem of infinite chess is the problem of determining whether a designated player can force a win from a given finite position in at most n moves. A naive formulation of this problem leads to assertions of high arithmetic complexity with $2n$ alternating quantifiers---there is a move for white, such that for every black reply, there is a move for white, and so on. In such a formulation, the problem does not appear to be decidable; and one cannot expect to search an infinitely branching game tree even to finite depth. Nevertheless, the main theorem of this article, confirming a conjecture of the first author and C. D. A. Evans, establishes that the mate-in-$n$ problem of infinite chess is computably decidable, uniformly in the position and in $n$. Furthermore, there is a computable strategy for optimal play from such mate-in-$n$ positions. The proof proceeds by showing that the mate-in-$n$ problem is expressible in what we call the first-order structure of chess $\frak{Ch}$, which we prove (in the relevant fragment) is an automatic structure, whose theory is therefore decidable. Unfortunately, this resolution of the mate-in-$n$ problem does not appear to settle the decidability of the more general winning-position problem, the problem of determining whether a designated player has a winning strategy from a given position, since a position may admit a winning strategy without any bound on the number of moves required. This issue is connected with transfinite game values in infinite chess, and the exact value of the omega one of chess $\omega_1^{\rm chess}$ is not known.

Many of us are familiar with the White to mate in 3 variety of chess problems, and we may consider the natural analogue in infinite chess. Thus, we refine the winning-position problem, which asks whether a designated player has a winning strategy from a given position, to the mate-in-$n$ problem, which asks whether a designated player can force a win in at most $n$ moves from a given finite position. (And note that as discussed in Johan Wästlunds's question checkmate in $\omega$ moves?, there are finite winning positions in infinite chess which are not mate-in-$n$ for any finite $n$.) Even so, the mate-in-$n$ problem appears still to be very complicated, naturally formulated by assertions with $2n$ many alternating quantifiers: there is a move for white, such that for every black reply, there is a countermove by white, and so on. Assertions with such quantifier complexity are not generally decidable, and one cannot expect to search an infinitely branching game tree, even to finite depth. So one might naturally expect the mate-in-$n$ problem to be undecidable.

Despite this, the mate-in-n problem of infinite chess is computably decidable, and uniformly so. Dan Brumleve, myself and Philipp Schlicht have just submitted an article establishing this to the CiE 2012, and I hope to speak on it there in June.

D. Brumleve, J. D. Hamkins and P. Schlicht, "The mate-in-n problem of infinite chess is decidable," 10 pages, arxiv pre-print, submitted to CiE 2012.

Abstract. Infinite chess is chess played on an infinite edgeless chessboard. The familiar chess pieces move about according to their usual chess rules, and each player strives to place the opposing king into checkmate. The mate-in-$n$ problem of infinite chess is the problem of determining whether a designated player can force a win from a given finite position in at most n moves. A naive formulation of this problem leads to assertions of high arithmetic complexity with $2n$ alternating quantifiers---there is a move for white, such that for every black reply, there is a counter-move for white, and so on. In such a formulation, the problem does not appear to be decidable; and one cannot expect to search an infinitely branching game tree even to finite depth. Nevertheless, the main theorem of this article, confirming a conjecture of the first author and C. D. A. Evans, establishes that the mate-in-$n$ problem of infinite chess is computably decidable, uniformly in the position and in $n$. Furthermore, there is a computable strategy for optimal play from such mate-in-$n$ positions. The proof proceeds by showing that the mate-in-$n$ problem is expressible in what we call the first-order structure of chess $\frak{Ch}$, which we prove (in the relevant fragment) is an automatic structure, whose theory is therefore decidable. Unfortunately, this resolution of the mate-in-$n$ problem does not appear to settle the decidability of the more general winning-position problem, the problem of determining whether a designated player has a winning strategy from a given position, since a position may admit a winning strategy without any bound on the number of moves required. This issue is connected with transfinite game values in infinite chess, and the exact value of the omega one of chess $\omega_1^{\rm chess}$ is not known.

J. D. Hamkins and P. Schlicht, "The mate-in-n problem of infinite chess is decidable," 10 pages, submitted to CiE 2012.

J. D. Hamkins and P. Schlicht, "The mate-in-n problem of infinite chess is decidable," 10 pages, arxiv pre-print, submitted to CiE 2012.

The solution can also be cast in terms of Presburger arithmetic, in a manner close to Dan Brumleve's answer to this question. Namely, once we restrict to a given collecton of pieces $A$, then we may represent all positions using only pieces in $A$ as a fixed-length tuple of natural numbers, and the elementary movement, attack and in-check relations are expressible for this representation in the language of Presburger arithmetic, essentially because the distance pieces---rooks, bishops and queens---all move on straight lines whose equations are expressible in Presburger arithmetic. (There is no need to handle sequence coding in general, since the number of pieces does not increase during play.) Since the mate-in-$n$ problem is therefore expressible in Presburger arithmetic, it follows that it is decidable.