Definable constructions in o-minimal geometry Recently I've been working with o-minimal expansions of $(\mathbb{R},\times,+)$, and I want to work "internally" to the language of o-minimal sets instead of working with "definable families".
This is for a simple practical reason: I can't explain ANYTHING in the definable family formalism to my combinatorialist colleagues, since they haven't had the luxury of being fully saturated in the Yoneda-lemma style Grothendieckian constructions certain (algebraic) geometers have become accustomed to.
However I've had great success with an alternate formalism.
Some natural constructions seem to "escape" this formalism, so I break the formalism in a consistent way to accommodate these constructions, making me think there's a formalism which encompasses what I'm doing. This seems like something that might be standard in model theory, and I am wondering if anyone can help.
The questions are at the end after some background.
Current Setup: Complexity Formalism
I have a finite collection of functions $f_1,\ldots,f_r$ of various arities $f_i:\mathbb{R}^{e_i}\to \mathbb{R}$, and I'm supposing that they generate an o-minimal structure, meaning that any first order formula with one free variable involving these functions and $+,\times$ defines a subset of $\mathbb{R}$ which is a finite union of points and intervals.
A definable set $S_\phi\subset \mathbb{R}^d$ is defined by a first order formula $\phi$ with $d$ free variables.
Say that the "complexity" of a formula $\phi$ is the number of symbols used in its definition (with real constants counting as 1 symbol).
I want to work with the notion of complexity in place of where theorems would typically generalize via "definable families", replacing $A\subset \mathbb{R}^n$ with a statement about the fibers of a map $\mathbb{R}^n\times \mathbb{R}^m\to \mathbb{R}^m$. (I don't forbid that definable families appear in constructions, just in the main use cases for extending theorems from single definable sets to families of definable sets).
Example comparing formalisms
Let's consider a simple example: A definable subset $A\subset \mathbb{R}^n$ has finitely many connected components. We want to generalize this to statements about how the number of connected components varies with $A$.
In the definable families formalism, this is generalized to say that if we have a subset $A'\subset \mathbb{R}^n\times \mathbb{R}^m$, then the number of components of the fibers of $\pi\times id|_{A'}$ are uniformly bounded.
In the complexity formalism, this is generalized to say that the number of connected components of $A$ is bounded in terms of the complexity of $A$.
These are actually completely equivalent: In one direction, the fibers of $\pi\times id|_{A'}$ are of bounded complexity in terms of $A'$ since the fiber over $x$ is obtained by intersecting $A'$ with $\mathbb{R}^n\times \{x\}$. In the other direction, for a fixed formula type (say two formulas have the same type if they only differ in the real constants used) take the "universal family" for that formula type, where $\mathbb{R}^m$ parametrizes all possible values of these $m$ constants. Then since there were only finitely many functions $f_1,\ldots,f_r$, there are only finitely many formula types of a given complexity.
Although they're equivalent, as long as I start with a definable set and only do "allowed" things to it, I'm always guaranteed to have bounded complexity. This means I can bound my quantities at the end of a proof in terms of the inputs at the beginning, without needing to drag along auxilliary definable families throughout.
Problem
After taking basic theorems in o-minimal geometry and phrasing them in terms of complexity, 99% of the time I can work without even knowing that my sets are o-minimal, and at my leisure I can access the "bounded complexity" oracle to plug into some theorem like the one above to get that some geometric quantity is bounded whenever I want.
However, although this might be fine to access the oracle to get natural numbers occasionally (breaking the abstraction slightly), I keep stumbling with theorems such as "Given a map $f:A\to B$, the set $\{x\in B:\dim f^{-1}(x)=k\}$ is a definable subset of $B$ of bounded complexity."
If I have two linear maps $f,g:A\to \mathbb{R}^n$ and the set
\begin{align}
\big\{x\in \mathbb{R}^n:\ &\dim f^{-1}(x)=k\text{ and }\\ &\big(\text{# of connected components of }g^{-1}(x)\big)=\ell\big\},
\end{align}
then I can apply the above two theorems in succession to bound the set's complexity in terms of $A$. But this process was not automatic --- I couldn't just use the fact that the formula was syntactically correct to deduce the conclusion.
Questions
Let $\mathcal{D}(\mathbb{R}^n)$ be the definable subsets of $\mathbb{R}^n$.
Consider the second order functions
\begin{align}
\text{complexity}&:\ \mathcal{D}(\mathbb{R}^n)\to \mathbb{N}\\
\dim&:\ \mathcal{D}(\mathbb{R}^n)\to \mathbb{N}\\
\#\text{ of connected components}&:\ \mathcal{D}(\mathbb{R}^n)\to \mathbb{N}\\
\end{align}
Consider also the constructions
\begin{align}
i^{th}\text{ simplex in a definable triangulation}&:\ \mathcal{D}(\mathbb{R}^n)\to \mathcal{D}(\mathbb{R}^n)\\
f^{-1}&:\ \phantom{\mathcal{D}(}\mathbb{R}^m\to \mathcal{D}(\mathbb{R}^n)
\end{align}
where $f$ is a definable function from $\mathbb{R}^n\to \mathbb{R}^m$.
My questions are:

*

*Is there a metatheorem that any formula
$$\Phi:\mathcal{D}(\mathbb{R}^n)\to \mathcal{P}(\mathbb{R}^n)$$
will always produce definable sets if it
combines these second-order functions and constructions with the usual first-order syntax for the $o$-minimal structure in a syntactically correct way?

*Is there a metatheorem that any similarly constructed formula
$$\Phi':\mathcal{D}(\mathbb{R}^n)\to \mathbb{N}$$
has an output bounded by a function of the input's complexity?

*What axioms would further constructions have to satisfy for these metatheorems to hold?

 A: I will expand my comment into at least a partial (but for me quite illuminating answer). As I’ve mentioned in the comments, the question of complexity in o-minimality was recently adressed in an ICM talk by Gal Binyamini and Dmitri Novikov, and then formally introduced together with Benny Zack in the following preprint https://arxiv.org/abs/2209.10972.
Unfortuantely, it is impossible to control connected components using your notion of complexity. As far as I understand, this is because $\mathbb{R}_{an}$ is too big (In the words of a renowned expert who shall remain anonymous “$\mathbb{R}_{an}$ is a POC”) , and you can’t control say the zeros of an analytic function, in general. See the example in section 1.4.2 from the attached preprint for more details. Another problem is that even if you manage to get bounds in terms of the OP’s suggested complexity, it will be exponential or even doubly exponential, even in important structures coming from geometry, making it problematic at least for a certain range of applications.
Notable exeptions are the semialgebraic structure and the various Pfaffian structures, where you have two parameters controlling complexity - “format” and “degree”. For a semialgebraic set, the format is its ambient dimension, and its degree is the sum of the degrees of a system defining the set. For (sub) Pfaffian sets the definition is similar. And in general, format is very similar to the definition you gave for complexity. It is important to distinguish between format and degree, as typically bounds on connected components (such as in the work of Khovanskii) are exponentiall or even doubly exponential in the format, but polynomial in the degree.
Actually, the above two structures are the only known examples of “sharply o-minimal structures”, o-minimal structures satisfying the axioms put forward by Binyamini, Novikov and Zack. In these axioms, definable sets have format and degree, and there are axioms about the format and degree of various (logical) set-theoretic operations. Additionally, there is an axiom saying that if a definable subset of the line has format F and degree D, then it has $poly_{F}(D)$ connected components. From this (and some other things) I believe they answer all of your questions (they have a section about triangulations), at least in the context of sharply o-minimal structures.
