I'm going through the chapter about the logarithm and exponential functions in Spivak's Calculus.
My question isn't about any particular computation or proof, but rather the following definition
For any number $x$, $e^x=\exp(x)\tag{1}$
To cut to the chase, is the definition above in effect defining a previously undefined symbol (the symbol $e^x$ when $x$ is irrational)?
To provide more details of what I mean, I need to back up and go through the sequence of concepts presented in the chapter.
The function $\log$ is defined
$$\log{x}=\int_1^x \frac{1}{t}dt\tag{2}$$
From this definition we can obtain various properties of $\log$, and in particular that it has an inverse $\log^{-1}$. We give this function the name $\exp$, and it has the property
$$\exp (x+y)=\exp (x)\exp (y)\tag{3}$$
Assume that for a number $a$, $a^n$ has been defined if $n\in\mathbb{N}$.
If we restrict a variable $x$ to be rational, using property $(3)$ we can show that
$$\exp(x)=[\exp(1)]^x$$
if we expand our definition of the symbol $a^x$, in a specific way, for the cases where $x$ is a rational but not natural number.
In particular, we define $a^0=1$, $a^{-n}=\frac{1}{a^n}$, $a^{1/n}=\sqrt[n] {a}$, and $a^{m/n}=\sqrt[n]{a^n}$.
At this point, we can compute $\exp(x)$ for rational $x$ if we know what $\exp{1}$ is. This turns out to be a very special number that we name $e$.
Thus for rational $x$, $\exp(x)=e^x$.
What about if $x$ is irrational?
We know that in this case $\exp(x)$ is defined because $(i)$ $\exp$ is continuous because $\log$ is, $(ii)$ $\exp$ is defined everywhere because the image of $\log$ is $\mathbb{R}$.
We just don't know how to compute it.
So now we reach the point I have a question about.
Note that at this point in the book, there is no definition of a number raised to an irrational power. For $x$ irrational, the symbols
$$2^\sqrt{2}, 3^\pi, e^\sqrt{10}, e^x$$
are undefined, correct?
The next step that Spivak takes is to simply define one of the undefined symbols.
$(1)$ defines the previously undefined symbol $e^x$ as the value of a function that we know exists.
Perhaps this simple definition seems trivial, but I found it to be one of aspects I most had to think about in this chapter.
It's weird because at this point we have
$$\exp(x)=[\exp(1)]^x$$
for all $x$. For rational $x$, $e^x$ means something independently from $\exp(x)$, but for irrational $x$, $e^x$ is simply defined in terms of $\exp{x}$, which means that even if we were to know exactly what the number $e$ is, it seems we wouldn't be able to compute $e^x$ for irrational $x$.
Is my interpretation of the definition and its motivation correct?
A definition of $a^x$ is then given in terms of this new definition of $e^x$
Definition: If $a>0$, then, for any real number $x$,
$$a^x=e^{x\log{a}}$$
and a definition of $\log_a{x}$ is obtained as a sort of consequence of the other definitions.
tl; dr: "Yes."
I can't speak for Spivak, only for myself, but this is how I prefer to develop elementary transcendental functions when teaching real analysis.
The advantages include establishing that $\exp$ has "nice, expected" properties (as listed in the question) with little additional work beyond what is needed to develop the integral and the derivative.
Just as you say, if $a$ is a positive real and $r = p/q$ is rational, we have an effectively algebraic definition of $a^{r} = a^{p/q}$ as the unique positive real whose $q$th power is $a^{p}$. (Existence and uniqueness of such a number must be proven separately, of course!)
An inductive argument shows $$ \exp(r) = [\exp(1)]^{r}\quad\text{for all rational $r$,} $$ and more generally that $$ \exp(r\log a) = a^{r}\quad\text{for all rational $r$.} $$ The expression on the left-hand side is defined for all real $r$, so it furnishes a reasonable definition of the right-hand side. Since $\exp$ is continuous and strictly increasing, this definition of real exponentiation "behaves as expected," e.g., $a^{x} = \sup \{a^{r} : r < x\}$.
As you say, prior to such a definition, an expression such as $2^{\sqrt{2}}$ or $3^{\pi}$ is undefined. (In fact, $\pi$ itself is undefined at this stage of Spivak if memory serves. Tangentially [heh], in developing the circular functions and defining $\pi$ I prefer to follow Ahlfors, whose power series approach I find cleaner than Spivak's inversion of integrals followed by patching.)