Model completeness for finite extensions of p-adic fields

This is joint work with Angus Macintyre.

We prove that the first-order theory of a finite extension of the field of p-adic numbers is model-complete in the language of rings, for any prime p.

To prove this we prove universal definability of the valuation rings of such fields using work of Cluckers-Derakhshan-Leenknegt-Macintyre on existential

definability, quantifier elimination of Basarab-Kuhlmann for valued fields in a many-sorted language involving higher residue rings and groups,

a model completeness theorem for certain pre-ordered abelian groups which generalize Presburger arithmetic (we call finite-by-Presburger groups),

and an interpretation of higher residue rings of such fields in the higher residue groups.