One can prove Elimination of Quantifiers of ACVF finding an extension of any partial embedding of a model $K$ into a $|K|^+$ Saturated one using the language $\mathcal{L} = ( 0,1,+,*, U, \mid )$. In this Language $U$ is the unary predicate standing for the Valuation Ring of the model, and $\mid $ is a binary relation such that $x\mid y \leftrightarrow \exists z\in U \ x*z=y$. How do you prove the completeness of this theory in that language?
1 Answer
Just like with algebraically closed fields, for completeness you need to specify the characteristic of the field and the characteristic of the residue field.
There is a general trick if you have a theory $T$ with quantifier elimination and a structure $A$ that is embedded in every model of $T$, then $T$ is complete. Let $M$ and $N$ be models of $T$ and let $\phi$ be any sentence. There is a quantifier free sentence $\psi$ that is equivalent to $\phi$ in models of $T$. But, since $\psi$ is quantifier free, $$M\models \psi\Leftrightarrow A\models\psi\Leftrightarrow N \models\psi.$$ Thus $M\models\phi\Leftrightarrow N\models \phi$.
Now, suppose you are looking at characteristic 0 fields with characteristic p residue field. The rationals with the p-adic valuation are a substructure of any model of ACVF of characteristic $0$ with characteristic $p$ residue field.