Models of $VTC^0$ as exponential integer parts

TL;DR

This paper demonstrates that models of the bounded arithmetical theory VTC^0 can be embedded as exponential integer parts within real-closed exponential fields, revealing deep structural properties of these models.

Contribution

It establishes that models of VTC^0 are exponential integer parts of real-closed exponential fields, linking bounded arithmetic with real algebraic geometry.

Findings

Models of VTC^0 are recursively saturated in a rich language.

Every countable model of VTC^0 is an exponential integer part of a real-closed exponential field.

The results connect bounded arithmetic with the structure of real-closed exponential fields.

Abstract

We prove that (additive) ordered group reducts of nonstandard models of the bounded arithmetical theory $\mathsf{VTC^0}$ are recursively saturated in a rich language with predicates expressing the integers, rationals, and logarithmically bounded numbers. Combined with our previous results on the construction of the real exponential function on completions of models of $\mathsf{VTC^0}$, we show that every countable model of $\mathsf{VTC^0}$ is an exponential integer part of a real-closed exponential field.