Which exponential functions are definable in the real ordered exponential field?

153 Views Asked by At

Consider the real ordered exponential field $(\mathbb{R};+,-,\times,0,1,<,\exp)$, where $\exp$ denotes the standard exponential function $e^x$. I want to know, what exactly is the set of positive real numbers $b$, such that the function $b^x$ is definable in that structure? For example, if $n$ is a positive integer greater than or equal to $2$, is $n^x$ definable in that structure? I would like a characterization of the set of positive real numbers $b$ such that the exponential function $b^x$ is definable in the real ordered exponential field.

2

There are 2 best solutions below

2
On BEST ANSWER

Since $$a^b=e^{b\cdot\ln(a)}=\mathrm{exp}(b\cdot \ln(a))$$ and $\ln$ is definable in your structure as $y=\ln(x)\leftrightarrow x=\mathrm{exp}(y)$, we get that the function $$\mathrm{exp}_a: b\mapsto a^b$$ is definable whenever $a$ is definable. The converse is immediate (consider $\mathrm{exp}_a(1)$), so this gives a complete characterization. In particular, for each positive integer $n$ the function $x\mapsto n^x$ is definable.

0
On

If you're allowing $b > 0$ as a parameter, then I think you can always do it. Write

$$ y = b^x \iff \exists z . \big ( (\exp(z) = b) \land (y = \exp(z \cdot x)) \big ) $$

Conversely, if $y=b^x$ is definable, then $b$ must be too since $b = b^1$.

So then $b^x$ is $\emptyset$-definable exactly when $b$ is $\emptyset$-definable. So in particular we can get $n^x$ for natural numbers $n$.


I hope this helps ^_^