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.