Lemma.
If every ideal (resp. monomial ideal) in n variables is finitely generated,
then the ACC holds for ideals (resp. monomial ideals) in n variables.
Pf. Take the union of the ideals; that's again an ideal, and its last generator occurs at some finite step along the way..
Lemma.
If the ACC holds for monomial ideals in n variables,
then every ideal in n+1 variables is finitely generated.
Pf. Take slices of the monomial ideals, to get an increasing chain in one dimension down, which by assumption must stop at some slice.
Thm. Every monomial ideal is f.g., and ACC holds in any number of variables.
Thm. The Buchberger algorithm terminates.
Pf. Look at the monomial ideal generated by the initial terms of the generators; this strictly increases each time we add a new generator (or else we wouldn't bother adding it).
Def. Colon ideals.
Def. init I.
