AN EXISTENTIAL O-DEFINITION OF Fq[[t]] IN Fq((t))

We show that the valuation ring F-q [[t]] in the local field F-q ((t)) is existentially definable in the language of rings with no parameters. The method is to use the definition of the henselian topology following the work of Prestel-Ziegler to give an there exists-F-q-definable bounded neighbouhood of 0. Then we "tweak" this set by subtracting, taking roots, and applying Hensel's Lemma in order to find an there exists-Fq-definable subset of F-q [[t]] which contains tF(q) [[t]]. Finally, we use the fact that Fq is defined by the formula x(q) x = 0 to extend the definition to the whole of F-q [[t]] and to rid the definition of parameters. Several extensions of the theorem are obtained, notably an there exists-empty set-definition of the valuation ring of a nontrivial valuation with divisible value group.