Tame pairs of transseries fields

TL;DR

This paper studies pairs of models of transseries fields that are tame, showing they are complete, model complete, and have quantifier elimination, with implications for differential fields like hyperseries and surreal numbers.

Contribution

It establishes the model-theoretic properties of tame pairs of transseries fields, including completeness, model completeness, and quantifier elimination, extending to differential-Hensel-Liouville closed pre-H-fields.

Findings

The theory of tame pairs is complete and model complete.

Quantifier elimination is achieved with additional predicates and a standard part map.

Small models are purely stably embedded, including the constant field.

Abstract

This paper concerns pairs of models of the theory of the differential field of logarithmic-exponential transseries that are tame as a pair of real closed fields. That is, the smaller model is bounded inside the larger model and there exists a standard part map. This covers for instance the differential fields of hyperseries or surreal numbers or maximal Hardy fields equipped with suitable enlargements of the differential field of transseries. The theory of such pairs is complete and model complete in a natural language and it has quantifier elimination in the same language expanded by two predicates and a standard part map. Additionally, the smaller model is purely stably embedded in the pair, and hence so is the constant field. More generally, we study differential-Hensel-Liouville closed pre-$H$-fields, i.e., pre-$H$-fields that are differential-henselian, real closed, and closed under exponential integration, equipped with lifts of their differential residue fields, and establish similar results in that setting relative to the differential residue field.