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.)
