I have an elliptic curve $E$ defined over a complete discrete-valued field $K$ of characteristc $0$. the residue field $k$ is of positive characteristic $p$.
Then $E[p]=\mathbb{Z}/p\mathbb{Z} \times \mathbb{Z}/p\mathbb{Z}$.
What can I say about the height of the formal group associated to $E$?
Seems that there isn't a definition of height of formal group in characteristic $0$.
However I have another question, the formal group law $F$ for $E$ has the coefficients in $\mathcal{O}_K$ so we can consider their reduction modulo the maximal ideal of $\mathcal{O}_K$. Now assume that $E$ has a good reduction $\tilde E$. Is the formal series obtained by reduction the coefficients of $F$ a formal group law on $\tilde E$ ?
If a formal group is defined over a $p$-adic ring $\mathscr O$, with residue field $k$ of characteristic $p$, then there certainly is a pretty standard definition of the height of the formal group. It’s just the height of the $k$-series. All of this is in the very old text of Fröhlich, I think. As you expect, the height of the formal group of an elliptic curve is $1$, $2$, or $\infty$, but always finite if the reduction is good.
I’m not sure about your second question. What is “a formal group on $\tilde E\,$” ? It’s certainly true, though, that the processes (1) of taking reduction modulo the maximal ideal and (2) localization to get the formal group commute with each other.