Relative decidability and definability in henselian valued fields

TL;DR

This paper explores the definability and decidability in henselian valued fields of characteristic 0, providing a partitioning approach and applications to quantifier elimination and definable sets.

Contribution

It introduces a novel definable partition in henselian valued fields that facilitates a relative quantifier elimination and a new way to represent definable sets.

Findings

Constructive quantifier elimination relative to leading terms

Definable sets as pullbacks of sets in leading terms

Partitioning enables computation of polynomial leading terms

Abstract

Let K be a henselian valued field of characteristic 0. Then K admits a definable partition on each piece of which the leading term of a polynomial in one variable can be computed as a definable function of the leading term of a linear map. Two applications are given: first, a constructive quantifier elimination relative to the leading terms, suggesting a relative decision procedure; second, a presentation of every definable subset of K as the pullback of a definable set in the leading terms subjected to a linear translation.