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:
- P(A) = It is White's move and White has not yet won in position A.
- R(A, B) = Position B legally follows in one move from position A.
- Q(A, 0) = P(A)
- Q(A, t) = for all B: (R(A, B) -> there exists C: R(B, C) -> Q(C, t - 1))
- 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.