Buechi's problem asked whether a surface of a specific type, defined over the rationals, has integer points other than some known ones. A consequence of a positive answer would be the following strengthening of the negative answer to Hilbert's tenth problem: the positive existential theory of the rational integers in the language of addition and a predicate for the property 'x is a square' would be undecidable. Despite some progress, including a conditional positive answer (pending on conjectures of Lang), Buechi's problem remains open. In this article we prove an analogue of Buechi's problem in rings of polynomials of characteristic either 0 or p ≥ 13. As a consequence we prove the following result in Logic: Let F be a field of characteristic either 0 or ≥ 17 and let t be a variable. Let R be a subring of F[t], containing the natural image of Z[t] in F[t]. Let L_t be the first order language which contains a symbol for addition in R, a symbol for the property 'x is a square in F[t]' and symbols for multiplication by each element of the image of Z[t] in F[t]. Then multiplication is positive-existentially definable over the ring R, in the language L_t. Hence the positive-existential theory of R in L_t is decidable if and only if the positive-existential ring-theory of R in the language of rings, augmented by a constant-symbol for t, is decidable.
展开▼