I only assumed the sequence was monotonic.

The second comment is fair. I think when I first read this, I ignored the bit about 7zip and understood the sentence as claiming "no Turing machine takes an input smaller than one byte and prints out a 10kb file".

"Suppose an advanced agent with a goal like, e.g., producing smiles or making paperclips."

Typo? Does not seem to be a complete sentence. Maybe "Suppose you have an..."

"Similarly, if you start with a 10 kilobyte text file, and 7zip compresses it down to 2 kilobytes, no amount of time spent trying to further compress the file using other compression programs will ever get that file down to 1 byte." (Emphasis added.)

This claim seems too strong. Do you mean that an arbitrary compression algorithm is unlikely to compress the file to one byte?

Taking what's written at face value, if I assume that every compression I apply monotonically decreases the size of the file, then I need only find a large enough sequence of compressions and compose them to compress my file to one byte. This is of course silly, since the composition is just a huge highly specialized compression program optimized for this instance, but I can spend enough time to make it happen.

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\left(x\right)+f\left(y\right)$. 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\left(x\right)+h\left(y\right)$:

$$h\left(g\right(x\cdot y\left)\right)=h\left(g\right(x\left)\right)+h\left(g\right(y\left)\right)$$

$h$, as defined, is a solution to Cauchy's functional equation. The family of functions given by $h\left(x\right)=ch\left(x\right)$ 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 $R$ to itself. The real numbers form an infinite dimensional vector space over the field $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 $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.

The proof of (5) only goes through for $n\in N$.

You can prove a version of (8) from (5), namely, $f\left(b\right)=1\Rightarrow f\left(b^q\right)=q$ for $q\in Q$, but this doesn't pin down $f$ completely, unless you include a continuity condition.

(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 $(R^{>0},\cdot )$ to $(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 $R$ as an infinite dimensional vector space over the rationals and, for example, swapping two dimensions.