Uniform existential interpretation of arithmetic in rings of functions of positive characteristic (Q2449847)

The authors show that there are positive existential formulas \(\varphi_1\) and \(\varphi_2\) such that for every field \(\mathbb F\) of positive characteristic \(p\), \(\varphi_1\) defines in \(\mathbb F[z]\) (and \(\varphi_2\) in \(\mathbb F(z)\)) the formula \(\exists s \,\,y = x^{p^s} \vee x = y^{p^s}\). They also show that there is a positive existential formula over the language \(\{0, 1,+,R\}\) which is independent of \(p\) and defines the multiplication in the structure \((\mathbb N, 0, 1,+, |_p)\) where \(y|_px\) means that there is an \(s\) such that \(y = p^sx\). Using this machinery (which is based on a generalization of Büchi's problem in functions over fields of finite characteristic), they prove that there is no algorithm to decide whether or not a system of polynomial equations over \(\mathbb Z[z]\) has solutions in all but finitely many polynomial rings \(\mathbb F_p[z]\). Analogous consequences are deduced for the rational function fields \(\mathbb F_p(z)\) for languages with a predicate for the valuation ring.