Let $\R$ be an o-minimal expansion of the real field, and let $\R_1$ be the expansion of $\R$ by all Rolle leaves over $\R$.
Theorem
The expansion $\R_1$ of $\R$ is o-minimal.
Proof. Let $\Lambda$ be the system of all Rolle sets over $\R$; by this post, $\Lambda$ satisfies Axioms 1–7 of this post. $\qed$
Remark
The previous proof does not give any obvious quantifier simplification for definable sets. It is not known whether $\R_1$ is model complete, for instance.
Some consequences
We can iterate the process of taking Rolle leaves: define, by induction on $n>1$, the set $\la_n$ of all Rolle leaves over $\R_{n-1}$ and the expansion $\R_n$ of $\R$ as $$\R_n:= \left(\R_{n-1}\right)_1,$$ and let $\P(\R)$ be the expansion of $\R$ generated by $\la:= \bigcup_{n \in \NN} \la_n$.
By the theorem, the structure $\P(\R)$ is an o-minimal expansion of $\R$ containing all Rolle leaves in $\la$.
Exercise
Show that every Rolle leaf over $\P(\R)$ is in $\la$ and, hence, is definable in $\P(\R)$.
Definition
In view of the exercise, we call $\P(\R)$ the pfaffian closure of $\R$. (A more appropriate name would be “Rolle closure” of $\R$ but, well, history is history, even in math.)
Exercise
Every set definable in $\P(\R)$ is a finite union of diffeomorphic projections of Rolle leaves in $\la$; in particular, $\P(\R)$ is model complete.
The problem with the model completeness of $\P(\R)$ in the language $\la$ is that $\la$ is too big a language: it follows from the construction that every set definable in $\R_n$ is, up to finite unions and projections, added to the language of $\R_{n+1}$. While this produces a model complete expansion in the end, it does not help us understand the added sets in terms of the original structure $\R$.
On the other hand, the exercise in this post implies that every pfaffian chain over $\R$ is definable in $\P(\R)$. So it is natural to let $\R_{\textrm{pfaff}}$ be the expansion of $\R$ by all pfaffian chains over $\R$; since $\R_{\textrm{pfaff}}$ is a reduct of $\P(\R)$ (in the sense that every set definable in $\R_{\textrm{pfaff}}$ is definable in $\P(\R)$), it is also o-minimal.
Open questions
- Is $\R_{\textrm{pfaff}}$ model complete (in the language of all pfaffian chains over $\R$)?
- Is $\R_{\textrm{pfaff}}$ interdefinable with $\P(\R)$, that is, is every set definable in $\P(\R)$ also definable in $\R_{\textrm{pfaff}}$?
It is known, however, that if one replaces “pfaffian chain” by “nested Rolle leaf”, one obtains a reduct $\R_{\textrm{rolle}}$ of $\P(\R)$ that is both model complete (in the language of all nested Rolle leaves over $\R$) and interdefinable with $\P(\R)$.
Therefore, both open questions would have positive answers if one could show that every nested Rolle leaf is existentially definable in $\R_{\textrm{pfaff}}$.