Liouville's theorem gives such a proof for antiderivatives of functions like $e^x/x$ or $e^{x^2}$, and differential Galois theory extends that to Bessel functions, say. But what tools exist for implicit functions like Lambert's W?

1$\begingroup$ Well, $W(z)$ does satisfy a differential equation, $z W'(z) = \frac{W(z)}{1+W(z)}$. So one could still pose this as a question in differential Galois theory. Unfortunately, this equation is nonlinear, which makes it rather complicated. $\endgroup$ – Igor Khavkine Jul 6 '13 at 9:44

$\begingroup$ I would try to show elementary functions cannot have a branch point with such properties as $W(z)$ $\endgroup$ – reuns Feb 25 '17 at 22:22
It seems that the nonlinear differential equation satisfied by the Lambert $W$ function is simple enough for this question to have already been answered. This paper proves that the Lambert $W$ is nonelementary by appealing to a result of Rosenlicht (1969):
Bronstein, M., Corless, R. M., Davenport, J. H. and Jeffrey, D. J. (2008) Algebraic properties of the Lambert W Function from a result of Rosenlicht and of Liouville. Integral Transforms and Special Functions, 19 (10). pp. 709712. https://dx.doi.org/10.1080/10652460802332342
The argument runs roughly as follows. First note that $W(x)$ satisfies a twovariable algebraicdifferential system, where the differential part has a special form:
\begin{equation*} W e^W = x \implies W'\!/W + W' = 1/x \implies \{Y = x/W,\; Y'\!/Y = W'\} . \end{equation*}
Now, consider the differential field $\mathbb{C}(x)(Y,W)$ where $x'=1$, $Y'/Y = W'$ and $f(x,Y,W)=0$, with $f$ polynomial in $Y$ and $W$ over $\mathbb{C}(x)$. According to a more general result of Rosenlicht, the field $\mathbb{C}(x)(Y,W)$ is Liouvillian only if $Y$ and $W$ are algebraic over $\mathbb{C}(x)$. So, if $W(x)$ were elementary (elementary is a special case of Liouvillian) then it would be algebraic.
It remains to check that $W(x)$ is not algebraic. The above article shows that as well. I'll just leave it at saying that it follows from the fact that it satisfies a transcendental equation.

1$\begingroup$ I have worked out another example of this method, supplying a few more details, in the answer to another MO question. $\endgroup$ – Timothy Chow Oct 9 at 17:06
In [Ritt 1948], the method of J. Liouville is given for the Kepler equation.
[Ritt 1948] Ritt, J. F.: Integration in finite terms. Liouville's theory of elementary methods. 1948, page 56
A further method is the method of Rosenlicht, M.: On the explicit solvability of certain transcendental equations. Publications mathématiques de l'IHÉS 36 (1969) 1522. It is a byproduct of Liouville's theory of integration in finite terms. It is written in the language of Differential algebra, but it can be represented also without that.
This method is applicable only for functions satisfying a differential equation that is simple enough.
A reference for Kepler's equation is Zarzuela Armengou, S.: About some questions of differential algebra concerning to elementary functions. Pub. Mat. UAB 26 (1982) (1) 515.
A reference for Lambert W function is Bronstein/Corless/Davenport/Jeffrey 2008 from the answer of Igor Khavkine above.
The branches of Lambert W are the local inverses of the Elementary function $f$ with $f(z)=ze^z$, $z \in \mathbb{C}$.
The incomprehensibly unfortunately hardly noticed theorem of Joseph Fels Ritt in Ritt, J. F.: Elementary functions and their inverses. Trans. Amer. Math. Soc. 27 (1925) (1) 6890 answers which kinds of Elementary functions can have an inverse which is an Elementary function.
And Ritt's theorem shows that no antiderivatives, no differentiation and no differential fields are needed for defining the Elementary functions.
Ritt's theorem is proved also in Risch, R. H.: Algebraic Properties of the Elementary Functions of Analysis. Amer. J. Math 101 (1979) (4) 743759.
By extension of Risch's structure theorem for the elementary functions, Ritt's theorem could possibly be extended to other and to larger classes of functions, as I proposed in my question here: How to extend Ritt's theorem on elementary invertible bijective elementary functions.