: We give axiomatizations and prove quantifier elimination theorems for first-order theories of unramified valued fields with an automorphism having a close interaction with the valuation. We achieve an analogue of the classical Ostrowski theory of pseudoconvergence. In the outstanding case of Witt...
. We give examples of fields elementarily equivalent to a given finite extension of the p-adic numbers but not containing a subfield of finite codimension elementarily equivalent to the p-adics.