I've been researching Symbolic Integration in Finite Terms using a Differential Algebra and Computer Algebra perspective, reading papers by Risch, Rothstein, Trager, Ritt, Bronstein, etc., as well as some books (the most complete being the last chapter of Geddes' Algorithms for Computer Algebra).
Lately, I've been playing around with the Rothstein/Trager method to determine if an antiderivative with integrand in a Logarithmic Trascendental Extension is elementary or not (in Geddes, it's theorem 12.7). I've been able to determine the symbolic integrability of a lot of functions using this method, and suddenly I thought about using these results to show that some integrals with exponentials are also non-elementary, without proving Rothstein/Trager's method for Exponential Extensions. It's easy to see that, using $u=\log(x)$, $$\int \frac{1}{\log(x)}dx=\int \frac{e^u}{u}du.$$ And hence, as I've already shown that the logarithmic integral is not elementary, then the exponential integral is also non-elementary. I believe that this method can be generalized, and that any function with exponentials and logarithms can be expressed using only logarithms through substitution (or viceversa). Some other examples: $$\int\frac{\log^2(x)+e^{2x}}{e^x\log(x)}dx=\int\frac{v^2+e^{2e^v}}{ve^{e^v}}dv=\int\frac{\log^2(\log(u))+u^2}{u^2\log(\log(u))}du,$$ $$\int \log(\log(x))e^{e^x}dx=\int ve^{e^{e^{e^v}}}dv= \int\frac{\log(\log(\log(\log(u))))}{\log(u)}du.$$
I see two potential problems as to why this isn't the perspective adopted by the papers and books I've read. The first is that there could be a function in terms of exponentials (and maybe also logarithms) that cannot be converted completely into terms of logarithms. However, at least for now, I haven't been able to find any (and believe me, I've tried some weird functions). The other potential problem is related to the formalisms of differential algebra. Function composition is treated from afar in this field of study, and really only comes up through the means of field extensions. For example, the field $\mathbb{C}(x,\log(x))$ doesn't contain the function $\log(\log(x))$, so you would need to adjoin it using $\mathbb{C}(x,\log(x))(\log(\log(x)))=\mathbb{C}(x,\log(x),\log(\log(x)))$. So, I haven't been able to find any theorems regarding substitution as a "technique" of integration. I could rely on analysis to solve this problem, by transfering the burden of proof onto function substitution theorems in analysis, but I feel like that would be too obvious and authors wouldn't bother to make two completely different proofs for logarithmic and exponential extensions if that strategy was available (so maybe it isn't. Why?).
Anyway, I'd like to ask if there really is a need to prove both cases (logarithmic and exponential), or if you could prove one and use substitution for the other. And if this isn't viable, I'd like to know, why? If it's viable, why not use it and avoid long proofs for two cases?
Well, consider the famous $$\int e^{x^2}dx.$$ Do $u=e^{x^2}$. Then $x=\sqrt{\log(u)}$, which makes $dx=\frac{1}{2u\sqrt{\log(u)}}du$. So, $$\int e^{x^2}dx=\frac{1}{2}\int\frac{1}{\sqrt{\log(u)}}du.$$ The elemental-integrability of this "logarithmic" function is not decidable using only the theory of trascendental logarithmic extensions, as the integrand $1/\sqrt{\log(u)}$ lives in an algebraic extension, namely, in $\mathbb{C}(u,\log(u),\sqrt{\log(u)})$. This last extension is algebraic over $\mathbb{C}(u,\log(u))$ because the polynomial $p(z)=z^2-\log(u)\in \mathbb{C}(u,\log(u))[z]$ maps the function $\sqrt{\log(u)}$ to zero.
And thus, we are left with the problem of proving the case for algebraic extensions, which are even harder than exponentials as the theory involves some heavy algebraic geometry. So, probably no case-skipping is for the better. There might be other reasons to prove the exponential case separately, but this seems to me like a good enough reason already.