Characterizing decidability in a quasianalytic setting

TL;DR

This paper establishes that the decidability of the first-order theory of certain quasianalytic structures depends precisely on the decidability of two specific oracles related to approximation and geometric decision problems.

Contribution

It introduces a framework linking decidability to approximation and geometric oracles in quasianalytic expansions of the real field, and develops an effective local resolution of singularities.

Findings

Decidability of the theory is equivalent to oracle decidability.

Develops an effective local resolution of singularities.

Proves new theorems about the model theory of quasianalytic structures.

Abstract

Let $\RR_S$ denote the expansion of the real ordered field by a family of real-valued functions $S$, where each function in $S$ is defined on a compact box and is a member of some quasianalytic class which is closed under the operations of function composition, division by variables, and implicitly defined functions. It is shown that the first order theory of $\RR_S$ is decidable if and only if two oracles, called the approximation and precision oracles for $S$, are decidable. Loosely stated, the approximation oracle for $S$ allows one to approximate any partial derivative of any function in $S$ to within any given error, and the precision oracle for $S$ allows one to decide when a manifold $M\subseteq\RR^n$ is contained in a coordinate hyperplane $\{x\in\RR^n : x_i = 0\}$ when one is given $i\in\{1,\ldots,n\}$ and a system of equations which defines $M$ nonsingularly, where the functions occurring in the equations are rational polynomials of the coordinate variables $x = (x_1,\ldots,x_n)$ and the partial derivatives of the functions in $S$. A key component of the proof is the development of a local resolution of singularities procedure which is effective in the approximation and precision oracles for $\S$, and in the course of proving our main theorem, numerous theorems about the model theory of such structures $\RR_S$ are also proven.