On the undecidability of power series fields

Abstract

REMARK. Malcev [1] obtained special cases of this result. PROOF. It suffices to show that the valuation subring A = F[ [T]] is elementarily definable in F((T)) [3, Sec. 6]. Fix m> 1 such that char(F) tm. An idea in J. Robinson [3] shows that A is definable in terms of T:A=the set of x such that 2y[ym=l+Txml. By compounding this idea and another trick we can get rid of T: A =the set of x such that aw yVUVxVlVx2 azVylVy2 [(zm =1 +Wxe JXVYi 1 +wX1 Vy2 5 1 +WX2)Aum5zWAYm=1+WXml. Indeed, this follows from the fact that A =UwcGAA, where A =wthe set of x such that By [yn =1 +wXm], if G C F((T)) has the following properties: (1) TCG; (2) for each wCG, Aw is closed under multiplication and its elements have poles of bounded order. (1) shows that UWEG AWDA while (2) gives the reverse inclusion.