Consider the field of real numbers $(\mathbb R,+,\cdot)$. An expansion of $(\mathbb R,+,\cdot)$ is a tuple $(\mathbb R,+,\cdot,S)$, where $S$ is a collection of subsets of $\mathbb R^n$ for $n \in \mathbb N$. A subset of $\mathbb R^n$ is said to be definable in $(\mathbb R,+,\cdot,S)$, when it is definable by a first order formula in $(\mathbb R,+,\cdot)$ that is allowed to refer to sets in $S$.

A field expansion is said to be $o$-minimal if it allows to define exactly the same subsets of $\mathbb R$. It is a famous theorem of Wilkie (A. J. Wilkie, Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. J. Amer. Math. Soc. 9 (1996), no. 4, 1051–1094.) that $(\mathbb R,+,\cdot,G(\exp))$, where $$G(\exp) = \{(x,\exp(x)) \in \mathbb R^2 \mid x \in \mathbb R\},$$ is an $o$-minimal expansion of $(\mathbb R,+,\cdot)$.

A function $f \colon \mathbb R \to \mathbb R$ is definable if and only if its graph is a definable subset of $\mathbb R^2$. Clearly, $\exp \colon \mathbb R \to \mathbb R$ is definable in $(\mathbb R,+,\cdot,G(\exp))$ but not in $(\mathbb R,+,\cdot)$.

There is a remarkable dichotomy proved by Miller (Chris Miller, Exponentiation is hard to avoid. Proc. Amer. Math. Soc. 122 (1994), no. 1, 257–259.):

Theorem: Let $(\mathbb R,+,\cdot,S)$ be an $o$-minimal expansion of $(\mathbb R,+,\cdot)$. Then either

1. the function $\exp \colon \mathbb R \to \mathbb R$ is definable, or 2. all definable functions are polynomially bounded.

Now, consider $(\mathbb R,<,0,1,+,\cdot,G(\exp\circ \exp))$. This is clearly $o$-minimal, since $G(\exp\circ\exp)$ is definable in $(\mathbb R,<,0,1,+,\cdot,G(\exp))$. According to the theorem, $\exp \colon \mathbb R \to \mathbb R$ should now be definable!

Question: How do you define $\exp \colon \mathbb R \to \mathbb R$ in $(\mathbb R,<,0,1,+,\cdot,G(\exp\circ \exp))$?

There must be some first order formula in $(\mathbb R,+,\cdot)$ making reference to the set $G(\exp \circ \exp)$ that defines the function $\exp \colon \mathbb R \to \mathbb R$. Is it possible to write it down?

More generally, one might then also wonder if some (maybe unique) function $f \colon \mathbb R \to \mathbb R$ is definable in $(\mathbb R,<,0,1,+,\cdot,G(\exp))$ such that $f \circ f = \exp$. Maybe an answer to that is hidden in Kneser's construction of an analytic solution to this problem in (Hellmuth Kneser, Reelle analytische Lösungen der Gleichung $f(f(x))=e^x$ und verwandter Funktionalgleichungen. Journal für die reine und angewandte Mathematik (1950) Volume: 187, page 56-67.)

Consider the field of real numbers $(\mathbb R,+,\cdot)$. An expansion of $(\mathbb R,+,\cdot)$ is a tuple $(\mathbb R,+,\cdot,S)$, where $S$ is a collection of subsets of $\mathbb R^n$ for $n \in \mathbb N$. A subset of $\mathbb R^n$ is said to be definable in $(\mathbb R,+,\cdot,S)$, when it is definable by a first order formula in $(\mathbb R,+,\cdot)$ that is allowed to refer to sets in $S$.

A field expansion is said to be $o$-minimal if it allows to define exactly the same subsets of $\mathbb R$. It is a famous theorem of Wilkie (A. J. Wilkie, Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. J. Amer. Math. Soc. 9 (1996), no. 4, 1051–1094.) that $(\mathbb R,+,\cdot,G(\exp))$, where $$G(\exp) = \{(x,\exp(x)) \in \mathbb R^2 \mid x \in \mathbb R\},$$ is an $o$-minimal expansion of $(\mathbb R,+,\cdot)$.

A function $f \colon \mathbb R \to \mathbb R$ is definable if and only if its graph is a definable subset of $\mathbb R^2$. Clearly, $\exp \colon \mathbb R \to \mathbb R$ is definable in $(\mathbb R,+,\cdot,G(\exp))$ but not in $(\mathbb R,+,\cdot)$.

There is a remarkable dichotomy proved by Miller (Chris Miller, Exponentiation is hard to avoid. Proc. Amer. Math. Soc. 122 (1994), no. 1, 257–259.):

Theorem: Let $(\mathbb R,+,\cdot,S)$ be an $o$-minimal expansion of $(\mathbb R,+,\cdot)$. Then either

1. the function $\exp \colon \mathbb R \to \mathbb R$ is definable, or 2. all definable functions are polynomially bounded.

Now, consider $(\mathbb R,+,\cdot,G(\exp\circ \exp))$. This is clearly $o$-minimal, since $G(\exp\circ\exp)$ is definable in $(\mathbb R,+,\cdot,G(\exp))$. According to the theorem, $\exp \colon \mathbb R \to \mathbb R$ should now be definable!

Question: How do you define $\exp \colon \mathbb R \to \mathbb R$ in $(\mathbb R,+,\cdot,G(\exp\circ \exp))$?

There must be some first order formula in $(\mathbb R,+,\cdot)$ making reference to the set $G(\exp \circ \exp)$ that defines the function $\exp \colon \mathbb R \to \mathbb R$. Is it possible to write it down?

More generally, one might then also wonder if some (maybe unique) function $f \colon \mathbb R \to \mathbb R$ is definable in $(\mathbb R,+,\cdot,G(\exp))$ such that $f \circ f = \exp$. Maybe an answer to that is hidden in Kneser's construction of an analytic solution to this problem in (Hellmuth Kneser, Reelle analytische Lösungen der Gleichung $f(f(x))=e^x$ und verwandter Funktionalgleichungen. Journal für die reine und angewandte Mathematik (1950) Volume: 187, page 56-67.)