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?
