Quantifier Elimination for Valued Fields Equipped with an Automorphism

TL;DR

This paper develops a general axiomatization and quantifier elimination for valued fields with automorphisms in residue characteristic zero, removing previous restrictive assumptions and applying to transseries fields with shift automorphisms.

Contribution

It provides the first general framework for quantifier elimination in valued fields with automorphisms without strong interaction assumptions.

Findings

Axiomatization of valued fields with automorphisms in residue characteristic zero.

Quantifier elimination achieved under minimal interaction assumptions.

Application to the transseries field with the shift automorphism.

Abstract

We provide axiomatization and relative quantifier elimination for valued fields equipped with an automorphism, in residue characteristic zero. Similar results are known under strong assumptions on the interaction between the automorphism and the valuation. We remove such assumptions and provide general treatment. As a consequence we obtain an axiomatization of the transseries field (as a valued field with an automorphism) equipped with the automorphism which sends f(x) to f(x+1).