[FOM] Groebner bases

[Timothy Y. Chow]

I just learned of the book "Groebner Bases" by Thomas Becker and Volker 
Weispfenning.  The authors can be commended for trying to draw the 
reader's attention to a foundational issue, namely the use of the axiom of 
choice in modern commutative algebra.  Unfortunately, their treatment 
suffers from some remarks that make me (and presumably most FOMers) 
cringe.  For example, after pointing out that the collection of all fields 
"is not a set in the framework of ZF," they explain this not by referring 
to Russell's paradox but by saying:

  If you are not familiar with ZF, just recall that ZF takes an
  extremely conservative attitude towards allowing things to call
  themselves sets.

Earlier in the same chapter they remark:

  Interestingly, we do not at present know for sure whether ZF is
  consistent, i.e., leads to contradictions or not, but we know that
  if we drop any one of its axioms, then we can hardly do any
  mathematics at all.

Comments like these do not inspire confidence that when the authors remark 
that some theorem "needs" the axiom of choice, that it is really needed in 
a strong sense.

What really is needed to prove that, say, Buchberger's algorithm for 
computing a Groebner basis always terminates, for rings of the kind that 
software packages like Magma or Macaulay know about?

Tim