Interpreting Arithmetic in the First-Order Theory of Addition and Coprimality of Polynomial Rings

Abstract

We study the first-order theory of polynomial rings over a GCD domain and of the ring of formal entire functions over a non-Archimedean field in the language {1,+} We show that these structures interpret the first-order theory of the semi-ring of natural numbers. Moreover, this interpretation depends only on the characteristic of the original ring, and thus we obtain uniform undecidability results for these polynomial and entire functions rings of a fixed characteristic. This work enhances results of Raphael Robinson on essential undecidability of some polynomial or formal power series rings in languages that contain no symbols related to the polynomial or power series ring structure itself.