Alternate proofs of Hilberts Basis Theorem I'm interested in proofs using ideas from outside commutative algebra of Hilbert's Basis Theorem.

If $R$ is a noetherian ring, then so is $R[X]$.

or its sister version

If $R$ is a noetherian ring, then so is $R[[X]]$.

I am very much aware of the standard non-construtive proof by contradiction given by Hilbert as well as the direct version using Groebner basis.
Most important theorems in mathematics that are old enough have several very different proofs. Comparing different ideas can be very enlightening and also give a hint to possible generalizations in different areas. For the Basis Theorem however, I am not aware of such.
 A: Sorry, this is not an answer, but rather a too-long elaboration on constructive aspects. I post this here because there was some interest about the constructive content of the theorem in the comments.


*

*As pointed out in the comments, the first thing to get straight is the definition of a Noetherian module (or ring). For instance, with the usual definition "any submodule is finitely generated", even the $\mathbb{Z}$-module $\mathbb{Z}$ cannot be shown to be Noetherian constructively: Pick a formula $\varphi$ such that neither $\varphi$ nor $\neg\varphi$ can be shown. Then consider the submodule $U = \{ x \in \mathbb{Z} \,|\, (x = 0) \vee \varphi \}$. If $U$ were finitely generated, it would a forteriori be generated by a single element (Euclid's algorithm) and we could decide whether $1 \in U$ or $1 \not\in U$, that is whether $\varphi$ or $\neg\varphi$.

*A suitable notion of a Noetherian module is given in the very fine book A Course in Constructive Algebra by Mines, Richman, and Ruitenburg: A module is Noetherian if every ascending chain of finitely generated submodules stops (think "$U_n = U_{n+1}$", not "$U_n = U_{n+1} = U_{n+2} = \cdots$").
This definition works fine for many purposes, but not for showing that $R[X]$ is Noetherian if $R$ is. See Chapter VIII of that book. Also it doesn't work well if dependent choice is not available, since it refers to sequences, which can be quite elusive without choice.
A different definition appears in http://www.mittag-leffler.se/sites/default/files/IML-0001-30.pdf (by Coquand and Lombardi). There they claim that Noetherianity of $R$ implies Noetherianity of $R[X]$.
Finally let me recommend the nice article Strongly Noetherian rings and constructive ideal theory by Hervé Perdry. He surveys several kinds of Noetherian conditions.

*A thesis of Coquand, Lombardi and others is that the Noetherian condition is often not the right one constructively. Instead, one should refer to the notion of a coherent ring. In classical mathematics, any Noetherian ring is coherent. See for instance page 27 of Commutative Algebra: Constructive Methods by Lombardi and Quitté.

*Finally, a short and constructive proof that the Krull dimension of $K[X_1,\ldots,X_n]$ is $n$ appears at http://hlombardi.free.fr/publis/KrullMathMonth.pdf (by Coquand and Lombardi).
A: Although I can't imagine I'm telling anyone anything new, here's the proof I know. If $R$ is Noetherian and $I$ is an ideal in $R[X]$ then for each $n\geq0$ consider the subset $J_n$ of $R$ comprised of $\{0\}$ and the leading coefficients of the degree $n$ polynomials in $I$. The $J_n$ are an increasing sequence of ideals; if $J$ is their union then $J=J_N$ for some large $N$; now build a subset of $I$ by looping from $i=0$ to $N$ and at each stage throwing in finitely many polynomials whose leading terms generate $J_i$; an easy induction on degree shows that these polynomials generate $I$. People can muse over just how constructive this is but I have long since ceased to find such questions interesting from a mathematical viewpoint -- ZFC will do for me.
A: There is a proof of the theorem for $R[[x]]$ that uses the well-known result of I.S. Cohen that a ring is noetherian if and only if its prime ideals are finitely generated.  Such a proof is given by Kaplansky in his 1970 book Commutative Rings, Theorem 70.  
This method of proof can be generalized to noncommutative rings to show that the power series ring $R[[x]]$ over a left noetherian ring is left noetherian, as long as one is careful when putting forth a definition of "prime left ideal."  Gerhard Michler gave such a proof in a paper that's not so easy to locate (but it seems to be described here), and I gave a similar proof in Theorem 3.9 in this paper.  
