Let $L$ be a first-order language and $M$ be an $L$-structure. Let $D \subseteq M^n$ . Let us say $D$ is definable in $M$ if for some finite set (possibly empty) $A=\{a\_1,...,a\_m\} \subseteq M$ and some formula $\psi[x\_1,...,x\_n,y\_1,...,y\_m]$ , $D=\{(b\_1,...,b\_n)\in M^n : M\vDash \psi[b\_1,...,b\_n,a\_1,...,a\_m] \}$.


(i.e. $D$ is definable by a finite set of parameters according to this definition 
<https://en.wikipedia.org/wiki/Definable_set> ). 


Now consider the first order theory of commutative rings. Take $M=\mathbb C[[X]]$ (the formal power series ring with complex coefficients) .


My questions are : Is $\mathbb C$ definable in $\mathbb C[[X]]$ ? Is $\mathbb C[X]$ definable in $\mathbb C[[X]]$ 



Are $\mathbb C$ , $\mathbb C[X]$ definable in $\mathbb C[[X]]$?
Emil's idea about quantifier elimination is a good one.


The paper "Model Theory of valued fields" by Raf Cluckers cites the thesis "Quelques propriétés des corps valués" by F. Delon, which I wasn't able to find online, for the claim that the field $\mathbb C((t))$ admits quantifier elimination for the language of Macintyre which consists of the language of field theory, a symbol for elements of the valuation ring $\mathbb C[[t]]$, and a symbol for $n$th powers. Thus any set definable in your sense is definable, without quantifiers, in this language.


It is clear that any set definable in this language has only finitely many isolated points and therefore cannot be $\mathbb C$ or $\mathbb C[x]$.


