Decidability questions for a ring of Laurent polynomials

摘要

We prove that the additive structure of the ring of Laurent polynomials augmented by the predicate symbol P, where P(x) if and only if x is a power of t, is decidable. We also prove that the first-order theory of the previous structure together with the relation | _t, where x| _ty if and only if xs∈Zy=x{dot operator}ts, is undecidable.