Are $\mathbb C$ , $\mathbb C[X]$ definable in $\mathbb C[[X]]$?

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]]$

• The answer to the second question is no: pick any power series $Y = X + \ldots$, then there is an automorphism of $\mathbb{C}[[X]]$ sending $X$ to $Y$, and hence $\mathbb{C}[X]$ to $\mathbb{C}[Y]$. – Piotr Achinger Mar 1 '18 at 14:09
• @PiotrAchinger Note that the OP is interested in definability with parameters. Your argument is blocked if you take e.g. $X$ as a parameter. – Emil Jeřábek Mar 1 '18 at 15:00
• Nevertheless, I think that some kind of automorphism argument might work. In particular, since $\mathbb C$ has infinite transcendence degree, I would expect that even if you fix finitely many parameters, there should be an automorphism of $\mathbb C[[X]]$ that moves some element of $\mathbb C$ outside $\mathbb C[X]$. – Emil Jeřábek Mar 1 '18 at 15:06
• Hmm. So, that means the question is cross-posted from math.stackexchange.com/questions/2667763/… . – Emil Jeřábek Mar 1 '18 at 15:26
• There is also vast literature on quantifier elimination in henselian valued fields (or valuation rings, for that matter), which I am mostly unfamiliar with, but very likely some of it can be applied here. – Emil Jeřábek Mar 1 '18 at 15:30

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]$.
• What do you get from eliminating quantifiers in "x is the difference of two non-squares in C[[x]]"? I.e. $\exists y \in C[[x]] \exists z \in C[[x]] \forall w \in C[[x] \ x = y - z\ \&\ y \neq w^2\ \&\ z \neq w^2$. That should, at least roughly, define the elements with 0 constant term. – Matt F. Mar 7 '18 at 18:06
• @Matt F. If you want to define the elements with zero constant term, you just need to state that $X^{-1} x$ is an element of $C[[x]]$. I think this is in fact equivalent to your statement. – Will Sawin Mar 7 '18 at 18:13
• Can you explain a bit more the assertion about finitely many isolated points? Do you mean in the topology induced by the valuation? Doesn't $\mathbb{C}[X]$ have no isolated points in this topology? – Alex Kruckman Mar 9 '18 at 5:36