If Artemov denies that a statement like $S$ is talking about the number 114 being a sum of cubes, then how does anything stated and proved in PA prove anything about the real world?

@LucGuyot I was not familiar with Nagata's criterion. It is very convenient in this setting, and streamlines things. Thanks!

@JesseElliott Thanks for that reference. Lemma 11.1 is quite close to what we want.

@EmilJeřábek Thanks for that example. I recently came up with a slightly different nastiness, so I'm thinking that there may not be any pretty structure theorem.

I don't understand that recent preprint. Namely, I don't see how it answers the question: How do we tell whether a zero $\gamma$ of $\zeta$ really lies on the critical line, or could be part of a pair of zeros slightly off the critical line? This issue needs to addressed in the proof of Lemma 3 (first paragraph on page 7, where we are given a priori access to the knowledge that $\gamma$ lies on the critical lie).

It turns out that Mathematica has a satisfiability solver "SatisfiableQ" which works well for the problem.

Assume $|R|=\mathbb{N}$. Supposing a player has decided on a strategy, then that player could supplement that strategy with an extra step, where if $(r,s)$ is colored, and $(r',s)$ is uncolored with $r'<r$, then they also color $(r',s)$. This extra step cannot hurt them in any way. So, we may assume that both players follow this extra supplement. So, rather than color random finite subsets, they both color consecutive blocks. In other words, the coloring in each column $R\times \{s\}$ is determined by a list of integers. This suggests some sort of connection to the axiom of determinacy.

@LajosSoukup That is exactly the kind of thing I was looking for. Do you have a reference?

@j.p. No idea. I'm planning to work with hundreds of polynomials in hundreds of variables. I don't expect this is too big for most systems.

Colin McQuillen posted an answer over on stack exchange.

@JeremyRickard Ah, so we take the commutative monoid generated by two elements $a,b$, subject to the single relation $a+a=b+b+b$. Taking $R$ to be the endomorphism ring of the projective module corresponding to $a$, and taking $S$ to be the endomorphism ring of the projective module corresponding to $b$, we are done (because, clearly, no element $c$ exists with $6c=2a=3b$).