(8) doesn't follow from (5). The assumption in (5) was than $~$n$~$ ranged over naturals, not reals. In fact, (1) only implies (8) if you also require the function to be continuous.
(1) essentially says $~$f$~$ is a homomorphism from $~$(\mathbb{R}^{>0},\cdot)$~$ to $~$(\mathbb{R},+)$~$. To generate a function satisfying (1) but not (8), we need only compose $~$log$~$ (choose a base) with an automorphism in the additive group and show that the composition is not a multiple of a logarithm. We can get such an automorphism by considering $~$\mathbb{R}$~$ as an infinite dimensional vector space over the rationals and, for example, swapping two dimensions.
Comments
Nate Soares
(5) was intended to assume that $~$n \in \mathbb R^{\ge 1},$~$ or possibly $~$\in \mathbb R^{\ge 0}$~$ if you want an easy way to prove (6). In that case, how does (8) not follow from (5)? (If $~$f(x^y)=yf(x)$~$ in general, then $~$f(b^n)=nf(b)$~$ and $~$f(b)=1 \implies f(b^n)=n,$~$ unless I'm missing something.)
Kaya Fallenstein
The proof of (5) only goes through for $~$n\in\mathbb{N}$~$.
You can prove a version of (8) from (5), namely, $~$f(b)=1\Rightarrow f(b^q)=q$~$ for $~$q\in\mathbb{Q}$~$, but this doesn't pin down $~$f$~$ completely, unless you include a continuity condition.
Kaya Fallenstein
tl;dr: I did some reading on related topics, and it turns out that (1) may be sufficient to define logarithms if we take as an axiom that every set is Lebesgue measurable (which is incompatible with the axiom of choice). Otherwise, we need to add an additional condition to (1).
(1) states that $~$f(x\cdot y)=f(x)+f(y)$~$. Given a function $~$g$~$ satisfying this condition, we can generate an additional function satisfying this condition by composing $~$g$~$ with a function $~$h$~$, where $~$h(x+y)=h(x)+h(y)$~$:
$$~$h(g(x\cdot y))=h(g(x))+h(g(y))$~$$
$~$h$~$, as defined, is a solution to Cauchy's functional equation. The family of functions given by $~$h(x)=ch(x)$~$ for some constant $~$c$~$ is always a solution, giving the usual logarithm family. The existence of other solutions is independent of ZF. When they do exist they are always pathological and generate non-Lebesgue measurable sets (for more, see this stackexchange link).
We can prove the existence of such solutions in ZFC by noting that the solutions of the Cauchy functional equation are exactly the homomorphisms from the additive group of $~$\mathbb{R}$~$ to itself. The real numbers form an infinite dimensional vector space over the field $~$\mathbb{Q}$~$. Linear transformations from the vector space to itself translate into homomorphisms from the group to itself. Since the axiom of choice implies that any vector space has a basis, we can, for example, find a non-trivial linear transformation by swapping two basis vectors. This in turn induces a homomorphism from the group to itself. (The Wikipedia page gives the general form of a solution to this functional, which turn out to be all the linear transformations on the vector space.)
(I'm not saying that this article should discuss axiomatizations of set theory, but it doesn't seem good to make statements that are only true if you assume, e.g., an unusual alternative to the axiom of choice.)
Wikipedia proves that the pathological solutions must all be dense in $~$\mathbb{R}$~$, so to exclude them, we can adopt any number of conditions. Wikipedia points at "$~$f$~$ is continuous", "$~$f$~$ is monotonic on any interval", and "$~$f$~$ is bounded on any interval". Continuity seems to be most intuitive; once we have defined the value of the function on the rationals (which we can do with basically the arguments already on this page), the rest of its values are determined.
Nate Soares
How are these changes? (starting at prop 5, through the end)