I am familiar with the following 3 way of defining real powers:
Given $x,y\in\mathbb{R}$, such that $x\gt0$, we can define $$ x^y = \begin{cases} \sup_{\,q\in\mathbb{Q}}\{x^q :q\le y\} &;\ 1\le x\\ \\ \inf_{\,q\in\mathbb{Q}}\{x^q :q\le y\} &;\ 0\lt x\lt 1\\ \end{cases} $$
Using the theory of integration, we define for $x\gt0$: $$ \ln x:=\int_1^x{\frac{dt}{t}} $$ We can then show, using this definition, that $\ln x$ has all the familiar identities of logarithms. In addition we can show that $\ln x$ is a bijection, and has an inverse which we define as $e^x$. We then define for any $x,y\in\mathbb{R}$, such that $x\gt0$: $$ x^y :=e^{y\ln x} $$ And show that this definition coincides with the definition of rational powers (using the identities of logarithms).
Using the theory of series' we can show that the series: $$ e^x:=\sum_{k=0}^{\infty}{\frac{x^k}{k!}} $$ converges for all $x\in\mathbb{R}$. Then, similarily to definition 2, we show that $e^x$ is a bijection and define it's inverse as $\ln x$. Finally we define for any $x,y\in\mathbb{R}$, such that $x\gt0$: $$ x^y :=e^{y\ln x} $$ We can then proceed to show as before that the familiar identities of the exponent hold, and thus the definition coincides with the rational powers.
My question has two parts:
First off, while these definitions coincide (meaning that for a given $x,y\in\mathbb{R}$ all definitions give the same value for $x^y$), can the definitions themselves be derived from a simpler basis. Or, in other words, are all three definitions different descriptions of the same underlying definition, deriving from the same axioms?
Are there additional descriptions for real powers?
The function $f(x)=a^x$ for $a\geq 0$ is uniquely determined by these three properties:
What Martín-Blas is trying to convey is that, once you agree that the fundamental property that an 'exponential-like' operation $E:\Bbb R\rightarrow \Bbb R$ has is $E(x+y)=E(x)E(y)$, then there are, unfortunately, several such maps. However, a lot of these functions are extremely erratic. If we impose even a little amount of 'well-behavedness', we are left with a set of functions which are equivalent to $a^x$ for some $a\geq 0$.
I do not know the proof for when we assume that $f$ is measurable, but I do know the proof for when $f$ is continuous at at least one point. Let's take care of the case when $f(1)=0$. From this alone, you should be able to see that $f(r)=0$ for all $r\in\Bbb Q$ just from the functional equation, and continuity requires that $f$ be equivalently $0$.
Now assume $f$ is not equivalently $0$. Then the functional equation is the statement that $f$ is a group homomorphism from $(\Bbb R, +)$ to $(\Bbb R^+, \cdot)$. Now $(\Bbb R, +)$ and $(\Bbb R^+, \cdot)$ are each topological groups. And it is a theorem that any homomorphism between two topological groups which is continuous at one point is continuous everywhere.
Once we know our function is continuous everywhere, we can actually discover other properties. It is an exercise in Rudin to demonstrate that a function which satisfies the functional equation and is continuous actually equals $e^{cx}$ for some $c$. Let's assume we have the existence of the exponential map and the natural logarithm, but we didn't go any further in defining real exponentials.
The functional equation actually tells us that $f$ is either equivalently zero or never zero. In the latter case, since $f(0)=1$ (as it is a group homomorphism), it is always positive. Set $g(x)=\ln(f(x))$. Then we have $g(x+y)=g(x)+g(y)$ and that $g$ is continuous. It is a common exercise in real analysis to show that functions like $g$ which satisfy the Cauchy equation $g(x+y)=g(x)+g(y)$ and are also continuous are precisely the linear maps. Thus $g(x)=cx$ for some $c\in\Bbb R$. And thus $f(x)=e^{cx}$. Now we set $x=1$ to get that $c=\ln a$ which 'legitimizes' the definition $a^x:= e^{\ln a\cdot x}$.