Axiomatizing the existential theory of Fq((t))

TL;DR

This paper provides an axiomatization and decision procedure for the existential theory of equicharacteristic henselian valued fields with a uniformizer, under weak resolution of singularities assumptions, extending previous algorithms.

Contribution

It introduces a new axiomatization and decision algorithm for the existential theory of certain valued fields, requiring weaker assumptions than prior methods.

Findings

Axiomatization of the existential theory relative to the residue field

Decision algorithm under weak resolution hypotheses

Comparison with and extension of Denef and Schoutens' algorithm

Abstract

We study the existential theory of equicharacteristic henselian valued fields with a distinguished uniformizer. In particular, assuming a weak consequence of resolution of singularities, we obtain an axiomatization of - and therefore an algorithm to decide - the existential theory relative to the existential theory of the residue field. This is both more general and works under weaker resolution hypotheses than the algorithm of Denef and Schoutens, which we also discuss in detail. In fact, the consequence of resolution of singularities our results are conditional on is the weakest under which they hold true.