Edit - MathOverflow

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

Required fields*

Rev

Required fields*

Decidability of chess on an infinite board

The recent question Do there exist chess positions that require exponentially many moves to reach? of Tim Chow reminds me of a problem I have been interested in. Is chess with finitely many men on an infinite board decidable? In other words, given a position on an infinite board (say $\mathbb{Z}\times \mathbb{Z}$, though now pawn promotion is not possible) with finitely many men, say with White to move, is there an algorithm to determine whether White can checkmate Black (or prevent Black from checkmating White) against any Black defense?

Answer*

Yes, because any chess position can be translated into Presburger arithmetic.  For a fixed initial combination of piece types, let's define a position to consist of an (x, y) location for each piece as well as a bit (c) to indicate whether or not it has been captured.  Multiplication of these parameters is not required to describe the legality and the effects of any one move, so in Presburger arithmetic we can recursively define the proposition "White cannot capture Black's King in fewer than t moves starting from initial position X.", then apply the axiom schema of induction to get an expression meaning "White cannot ever checkmate starting from initial position X."  Since Presburger arithmetic is complete we will always be able to prove either this statement or its negation.

EDIT: Summary of how this is supposed to work:

1. P(A) = It is White's move and White has not yet won in position A.
2. R(A, B) = Position B legally follows in one move from position A.
3. Q(A, 0) = P(A)
4. Q(A, t) = for all B: (R(A, B) -> there exists C: R(B, C) -> Q(C, t - 1))
5. S(A) = Q(A, 0) and (for all t: Q(A, t) -> Q(A, t + 1))

This works fine at least up to line four where Q(A, t) is defined recursively.  If Q(A, t) could be defined as a predicate in Presburger arithmetic then I think line five would also work.  But this is a serious problem and maybe breaks the whole approach.

Edit Summary*

Cancel

1

$\begingroup$ Could you explain why Presburger arithmetic (which has only addition) is able to carry out this kind of encoding? The usual Goedel coding of such combinatorial operations, such as for Turing machines, would use something more like Peano Arithmetic or weakened forms. Presburger arithmetic, in contrast, cannot carry out that arithmetization, for example in the case of Turing machines, precisely because it is a decidable theory. $\endgroup$

Joel David Hamkins
– Joel David Hamkins

2010-09-05 00:04:13 +00:00
Commented Sep 5, 2010 at 0:04
1

$\begingroup$ Yes, there is induction, but only for assertions involving only addition. There is no Goedel encoding of finite sequences in Presburger arithmetic, for if there were, then its theory could not be decidable, since we could express the halting problem. $\endgroup$

Joel David Hamkins
– Joel David Hamkins

2010-09-05 00:59:47 +00:00
Commented Sep 5, 2010 at 0:59
3

$\begingroup$ Although Presburger arithmetic can prove all instances of the proof-by-induction principle that can be expressed in its (very limited) language, it cannot express definitions by recursion, such as those proposed in this answer. If definition by recursion were available, then we could use it to define multiplication and therefore have an undecidable theory. $\endgroup$

Andreas Blass
– Andreas Blass

2010-09-05 02:49:12 +00:00
Commented Sep 5, 2010 at 2:49
2

$\begingroup$ Although the inductive part of this answer is problematic, it does contain a correct account of the mate-in-n problem via Presburger arithmetic. For a fixed collection of pieces, one needn't do the Goedel coding of sequences inside the Presburger theory, because the number of pieces does not increase during play. Thus, one may represent a position with $r$ many pieces as a $3r+1$ tuple of natural numbers, in the manner Philipp Schlicht and I describe in our paper, and the movement and in-check relations are expressible in Presburger arithmetic, ...(cont'd) $\endgroup$

Joel David Hamkins
– Joel David Hamkins

2012-01-27 14:31:12 +00:00
Commented Jan 27, 2012 at 14:31
2

$\begingroup$ ...essentially because the distance pieces move on straight lines whose equations are expressible in Presburger arithmetic. Thus, the mate-in-n problem for a fixed collection of pieces is expressible in Presburger arithmetic, and hence decidable. Similarly, one can get computable strategies from such positions in this way. I voted up this answer when it was first posted, but I feel it deserves more votes. $\endgroup$

Joel David Hamkins
– Joel David Hamkins

2012-01-27 14:33:58 +00:00
Commented Jan 27, 2012 at 14:33

| Show 2 more comments

Correct minor typos or mistakes
Clarify meaning without changing it
Add related resources or links
Always respect the author’s intent
Don’t use edits to reply to the author

create code fences with backticks ` or tildes ~
```
like so
```
add language identifier to highlight code
```python
def function(foo):
print(foo)
```
put returns between paragraphs
for linebreak add 2 spaces at end
_italic_ or **bold**
quote by placing > at start of line
to make links (use https whenever possible)

<https://example.com>

[example](https://example.com)

<a href="https://example.com">example</a>
MathJax equations $\sin^2 \theta$

formatting help »
answering help »

MathJax help »